diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-07 16:13:41 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-07 09:13:41 -0500 |
| commit | eb4321c5040258ac1ac41eb955aa5b6b5199011e (patch) | |
| tree | 01524ae48f79b8aa0ab60728e29e3a4b80e92e8f /test/regress/regress0 | |
| parent | 1a97c19443833604d57f1453a1bebfe0714d3d8e (diff) | |
Make sure conflicts are not rewritten (in arithmetic) (#5219)
The arithmetic inference manager did rewrite conflicts, which lead to nodes from the conflict not being assumptions (but rewritten assumptions) triggering an assertion. This rewrite is now removed.
Furthermore rewrites triggering the same assertion within the icp subsolver have been refactored to avoid this issue.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 new file mode 100644 index 000000000..3c8a949ad --- /dev/null +++ b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 @@ -0,0 +1,8 @@ +; REQUIRES: poly +; COMMAND-LINE: --theoryof-mode=term --nl-ext --nl-icp +; EXPECT: unknown +(set-logic QF_NRA) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (and (< 1 y) (= y (+ x (* x x))))) +(check-sat) |