Some backend SMT solvers failed on a program with an array
Closed this issue · 4 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 --unwind 6 --bounds-check --unwinding-assertions --bitwuzla
What behaviour did you expect: the SMT solver can handle the formulas
What happened instead: errors (see below)
...
Passing problem to SMT2 QF_AUFBV (with FPA) using Bitwuzla
converting SSA
Runtime Convert SSA: 0.00691677s
Running SMT2 QF_AUFBV (with FPA) using Bitwuzla
Runtime Solver: 0.00405312s
Runtime decision procedure: 0.0111767s
** Results:
binsearch.c function binsearch
[binsearch.unwind.0] line 6 unwinding assertion loop 0: ERROR
[binsearch.array_bounds.1] line 10 array 'a' lower bound in a[(signed long int)middle]: ERROR
[binsearch.array_bounds.2] line 10 array 'a' upper bound in a[(signed long int)middle]: ERROR
[binsearch.array_bounds.3] line 12 array 'a' lower bound in a[(signed long int)middle]: ERROR
[binsearch.array_bounds.4] line 12 array 'a' upper bound in a[(signed long int)middle]: ERROR
** 0 of 5 failed (1 iterations)
VERIFICATION ERROR
The input file binsearch.c was taken from the tutorial.
Such errors also happened for boolector, cvc4, cvc5, mathsat, and yices.
The default SMT solver Z3 worked fine on the program.
I increased the verbosity level to 100 in order to see what SMT solvers complained about, but it seems such information was not relayed to console logs.
Are the SMT solvers on your path? If not, it could be that. Can you try generating the SMT directly to a file (using --smt2 --outfile problem.smt2) and running the SMT solvers on that?
Are the SMT solvers on your path? If not, it could be that. Can you try generating the SMT directly to a file (using
--smt2 --outfile problem.smt2) and running the SMT solvers on that?
Thanks for the reply! Indeed, some solvers were not on the path, but Boolector still complained about the dumped SMT file.
problem.smt:3: unsupported command 'set-option'
It would be helpful if CBMC could make its console logs more helpful.
Interesting. Are you using Boolector or Bitwuzla? Yes; the logging for the SMT back-end could be improved.
I was using Boolector.