Skip to content

Commit b0fd00d

Browse files
committed
Add incremental-smt2-solver command line option
So that the new interface can be kept separate from the existing one whilst work is in-progress.
1 parent aef9f3f commit b0fd00d

File tree

2 files changed

+11
-0
lines changed

2 files changed

+11
-0
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff 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"

src/cbmc/cbmc_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff 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)" \

0 commit comments

Comments
 (0)