Initial version

Needs some tidy up but this prints output that is consistent with the
old version

Author: Thomas Kiley

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "bmc_util.h"
 #include "counterexample_beautification.h"
+#include "report_util.h"
 
 single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
   const optionst &options,
@@ -64,6 +65,14 @@ 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);
+
     initial_equation_generated = true;
   }
 
@@ -129,8 +138,14 @@ operator()(propertiest &properties)
           ? resultt::progresst::FOUND_FAIL
           : resultt::progresst::DONE;
 
+      const auto is_failure = result.progress ==
+                              resultt::progresst::FOUND_FAIL;
+
+//      output_overall_result(
+//        is_failure ? ::resultt::FAIL : ::resultt::PASS, ui_message_handler);
+
       // We've got a trace to report.
-      if(result.progress == resultt::progresst::FOUND_FAIL)
+      if(is_failure)
         break;
 
       // Nothing else to do with the current set of assertions.
@@ -162,6 +177,15 @@ operator()(propertiest &properties)
       properties, result.updated_properties, equation);
 
     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);
+
   }
 
   return result;