Closed juliusbrehme closed 1 year ago
Formula f{(x1 != x2) && (x1 < 1) && (x2 < 1) && (0 <= x1) && (0 <= x2)};
Let me rewrite this formula using a list of conjuncts:
The first conjunct x1 != x2
can be rewritten into (x1 > x2) or (x1 < x2)
so we have:
I'd like to show you that the found model (x1, x2) = (0.0, 0.0)
is a solution to the delta-weakening of the original problem. FYI, here is the delta-weakening of the original problem where delta is 0.001.
When x1, x2 = 0.0, 0.0
, we have:
You can check that all of these conjuncts are true. So this is a delta-sat solution.
Reference:
Delta-Decidability over the Reals [arXiv] Sicun Gao, Jeremy Avigad, and Edmund Clarke LICS (Logic in Computer Science) 2012
Hello everyone,
Consider the following Code:
The result should be false, because the formula f is not satisfiable, but the result is true. If I print the result from the box, I get the following:
But this should not be an appropriate result.
Maybe the Issue #304 has something to do with the result as well.
Thank you in advance.