Use goto verifier for stop-on-fail in JBMC

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
+#include <util/make_unique.h>
 #include <util/unicode.h>
 #include <util/xml.h>
 #include <util/version.h>
@@ -30,6 +31,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/multi_path_symex_only_checker.h>
+#include <goto-checker/stop_on_fail_verifier.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/lazy_goto_model.h>
@@ -571,17 +573,27 @@ int jbmc_parse_optionst::doit()
         return result_to_exit_code(result);
       }
     }
-    else
+
+    if(!options.get_bool_option("paths"))
     {
-      // we do all properties
-      if(!options.get_bool_option("paths"))
+      std::unique_ptr<goto_verifiert> verifier;
+
+      if(options.get_bool_option("stop-on-fail"))
       {
-        all_properties_verifiert<multi_path_symex_checkert> verifier(
-          options, ui_message_handler, goto_model);
-        resultt result = verifier();
-        verifier.report();
-        return result_to_exit_code(result);
+        verifier =
+          util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
       }
+      else
+      {
+        verifier =
+          util_make_unique<all_properties_verifiert<multi_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
+      }
+
+      resultt result = (*verifier)();
+      verifier->report();
+      return result_to_exit_code(result);
     }
 
     // The `configure_bmc` callback passed will enable enum-unwind-static if