search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
847 stars 262 forks source link

Some backend SMT solvers failed on a program with an array #8186

Closed nianzelee closed 9 months ago

nianzelee commented 9 months ago

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.

martin-cs commented 9 months ago

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?

nianzelee commented 9 months ago

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.

martin-cs commented 9 months ago

Interesting. Are you using Boolector or Bitwuzla? Yes; the logging for the SMT back-end could be improved.

nianzelee commented 9 months ago

I was using Boolector.