Use goto verifier for --paths with show-vcc and -program-only in CBMC

We can now use single_path_symex_only_checkert instead of bmct.

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -40,6 +40,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/multi_path_symex_only_checker.h>
 #include <goto-checker/properties.h>
+#include <goto-checker/single_path_symex_only_checker.h>
 #include <goto-checker/stop_on_fail_verifier.h>
 
 #include <goto-programs/adjust_float_expressions.h>
@@ -559,13 +560,22 @@ int cbmc_parse_optionst::doit()
     options.get_bool_option("program-only") ||
     options.get_bool_option("show-vcc"))
   {
-    if(!options.get_bool_option("paths"))
+    std::unique_ptr<goto_verifiert> verifier;
+    if(options.get_bool_option("paths"))
     {
-      all_properties_verifiert<multi_path_symex_only_checkert> verifier(
+      verifier = util_make_unique<
+        all_properties_verifiert<single_path_symex_only_checkert>>(
         options, ui_message_handler, goto_model);
-      (void)verifier();
-      return CPROVER_EXIT_SUCCESS;
     }
+    else
+    {
+      verifier = util_make_unique<
+        all_properties_verifiert<multi_path_symex_only_checkert>>(
+        options, ui_message_handler, goto_model);
+    }
+
+    (void)(*verifier)();
+    return CPROVER_EXIT_SUCCESS;
   }
 
   if(