SMT2 back-end: detect when solver returns unexpected model

[tautschnig]

We have seen examples of Z3 responding with

((B1502 (forall ((|main::tmp_cc$0!0@1#0| (_ BitVec 64)))
  (let ((a!1 (or (and (not (bvule #x000000000000000c |main::tmp_cc$0!0@1#0|))
                      (bvule #x000000000000000b |main::tmp_cc$0!0@1#0|)
[...]

when we expected just true or false as model (which Bitwuzla seemed to get right on the very same input program). Report these as errors rather than using the incomplete assignment. Such an incomplete assignment would make us re-try forever without making progress.

Fixes: #8365

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 42.10526% with 11 lines in your changes missing coverage. Please review.

Project coverage is 78.32%. Comparing base (629dbcd) to head (b0eedde).
Report is 2 commits behind head on develop.

Files	Patch %	Lines
src/solvers/smt2/smt2_dec.cpp	42.10%	11 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8379      +/-   ##
===========================================
- Coverage    78.35%   78.32%   -0.03%     
===========================================
  Files         1726     1726              
  Lines       188424   188506      +82     
  Branches     18248    18249       +1     
===========================================
+ Hits        147631   147646      +15     
- Misses       40793    40860      +67     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[rod-chapman]

OK... trying it on the issues/8365 test case in my cbmc-examples repo. It terminates OK, and I see

SMT2 solver returned non-Boolean value for variable B1528

in the on-screen output, so better than before.

BUT... which actual proof is failing? It now reports 36 lines with ERROR at the end, so I've no idea which proof it is that's causing the problem.

[tautschnig]

BUT... which actual proof is failing? It now reports 36 lines with ERROR at the end, so I've no idea which proof it is that's causing the problem.

I'm afraid the answer given by Z3 is not useful enough for us to determine that. Replace --smt2 by --bitwuzla in your Makefile to get:

[...]
[main.assertion.1] line 32 assertion a[10] == 1: FAILURE

** 1 of 1596 failed (2 iterations)
VERIFICATION FAILED
make: *** [Makefile:16: results_smt] Error 10

[rod-chapman]

Ah yes... that's more like it.

[kroening]

SMT2 solver returned non-Boolean value for variable B1528

Nudge: note that the value is Boolean. The problem is that it's not a constant.

[tautschnig]

SMT2 solver returned non-Boolean value for variable B1528

Nudge: note that the value is Boolean. The problem is that it's not a constant.

Err, yes, fixed.