Using MathSAT SMT2 not possible

[Markus Toran]

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

[Martin Nyx Brain]

On Thu, 2021-07-29 at 02:12 -0700, Markus Toran wrote:
> Dear all,
>
>
> currently using CBMC with MathSat SMT2 backend causes an verification
> error:
> Test Case:

<snip>

> 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.

That sounds about right.

> Is this a known bug of CBMC or should I open an issue on GitHub?

It is an area of debate but I hadn't realised that it had broken
support for solvers other than Z3 and CVC4. Please can you open an
issue for this on github because this is not OK.

Cheer,
- Martin

[Thomas Spriggs]

Hi

This isn't an issue I've seen before. Please raise it as a github issue.

The SAT solver support in CBMC is more thoroughly tested than SMT solver support. So you are likely to encounter the fewest issues using SAT solving. For the SMT back end I think more testing has been done recently using Z3 and CVC4. So you may wish to try those solvers instead if you are interested in SMT solving, but not specifically MathSat.

Thomas

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/b073cc8b-0147-4f9f-bb5e-24e6e2f97b5bn%40googlegroups.com.

Diffblue Ltd, a company registered in England and Wales number 09958102. Registered office 10 St Ebbes Street, Oxford, OX1 1PT, UK

[Markus Toran]

Hi

Thanks for the quick reply, I created an issue on GitHub.

Markus

[Martin Nyx Brain]

On Fri, 2021-07-30 at 07:22 -0700, Markus Toran wrote:
> Hi
>
> Thanks for the quick reply, I created an issue on GitHub.

Thank you!

Cheers,
- Martin