SMT solving is not invoked with `--incremental-loop`
Opened this issue · 2 comments
CBMC version: 5.95.1
Operating system: Ubuntu 22.04 (kernel version 6.5.0-15-generic)
Exact command line resulting in the issue: cbmc binsearch.c --function binsearch --bounds-check --unwinding-assertions --verbosity 8 --incremental-loop binsearch.0 --smt2 --unwind-max 3
What behaviour did you expect: Z3 (the default SMT solver) is used to solve the constraints
What happened instead: From the console log, MiniSAT 2.2.1 was used instead (see below)
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing binsearch.c
Converting
Type-checking binsearch
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Current unwinding: 1
Unwinding loop binsearch.0 iteration 1 (3 max) file binsearch.c line 6 function binsearch thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 2
Unwinding loop binsearch.0 iteration 2 (3 max) file binsearch.c line 6 function binsearch thread 0
Passing problem to refinement loop with MiniSAT 2.2.1 with simplified
...
The input file binsearch.c
was taken from the tutorial.
int binsearch(int x)
{
int a[16];
signed low = 0, high = 16;
while(low < high)
{
signed middle = low + ((high - low) >> 1);
if(a[middle] < x)
high = middle;
else if(a[middle] > x)
low = middle + 1;
else // a[middle]==x
return middle;
}
return -1;
}
I also tried adding --incremental-smt2-solver 'z3 -smt2 -in'
, but MiniSAT was used again.
Without --incremental-loop
, Z3 was invoked as expected.
IIRC the incremental mode works with MiniSAT because the SMT back-end is very much one-shot. The work that @thomasspriggs was doing on the new SMT back-end would resolve that in the longer term.
Looks like this should work with the new incremental SMT back end with a few minor fixes -
- Some command line argument / option fixing to ensure the correct decision procedure is used. The "refine" option causes a SAT based
bv_refinementt
to be used insolver_factory.cpp
even when an SMT solver is specified. I think "refine" and SMT options should probably be considered to be mutually exclusive and hence generate a usage error. The current behaviour is to ignore the SMT argument as outlined in this issue. - The
--incremental-loop
argument incbmc_parse_options.cpp
automatically switches on therefine
andrefine-arrays
options. This doesn't necessarily seem to be desirable behaviour; particularly given the aforementioned incompatibilities. - The
single_loop_incremental_symex_checkert
currently uses thepush()
andpop()
interface of the decision procedure. A minor change to implement this in the new SMT decision procedure is required. As incremental solving is supported along withpush
andpop
in the AST the implementation is trivial -
void smt2_incremental_decision_proceduret::push()
{
solver_process->send(smt_push_commandt{1});
}
void smt2_incremental_decision_proceduret::pop()
{
solver_process->send(smt_pop_commandt{1});
}