diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-29 15:37:39 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-29 22:37:39 +0000 |
| commit | e86e6c20286af0eece976e7560b3dc400384f9c7 (patch) | |
| tree | 73bfed2f763edbbb2e94d3e798f2f9aa9fd45353 /test | |
| parent | 9642be1703c26e76ab5144a4993814fdb804a9b8 (diff) | |
Fix proof of nl lemma for a corner case (#7530)
This PR fixes the proof generated for the nonlinear monomial bounds check lemmas. In some cases, it implies an equality (multiplied by a monomial) not from the equality but from the two weak inequalities. We now properly detect this special case and add a rather involved proof.
Fixes cvc5/cvc5-projects#326.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 | 13 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c6dcfa967..6df6ebe76 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -867,6 +867,7 @@ set(regress_0_tests regress0/proofs/open-pf-rederivation.smt2 regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 regress0/proofs/project-issue330-eqproof.smt2 + regress0/proofs/proj-issue326-nl-bounds-check.smt2 regress0/proofs/qgu-fuzz-1-bool-sat.smt2 regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 diff --git a/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 new file mode 100644 index 000000000..bc10e9cac --- /dev/null +++ b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 @@ -0,0 +1,13 @@ +; EXPECT: unknown +(set-logic ALL) +(set-option :check-proofs true) +(set-option :proof-check eager) +(declare-const x Real) +(assert + (and + (< 1.0 x) + (<= x (/ 0.0 0.0 x)) + (<= (/ 0.0 0.0 x) x) + ) +) +(check-sat) |