fix for bug 429

* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index fbaef61f2a8128e01573198ec8c83c01dbbe930d..b5d524c31a6d34ebb77720251773433af3e2679c 100644 (file)
--- 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 ca86f920d5111ec08076e57fab647a5e7bb39c1b..335b7d81863d413936bf16468b1a45c3428cbfe4 100644 (file)
--- 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 4989b925025b7af0ede061b42d8f87fb19a12072..06a22458cb503cc1ae97a6f8a22882c26fab28aa 100644 (file)
--- 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 39db126d0a2cb936a92f3ebe18096320f48facc9..74547db910110a5df5cc251d5f0e0f67036e098c 100644 (file)
--- 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)