Use goto verifier for dimacs and SMT2 outfile in CBMC

peterschrammel · peterschrammel · commit 2789dba36c74 · 2019-01-20T23:18:13.000Z
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -573,9 +573,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
`@@ -573,9 +573,23 @@ int cbmc_parse_optionst::doit()`
`573`	`573`	`}`
`574`	`574`	`}`
`575`	`575`
	`576`	`+ if(`
	`577`	`+ options.get_bool_option("dimacs") \|\| !options.get_option("outfile").empty())`
	`578`	`+ {`
	`579`	`+ if(!options.get_bool_option("paths"))`
	`580`	`+ {`
	`581`	`+ stop_on_fail_verifiert<multi_path_symex_checkert> verifier(`
	`582`	`+ options, ui_message_handler, goto_model);`
	`583`	`+ (void)verifier();`
	`584`	`+ return CPROVER_EXIT_SUCCESS;`
	`585`	`+ }`
	`586`	`+ }`
	`587`	`+`
`576`	`588`	`std::unique_ptr<goto_verifiert> verifier = nullptr;`
`577`	`589`
`578`		`- if(!options.get_bool_option("paths") && !options.is_set("cover"))`
	`590`	`+ if(`
	`591`	`+ !options.get_bool_option("paths") && !options.is_set("cover") &&`
	`592`	`+ !options.get_bool_option("dimacs") && options.get_option("outfile").empty())`
`579`	`593`	`{`
`580`	`594`	`if(options.get_bool_option("stop-on-fail"))`
`581`	`595`	`{`