diff options
| -rw-r--r-- | src/prop/sat_proof_manager.cpp | 15 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2 | 31 |
3 files changed, 44 insertions, 5 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index ad23bedc9..8891016a4 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -305,11 +305,19 @@ void SatProofManager::processRedundantLit( printClause(reason); Trace("sat-proof") << "\n"; } - // check if redundant literals in the reason. The first literal is the one we - // will be eliminating, so we check the others + // Since processRedundantLit calls can reallocate memory in the SAT solver due + // to explaining stuff, we directly get the literals and the clause node here + std::vector<SatLiteral> toProcess; for (unsigned i = 1, size = reason.size(); i < size; ++i) { - SatLiteral satLit = MinisatSatSolver::toSatLiteral(reason[i]); + toProcess.push_back(MinisatSatSolver::toSatLiteral(reason[i])); + } + Node clauseNode = getClauseNode(reason); + // check if redundant literals in the reason. The first literal is the one we + // will be eliminating, so we check the others + for (unsigned i = 0, size = toProcess.size(); i < size; ++i) + { + SatLiteral satLit = toProcess[i]; // if literal does not occur in the conclusion we process it as well if (!conclusionLits.count(satLit)) { @@ -325,7 +333,6 @@ void SatProofManager::processRedundantLit( // reason, not only with ~lit, since the learned clause is built under the // assumption that the redundant literal is removed via the resolution with // the explanation of its negation - Node clauseNode = getClauseNode(reason); Node litNode = d_cnfStream->getNodeCache()[lit]; bool negated = lit.isNegated(); Assert(!negated || litNode.getKind() == kind::NOT); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 17585d363..d1208ad0f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2110,7 +2110,7 @@ set(regress_1_tests regress1/strings/bug686dd.smt2 regress1/strings/bug768.smt2 regress1/strings/bug799-min.smt2 - regress1/strings/cee-norn-aes-trivially.smt2 + regress1/strings/cee-norn-aes-trivially.smt2 regress1/strings/chapman150408.smt2 regress1/strings/cmu-2db2-extf-reg.smt2 regress1/strings/cmu-5042-0707-2.smt2 @@ -2509,6 +2509,7 @@ set(regress_2_tests regress2/ooo.rf6.smt2 regress2/ooo.tag10.smt2 regress2/piVC_5581bd.smt2 + regress2/proofs/sat-proof-reloaded-reason.smt2 regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 regress2/quantifiers/cee-event-wrong-sat.smt2 diff --git a/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2 b/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2 new file mode 100644 index 000000000..8bc990b8b --- /dev/null +++ b/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --produce-proofs +; EXPECT: sat +; +; This is a benchmark exercising a dangerous behavior in SAT proofs +; where while eliminating redundant literals new clauses are added to +; the SAT solver and the reference to the reason of a literal could be +; lost. + +(set-logic QF_SLIA) +(declare-const x Int) +(declare-const x2 Int) +(declare-const x22 Int) +(declare-const x1 Int) +(declare-fun s () String) +(assert (not (= "0" (str.substr s (+ 1 1 1 1) 1)))) +(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1) (+ 1 1)))))) +(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))) (and (> (str.len (str.substr s (+ 1 1 1) (str.len s))) 1) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1 1 1 1) (- (str.len s) 1)) 1 1))) false true)) (= 1 (str.to_int (str.substr s x22 1))))) +(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) false true) (= 0 (str.to_int (str.substr s (+ 1 1) (+ 1 1)))))) +(assert (<= (ite (str.prefixof "-" (str.substr s 0 1)) (str.to_int (str.substr (str.substr s (+ 1 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s (+ 1 1 1) (+ 1 1 1))) 1))) (str.to_int (str.substr s 0 x2))) 0)) +(assert (ite (str.prefixof "-" (str.substr s 0 1)) (and (> (str.len (str.substr s 0 (+ 1 1))) 1) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1))))) true)) +(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1))))))) +(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1)))) true (= 1 (str.to_int (str.substr s (+ 1 1 1 1) 1))))) +(assert (= 1 (str.len (str.substr s (+ 1 1 1) 1)))) +(assert (not (= 1 (str.len (str.substr s 1 (+ 1 1 1)))))) +(assert (> (- (str.len s) 1 (+ 1 1) (+ 1 1)) 0)) +(assert (= "0" (str.substr s 1 1))) +(assert (not (<= (str.to_int (str.substr s x x1)) 0))) +(assert (not (= 1 (str.len (str.substr s (+ 1 1) (- (+ 1 1 1) 1)))))) +(assert (str.in_re s (re.+ (re.range "0" "9")))) +(assert (not (<= (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) 1)) (- (str.to_int (str.substr (str.substr s (+ 1 1 1 1) (+ 1 1)) 1 (- (str.len (str.substr s (+ 1 1) (+ 1 1))) 1)))) (str.to_int (str.substr s (+ 1 1 1 1) (+ 1 1)))) 1))) +(check-sat) |