Skip to content

Commit 2eb7294

Browse files
Use goto verifier for dimacs and SMT2 outfile in JBMC
1 parent d39b6ed commit 2eb7294

File tree

1 file changed

+17
-1
lines changed

1 file changed

+17
-1
lines changed

jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -583,9 +583,25 @@ int jbmc_parse_optionst::doit()
583583
}
584584
}
585585

586+
if(
587+
options.get_bool_option("dimacs") ||
588+
!options.get_option("outfile").empty())
589+
{
590+
if(!options.get_bool_option("paths"))
591+
{
592+
stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
593+
options, ui_message_handler, goto_model);
594+
(void)verifier();
595+
return CPROVER_EXIT_SUCCESS;
596+
}
597+
}
598+
586599
std::unique_ptr<goto_verifiert> verifier = nullptr;
587600

588-
if(!options.get_bool_option("paths") && !options.is_set("cover"))
601+
if(
602+
!options.get_bool_option("paths") && !options.is_set("cover") &&
603+
!options.get_bool_option("dimacs") &&
604+
options.get_option("outfile").empty())
589605
{
590606
if(options.get_bool_option("stop-on-fail"))
591607
{

0 commit comments

Comments
 (0)