From 8d9d3f84a5036a0254b00e99ebe00b5fad85b14b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 19 Jan 2022 14:36:08 -0800 Subject: [PATCH] Fix a subtle issue with double negations in coverings proof (#7967) When the coverings solver finds a conflict that consists only of a single negated assertion, the way we constructed the lemma would silently drop the double negation. While this is not a problem by itself, the generated proof is out of sync then. This PR makes sure the double negation stays in place and is only removed by rewriting in the core lemma processing. Fixes cvc5/cvc5-projects#430. --- src/theory/arith/nl/cad_solver.cpp | 2 +- test/regress/CMakeLists.txt | 1 + .../proj-issue430-coverings-double-negation.smt2 | 16 ++++++++++++++++ 3 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/proofs/proj-issue430-coverings-double-negation.smt2 diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 7ecbccf6d..18071f3b2 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -137,7 +137,7 @@ void CadSolver::checkFull() Trace("nl-cad") << "UNSAT with MIS: " << mis << std::endl; d_eqsubs.postprocessConflict(mis); Trace("nl-cad") << "After postprocessing: " << mis << std::endl; - Node lem = NodeManager::currentNM()->mkAnd(mis).negate(); + Node lem = NodeManager::currentNM()->mkAnd(mis).notNode(); ProofGenerator* proof = d_CAC.closeProof(mis); d_im.addPendingLemma(lem, InferenceId::ARITH_NL_CAD_CONFLICT, proof); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1d0f1f276..1358f7dc7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -894,6 +894,7 @@ set(regress_0_tests regress0/proofs/project-issue330-eqproof.smt2 regress0/proofs/proj-issue326-nl-bounds-check.smt2 regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2 + regress0/proofs/proj-issue430-coverings-double-negation.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-issue430-coverings-double-negation.smt2 b/test/regress/regress0/proofs/proj-issue430-coverings-double-negation.smt2 new file mode 100644 index 000000000..2fe632e3a --- /dev/null +++ b/test/regress/regress0/proofs/proj-issue430-coverings-double-negation.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --check-proofs +; EXPECT: unsat +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) +(assert (> 0.0 (+ 1 (* x (+ 1 x))))) +(check-sat) + +(reset) + +(set-logic QF_NRA) +(declare-fun skoD () Real) +(declare-fun skoY () Real) +(declare-fun skoX () Real) +(assert (not (<= (* skoY (+ (+ 2 (* skoD 2)) (* skoY (- 1)))) (+ (+ 1 (* skoD (+ 2 skoD))) (* skoX skoX))))) +(check-sat) -- 2.30.2