From e86e6c20286af0eece976e7560b3dc400384f9c7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 29 Oct 2021 15:37:39 -0700 Subject: 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. --- test/regress/CMakeLists.txt | 1 + .../regress0/proofs/proj-issue326-nl-bounds-check.smt2 | 13 +++++++++++++ 2 files changed, 14 insertions(+) create mode 100644 test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 (limited to 'test') 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) -- cgit v1.2.3