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 7ecbccf6db8b7bcbd400729f8b02955cfa6d495a..18071f3b216ed77886c47cf9c84d4cfad3d61222 100644 (file)
--- 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 1d0f1f2768ab2995b3d14564a72196ce3cb9262c..1358f7dc774e5df4f4baafdd1afcc6c7e0f4f5a4 100644 (file)
--- 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 (file)
index 0000000..2fe632e
--- /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)