From baf045ed88c2f72f435547e2de6424992b8c0810 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Wed, 24 Oct 2012 19:41:33 +0000
Subject: [PATCH] fix for bug 429 * not all asserted units were tracked in the
 user trail, moved the tracking into uncheckedEnqueue

---
 src/prop/minisat/core/Solver.cc               | 16 +++++----------
 test/regress/regress0/push-pop/Makefile.am    |  4 +++-
 .../regress0/push-pop/arith_lra_01.smt2       | 19 ++++++++++++++++++
 .../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)
-- 
2.30.2