Switch the output to incremental status

Author: Thomas Kiley

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -48,6 +48,23 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
     prop_conv_solver->set_all_frozen();
 }
 
+void output_incremental_status(
+  const propertiest &properties,
+  messaget &message_hander)
+{
+  const auto any_failures = std::any_of(
+    properties.begin(),
+    properties.end(),
+    [](const std::pair<irep_idt, property_infot> &property) {
+      return property.second.status == property_statust::FAIL;
+    });
+  std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE";
+  structured_datat incremental_status{
+    {{labelt({"incremental", "status"}),
+      structured_data_entryt::data_node(json_stringt(status))}}};
+  message_hander.statistics() << incremental_status;
+}
+
 incremental_goto_checkert::resultt single_loop_incremental_symex_checkert::
 operator()(propertiest &properties)
 {
@@ -65,13 +82,7 @@ operator()(propertiest &properties)
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, equation);
 
-    const auto is_failure = std::any_of(
-      properties.begin(), properties.end(), [](const
-                                               std::pair<irep_idt, property_infot> &property) {
-        return property.second.status == property_statust::FAIL;
-      });
-    output_overall_result(
-      is_failure ? ::resultt::FAIL : ::resultt::PASS, ui_message_handler);
+    output_incremental_status(properties, log);
 
     initial_equation_generated = true;
   }
@@ -178,13 +189,7 @@ operator()(propertiest &properties)
 
     current_equation_converted = false;
 
-    const auto is_failure = std::any_of(
-      properties.begin(), properties.end(), [](const
-      std::pair<irep_idt, property_infot> &property) {
-        return property.second.status == property_statust::FAIL;
-      });
-    output_overall_result(
-        is_failure ? ::resultt::FAIL : ::resultt::PASS, ui_message_handler);
+    output_incremental_status(properties, log);
 
   }