From 0b7b6fb608a897bf50861ce5a4c25e74c9245f01 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 22 Oct 2021 11:08:33 -0700 Subject: [PATCH] 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. --- src/theory/arith/nl/cad/cdcac.cpp | 2 +- test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) 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& 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))))) -- 2.30.2