Use goto verifier for dimacs and SMT2 outfile in CBMC

peterschrammel · peterschrammel · commit d39b6edc6d7a · 2019-01-24T22:45:43.000Z
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -558,9 +558,23 @@ int cbmc_parse_optionst::doit()
     }
   }
 
+  if(
+    options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
+  {
+    if(!options.get_bool_option("paths"))
+    {
+      stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
+        options, ui_message_handler, goto_model);
+      (void)verifier();
+      return CPROVER_EXIT_SUCCESS;
+    }
+  }
+
   std::unique_ptr<goto_verifiert> verifier = nullptr;
 
-  if(!options.get_bool_option("paths") && !options.is_set("cover"))
+  if(
+    !options.get_bool_option("paths") && !options.is_set("cover") &&
+    !options.get_bool_option("dimacs") && options.get_option("outfile").empty())
   {
     if(options.get_bool_option("stop-on-fail"))
     {

Original file line number	Diff line number	Diff line change
`@@ -558,9 +558,23 @@ int cbmc_parse_optionst::doit()`
`558`	`558`	`}`
`559`	`559`	`}`
`560`	`560`
	`561`	`+ if(`
	`562`	`+ options.get_bool_option("dimacs") \|\| !options.get_option("outfile").empty())`
	`563`	`+ {`
	`564`	`+ if(!options.get_bool_option("paths"))`
	`565`	`+ {`
	`566`	`+ stop_on_fail_verifiert<multi_path_symex_checkert> verifier(`
	`567`	`+ options, ui_message_handler, goto_model);`
	`568`	`+ (void)verifier();`
	`569`	`+ return CPROVER_EXIT_SUCCESS;`
	`570`	`+ }`
	`571`	`+ }`
	`572`	`+`
`561`	`573`	`std::unique_ptr<goto_verifiert> verifier = nullptr;`
`562`	`574`
`563`		`- if(!options.get_bool_option("paths") && !options.is_set("cover"))`
	`575`	`+ if(`
	`576`	`+ !options.get_bool_option("paths") && !options.is_set("cover") &&`
	`577`	`+ !options.get_bool_option("dimacs") && options.get_option("outfile").empty())`
`564`	`578`	`{`
`565`	`579`	`if(options.get_bool_option("stop-on-fail"))`
`566`	`580`	`{`