SMT solving is not invoked with `--incremental-loop`

[nianzelee]

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.

[martin-cs]

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.

[thomasspriggs]

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 in solver_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 in cbmc_parse_options.cpp automatically switches on the refine and refine-arrays options. This doesn't necessarily seem to be desirable behaviour; particularly given the aforementioned incompatibilities.
• The single_loop_incremental_symex_checkert currently uses the push() and pop() 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 with push and pop 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});
}