MathSAT SMT2 not working

[xXMarkuski]

CBMC version: Tested with CBMC 5.27.0 and 5.35.0 Operating system: Fedora 34 Test Case:

#include <assert.h>

void main(){
  assert(0);
}

Exact command line resulting in the issue:

$cbmc simpleProgram.c --mathsat | tail
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

What behaviour did you expect: Mathsat returns SAT What happened instead: MathSAT exits with an error message

I believe this is due to commit "Fixed SMT encoding of array_of_expr" 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.

Previously I created a question on the CProver Support list.

[martin-cs]

This will also affect Boolector, which is often the best performing solver and is used by several commercial users.

[martin-cs]

@thomasspriggs @TGWDB I know you are working with this at the moment.