CBMC silently ignores syntax errors from SMT solver

[SaswatPadhi]

CBMC version: d98b56b
Operating system: Mac OS 10.15.7

Test case:

#include <assert.h>

__CPROVER_bool arr[2];

void main()
{
  int i;
  __CPROVER_assume(0 <= i && i < 2);

  assert(!arr[i]);
}

Exact command line resulting in the issue:

cbmc --smt2 test.c

The above command will trigger a solver-agnostic (generic) SMT2 translation which should not currently work with Z3.

What behaviour did you expect:

CBMC would report an ERROR status.
Indeed Z3 does not accept the generated SMT2 file:

$ cbmc --smt2 test.c --outfile test.smt2
. . .
$ z3 -smt2 test.smt2 | head
(error "line 53 column 73: logic does not support quantifiers")
(error "line 59 column 73: logic does not support quantifiers")
(error "line 65 column 66: Sorts (_ BitVec 1) and Bool are incompatible")
(error "line 71 column 44: Sorts (_ BitVec 1) and Bool are incompatible")
(error "line 72 column 44: Sorts (_ BitVec 1) and Bool are incompatible")
unsat
(error "line 107 column 17: model is not available")
(error "line 108 column 17: model is not available")
(error "line 109 column 17: model is not available")
(error "line 110 column 40: model is not available")

The errors at lines 53,59 are being discussed at #5977.
The errors at lines 65,71,72 will be fixed by #6004.

What happened instead:

1. CBMC does not display any of the Z3 errors & silently ignores them.
2. It reports that verification was SUCCESSFUL (Perhaps because Z3 returned unsat after the errors).

[thomasspriggs]

Firstly, there is a slight misunderstanding with how the cbmc options are working here. The cbmc --smt2 test.c does not generate solver-agnostic (generic) SMT2 formulas. It uses the z3 solver by default and crucially, it does so with z3 specialisations. See src/solvers/smt2/smt2_conv.cpp line 108 for details of what these z3 specific settings/feature sets are.
When using cbmc --smt2 test.c --outfile test.smt2, the z3 specific formula generation settings are switched off and the file written is intended to be generic. However it is different from the file generated in the previous case. The smt2 output file with the z3 feature set can be written by using cbmc --smt2 --z3 test.c --outfile test.smt2. When the file generated in this manner is given to z3, no errors are returned from before the unsat line of output.

The second issue here are the errors generated after the unsat output. My understanding is that these are due to the non-interactive nature of how cbmc currently interacts with the solver. The entire input to the solver is written out to a file at once. In the case where the solver returns sat we need a set of get-value commands after the (check-sat) command is issued. But at the time of writing the file cbmc does not know if the problem is satisfiable or not. So the get-value commands are included in the file either way and the get-value commands are evaluated by the solver even when it has returned unsat. This generates expected errors, which cbmc can then safely ignore. Solver errors should only be ignored after cbmc has parsed the unsat result. Errors before receiving unsat or when the result is sat should not be ignored. See smt2_dect::read_result for the implementation of this.

I think the "Sorts (_ BitVec 1) and Bool are incompatible" errors have been resolved by merging PR #6004. Given that all the errors should now either be fixed or explained are you OK with this ticket being closed out @SaswatPadhi ?

[SaswatPadhi]

Thanks for looking into this, and for the detailed explanation, @thomasspriggs!

Yes, I am closing this issue now, since, as you said, all errors before the unsat error are fixed / explainable.