From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 19 Jan 2022 22:36:08 +0000 (-0800)
Subject: Fix a subtle issue with double negations in coverings proof (#7967)
X-Git-Tag: cvc5-1.0.0~525
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d9d3f84a5036a0254b00e99ebe00b5fad85b14b;p=cvc5.git

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.
---

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)