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.