Use goto verifier for stop-on-fail in JBMC

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -19,16 +19,18 @@ 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>
+#include <util/xml.h>
 
 #include <langapi/language.h>
 
 #include <ansi-c/ansi_c_language.h>
 
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
+#include <goto-checker/stop_on_fail_verifier.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/lazy_goto_model.h>
@@ -585,7 +587,13 @@ int jbmc_parse_optionst::doit()
 
     if(!options.get_bool_option("paths") && !options.is_set("cover"))
     {
-      if(!options.get_bool_option("stop-on-fail"))
+      if(options.get_bool_option("stop-on-fail"))
+      {
+        verifier = util_make_unique<
+          stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
+      }
+      else
       {
         verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
           java_multi_path_symex_checkert>>(