From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 20:36:36 +0000 (-0600)
Subject: Fix incorrect assertion in prop engine proofs (#8204)
X-Git-Tag: cvc5-1.0.0~342
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=edfcb4be0617bd28eb9379d8bfe49524ecde3ec1;p=cvc5.git

Fix incorrect assertion in prop engine proofs (#8204)

Leftover from when unsat cores mode was tied to proof mode.

Fixes cvc5/cvc5-projects#462.
---

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c14b0183d..bf9a80008 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -225,8 +225,8 @@ void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
   Node node = trn.getNode();
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
   bool negated = trn.getKind() == TrustNodeKind::CONFLICT;
-  Assert(!isProofEnabled() || trn.getGenerator() != nullptr
-         || options().smt.unsatCores);
+  // should have a proof generator if the theory engine is proof producing
+  Assert(!d_env.isTheoryProofProducing() || trn.getGenerator() != nullptr);
   assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
 }
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cc52cc126..6bafac256 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -933,6 +933,7 @@ set(regress_0_tests
   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/proj-issue462-sat-proof-option.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-issue462-sat-proof-option.smt2 b/test/regress/regress0/proofs/proj-issue462-sat-proof-option.smt2
new file mode 100644
index 000000000..2f04d62fa
--- /dev/null
+++ b/test/regress/regress0/proofs/proj-issue462-sat-proof-option.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(set-option :global-declarations true)
+(set-option :proof-mode sat-proof)
+(declare-const _x3 Int)
+(assert (>= (str.to_code (str.from_code _x3)) _x3))
+(check-sat)