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 ecb62b55488daedd50a53c9e68b87542a5219475..d259bc0968425644983e04426a73c9c662bcca1e 100644 (file)
--- 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 76898e07d1b2218a24781ba6b86317ea402e8884..ccb50c55da0964c4877f14c898299bd7334abf14 100644 (file)
--- 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)))))