Spurious verification error due to the use of SMT engine

[sepideha]

CBMC version: 5.72.1 (cbmc-5.72.1-dirty) Operating system: Ubuntu Exact command line resulting in the issue: ./cbmc --function f --trace --smt2 nonLinEquality.c What behavior did you expect: VERIFICATION SUCCESSFUL What happened instead:

Running SMT2 QF_AUFBV using Z3
** Results:
nonLinEquality.c function f
[f.assertion.1] line 21 assertion p == q: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

In the following example, using ./cbmc --function f --trace nonLinEquality.c with MiniSAT, the result is VERIFICATION SUCCESSFUL. However, by adding --smt2 to the command line a spurious error is reported. Is this bug due to the use of uninterpreted function in SMT?

unsigned int func(unsigned int a, unsigned int b)
  {
    unsigned int m = 1;
    for (int i = 0; i < 10; i++)
    {
      m = m + (a + b * a);
    }
    return (m % 2);
  }

int f(unsigned int a, unsigned int b)
  {
    if (a<-2 || a > 2 || b > 3 || b <-3)
            return;
    int c = a;
    int d = b;
    unsigned int p = func(a, b);
    unsigned int q = func(c, d);
    assert(p ==q );
    return (a+b+p+q);
  }

[thomasspriggs]

Hi. I haven't been able to reproduce this error on my local machine. I get a successful verification both with the SAT back end and with the --smt2 argument. For reference I am using "CBMC version 5.77.0 (cbmc-5.77.0-78-gb0dc2ea2f0) 64-bit x86_64 linux" and "Z3 version 4.8.12 - 64 bit". The most straight forward potential resolutions to your issue would be to confirm that you have a sufficiently recent version of Z3 installed and to try the latest version of cbmc. Note that cbmc requires separately installed SMT solvers as we don't bundle bundle any SMT solvers into the cbmc packages.

If the above suggestions don't get you anywhere, then the next step would be to run cbmc with --outfile formula.smt. This would write the SMT formula to file, so we can see what is being sent.

[thomasspriggs]

One thing that comes to mind is that --smt2 requires z3 to be in the path. I can also confirm that this example works with the new SMT back end. The new back end is a work-in-progress rewrite which does not yet support structs, unions or floating point arithmetic. But it is sufficiently complete for your example it can be run by using cbmc --function f --trace --incremental-smt2-solver "z3 --smt2 -in" example.c. In this case the parameter for --incremental-smt2-solver is the command to run the SMT solver including the path and the arguments to make it take smtlib 2 input from stdin if necessary for that solver.

[sepideha]

Thanks for your reply. I updated CBMC to the latest version (tag: 5.78.0 (cbmc-5.78.0-dirty)) and still the same issue. I noticed that even though I don't have Z3 installed in my machine, CBMC somehow can use Z3, perhaps it uses the default or an old version of z3 which is buggy? (I examined the PATH and I am sure I never installed Z3 and which z3 did not show it).

./cbmc --function f --trace nonLinEquality.c --smt2
...

**Passing problem to SMT2 QF_AUFBV using Z3**
converting SSA
Runtime Convert SSA: 0.00186448s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.00412017s
Runtime decision procedure: 0.00623634s

** Results:
nonLinEquality.c function f
[f.assertion.1] line 21 assertion p == q: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

I will install Z3 in my machine.

[peterschrammel]

Note that ERROR/VERIFICATION ERROR does not mean that the property is violated (that would be FAILURE/VERIFICATION FAILED), but that there was an error while running the verification (most likely because it can't find a z3 executable on the path).

[sepideha]

Thanks for the clarification.

[tautschnig]

Thanks for the clarification.

Would you mind letting us know whether installing z3 made a material difference?

[thomasspriggs]

Given that we haven't heard back from @sepideha for a number of days, I am going to assume that they have managed to get things working and close out the issue. Please feel free to re-open this issue if this is not the case.