Verification test fails despite formula being equivalent to true

Hello,

I wrote a simple program computing absolute value:

int f(int x) {
    _Assume(1);
    int y;
    if (x < 0) {
        y = 0 - x;
    } else {
        y = x;
   }
    _Assert(y >= 0);
   return y;
}

and I get the following formula:

Generated formula:
((1 ≠ 0) ⇒ (((x < 0) ⋀ (((0 - x) ≥ 0) ⋀ TRUE)) ⋁ ((¬(x < 0)) ⋀ ((x ≥ 0) ⋀ TRUE))))
Solver result:
UNSATISFIABLE

I went over it twice and compared it to my calculations on paper and it should always evaluate to true, yet the solver deems it unsatisfiable. If it helps, this is what I call at the end of the test:

SolverResult res = computeVerificationResult(code);
assertTrue(res.isUnSatifiable());

All my other tests (positive) have this as well and I doubt they are all just false positives.

As explained in the project presentation, a SMT solver solves the satisfaction problem, not the validity problem.

If we want to check whether a formula \varphi of first-order logic is valid (i.e. true for all assignments), we check whether \neg\varphi is unsatisfiable (see CompilerTests.java:342). Thus, on correct programs, computeVerificationResult returns unsat. If the program violates the specification, you get a counter-example.

This is also what happens in the public tests.

1 Like

I just solved the problem after staring at your explanation for a long while: I thought the formula was only produced when the test fails, but it turns out I pass my own test… thanks anyway :smile:

1 Like