Use goto verifier for all-properties in CBMC

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/multi_path_symex_only_checker.h>
 #include <goto-checker/properties.h>
 
@@ -563,6 +564,18 @@ int cbmc_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);
+    }
+  }
 
   if(cmdline.isset("validate-goto-model"))
   {