Dear all,
currently using CBMC with MathSat SMT2 backend causes an verification error:
Test Case:
#include <assert.h>
void main(){
assert(0);
}
Running $ cbmc simpleProgram.c --mathsat | tail results in:
SMT2 solver returned error message:
"The CNF conversion does not support quantifiers"
Running SMT2 QF_AUFBV using MathSAT
Runtime Solver: 0.0204232s
Runtime decision procedure: 0.0205809s
** Results:
simpleProgram.c function main
[main.assertion.1] line 4 assertion 0: ERROR
** 0 of 1 failed (1 iterations)
VERIFICATION ERROR
I believe this is due to commit "Fixed SMT encoding of array_of_expr" (aaa7a3a5394aaf5c8a283cba55094c19e5daecc3) first included in version 5.27.0, which enabled generation of using a quantifier-based initialization instead of lambda in smt2_conv.cpp line 4400, while MathSAT does not fully support quantifiers.
Version 5.26.0 correctly fails the verification.
Is this a known bug of CBMC or should I open an issue on GitHub?
Best regards
Markus Toran