diff options
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 16 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/arith_lra_01.smt2 | 19 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/arith_lra_02.smt2 | 20 |
4 files changed, 47 insertions, 12 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index fbaef61f2..b5d524c31 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -265,11 +265,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) PROOF( ProofManager::getSatProof()->registerUnitClause(ps[0], true); ) - if(assertionLevel > 0) { - // remember to unset it on user pop - Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl; - trail_user.push(ps[0]); - } return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); } else return ok; } else { @@ -686,6 +681,11 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) // Enqueue to the theory proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); } + if (from == CRef_Undef) { + if (assertionLevel > 0) { + trail_user.push(p); + } + } } @@ -1620,12 +1620,6 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; uncheckedEnqueue(lemma[0], lemma_ref); - if(lemma.size() == 1 && assertionLevel > 0) { - assert(decisionLevel() == 0); - // remember to unset it on user pop - Debug("minisat") << "got new unit (survived downward during updateLemmas()) " << lemma[0] << " at assertion level " << assertionLevel << std::endl; - trail_user.push(lemma[0]); - } } } } diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index ca86f920d..335b7d818 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -32,7 +32,9 @@ BUG_TESTS = \ bug233.cvc \ bug326.smt2 \ bug394.smt2 \ - bug396.smt2 + bug396.smt2 \ + arith_lra_01.smt2 \ + arith_lra_02.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/arith_lra_01.smt2 b/test/regress/regress0/push-pop/arith_lra_01.smt2 index 4989b9250..06a22458c 100644 --- a/test/regress/regress0/push-pop/arith_lra_01.smt2 +++ b/test/regress/regress0/push-pop/arith_lra_01.smt2 @@ -1,3 +1,22 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 (set-logic QF_LRA) (declare-fun x0 () Real) (declare-fun x1 () Real) diff --git a/test/regress/regress0/push-pop/arith_lra_02.smt2 b/test/regress/regress0/push-pop/arith_lra_02.smt2 index 39db126d0..74547db91 100644 --- a/test/regress/regress0/push-pop/arith_lra_02.smt2 +++ b/test/regress/regress0/push-pop/arith_lra_02.smt2 @@ -1,3 +1,23 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 (set-logic QF_LRA) (declare-fun x0 () Real) (declare-fun x1 () Real) |