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 c14b0183dc65c7a972c918f68fc2930103293a5e..bf9a80008eb4861ea95758efe398cb49452b282c 100644 (file)
--- 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 cc52cc126b4f034308e9efef41f8ac0ed3fa550e..6bafac256015ba575a9481fa39eaf2f51bfa2297 100644 (file)
--- 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 (file)
index 0000000..2f04d62
--- /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)