From edfcb4be0617bd28eb9379d8bfe49524ecde3ec1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Mar 2022 14:36:36 -0600 Subject: [PATCH] Fix incorrect assertion in prop engine proofs (#8204) Leftover from when unsat cores mode was tied to proof mode. Fixes cvc5/cvc5-projects#462. --- src/prop/prop_engine.cpp | 4 ++-- test/regress/CMakeLists.txt | 1 + .../regress0/proofs/proj-issue462-sat-proof-option.smt2 | 9 +++++++++ 3 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/proofs/proj-issue462-sat-proof-option.smt2 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) -- 2.30.2