Print incremental-status when doing incremental solving

It is not possible to conclude successful verification before
the unwinding has finished, so this prints inconclusive until
the analysis is complete. However, if one property has been
falsified, then even though the analysis can continue to check
other properties, the verification will certainly fail.

Author: Thomas Kiley

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -47,6 +47,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)
 {
@@ -64,6 +81,8 @@ operator()(propertiest &properties)
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, equation);
 
+    output_incremental_status(properties, log);
+
     initial_equation_generated = true;
   }
 
@@ -162,6 +181,8 @@ operator()(propertiest &properties)
       properties, result.updated_properties, equation);
 
     current_equation_converted = false;
+
+    output_incremental_status(properties, log);
   }
 
   return result;