From a51201298c2016fb4ed67372ccce84c26a797fd8 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 4 Mar 2016 14:42:38 +0000
Subject: [PATCH] Bugfix for assumptions in inc_sat_solver

---
 src/sat/sat_solver/inc_sat_solver.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 1c156d83e..7feed9fb1 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -151,6 +151,7 @@ public:
         lbool r = internalize_formulas();
         if (r != l_true) return r;
         r = internalize_assumptions(sz, assumptions, dep2asm);
+        SASSERT(sz == m_asms.size());
         if (r != l_true) return r;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
@@ -300,6 +301,7 @@ private:
 
     lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
         if (sz == 0) {
+            m_asms.shrink(0);
             return l_true;
         }
         goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
@@ -331,6 +333,7 @@ private:
         sat::literal lit;
         for (unsigned i = 0; i < sz; ++i) {
             if (dep2asm.find(asms[i], lit)) {
+                SASSERT(lit.var() <= m_solver.num_vars());
                 m_asms.push_back(lit);
                 if (i != j && !m_weights.empty()) {
                     m_weights[j] = m_weights[i];