From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 22 Oct 2021 18:08:33 +0000 (-0700)
Subject: Make CAD proofs user context dependent (#7466)
X-Git-Tag: cvc5-1.0.0~1004
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b7b6fb608a897bf50861ce5a4c25e74c9245f01;p=cvc5.git

Make CAD proofs user context dependent (#7466)

Given that arithmetic lemmas can survive the current (sat) context by being buffered in the inference manager, their proofs need to do as well. This PR changes the CAD proofs to be user context dependent.

Fixes cvc5/cvc5-projects#315.
---

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index ecb62b554..d259bc096 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -47,7 +47,7 @@ CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering)
   if (d_env.isTheoryProofProducing())
   {
     d_proof.reset(
-        new CADProofGenerator(context(), d_env.getProofNodeManager()));
+        new CADProofGenerator(userContext(), d_env.getProofNodeManager()));
   }
 }
 
diff --git a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
index 76898e07d..ccb50c55d 100644
--- a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
+++ b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
@@ -2,6 +2,7 @@
 ; COMMAND-LINE: --theoryof-mode=term --nl-icp
 ; EXPECT: unknown
 (set-logic QF_NRA)
+(set-option :check-proofs true)
 (declare-fun x () Real)
 (declare-fun y () Real)
 (assert (and (< 1 y) (= y (+ x (* x x)))))