diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-15 14:08:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-15 19:08:03 +0000 |
| commit | 216f3c9fb07a08909942b91a2a4739cd178f5a72 (patch) | |
| tree | 00de2d826d1b4ad6124856536923a2463c4d8641 /test/regress/regress1/nl | |
| parent | 6cbb7824dabd7ab8e85472a22ba30ad2498afebc (diff) | |
Make nonlinear extension account for relevant term set (#6147)
This fixes a subtle issue with non-linear and theory combination.
It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.
In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.
Fixes #5662.
Diffstat (limited to 'test/regress/regress1/nl')
| -rw-r--r-- | test/regress/regress1/nl/issue5662-nl-tc-min.smt2 | 16 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue5662-nl-tc.smt2 | 17 |
2 files changed, 33 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 new file mode 100644 index 000000000..0e7279ef9 --- /dev/null +++ b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 @@ -0,0 +1,16 @@ +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun j () Real) +(declare-fun k () Real) +(declare-fun h () Real) +(assert (< 0 k)) +(assert (= 1 (* k j))) +(assert + (or + (= h 0) + (= 0.0 (* a k)) + ) +) +(assert (distinct a h)) +(check-sat) diff --git a/test/regress/regress1/nl/issue5662-nl-tc.smt2 b/test/regress/regress1/nl/issue5662-nl-tc.smt2 new file mode 100644 index 000000000..d805b721d --- /dev/null +++ b/test/regress/regress1/nl/issue5662-nl-tc.smt2 @@ -0,0 +1,17 @@ +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(declare-fun d () Real) +(declare-fun j () Real) +(declare-fun e () Real) +(declare-fun f () Real) +(declare-fun k () Real) +(declare-fun g () Real) +(declare-fun h () Real) +(assert (forall ((i Real)) (xor (and (or (and (or (and (or (and (or + (and (> 0.0 (* a e) (* c e)) (>= 0 k)) (<= g 0)) (= (* b j) + 2.0))))) (> f k)) (>= 0.0 k))) (>= 0 k)))) +(assert (distinct a (* d h))) +(check-sat) |