Use goto verifier for all-properties in JBMC

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 
 #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-programs/adjust_float_expressions.h>
@@ -570,6 +571,18 @@ int jbmc_parse_optionst::doit()
         return result_to_exit_code(result);
       }
     }
+    else
+    {
+      // we do all properties
+      if(!options.get_bool_option("paths"))
+      {
+        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);
+      }
+    }
 
     // The `configure_bmc` callback passed will enable enum-unwind-static if
     // applicable.