File tree Expand file tree Collapse file tree 2 files changed +11
-0
lines changed
Expand file tree Collapse file tree 2 files changed +11
-0
lines changed Original file line number Diff line number Diff line change @@ -409,6 +409,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
409409 options.set_option (" smt2" , true );
410410 }
411411
412+ if (cmdline.isset (" incremental-smt2-solver" ))
413+ {
414+ options.set_option (
415+ " incremental-smt2-solver" , cmdline.get_value (" incremental-smt2-solver" )),
416+ solver_set = true ;
417+ }
418+
412419 if (cmdline.isset (" external-sat-solver" ))
413420 {
414421 options.set_option (
@@ -1042,6 +1049,9 @@ void cbmc_parse_optionst::help()
10421049 " --yices use Yices\n "
10431050 " --z3 use Z3\n "
10441051 " --refine use refinement procedure (experimental)\n "
1052+ " --incremental-smt2-solver cmd\n "
1053+ " command to invoke external SMT solver for\n "
1054+ " incremental solving (experimental)\n "
10451055 " --external-sat-solver cmd command to invoke SAT solver process\n "
10461056 HELP_STRING_REFINEMENT_CBMC
10471057 " --outfile filename output formula to given file\n "
Original file line number Diff line number Diff line change @@ -57,6 +57,7 @@ class optionst;
5757 OPT_JSON_INTERFACE \
5858 " (smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
5959 " (cprover-smt2)" \
60+ " (incremental-smt2-solver):" \
6061 " (external-sat-solver):" \
6162 " (no-sat-preprocessor)" \
6263 " (beautify)" \
You can’t perform that action at this time.
0 commit comments