From 2bd8d3b4852765cdd92abd7db6331fc5bac8fb5d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Jul 2019 10:27:47 +0800
Subject: [PATCH] fixes for input4/5 #2416

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp | 14 +++++++++-----
 src/sat/ba_solver.h   |  1 +
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 2de772b55..f59cff770 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -3159,14 +3159,18 @@ namespace sat {
     // -------------------------------
     // set literals equivalent
 
-    bool ba_solver::set_root(literal l, literal r) { 
-        if (s().is_assumption(l.var())) {
-            return false;
-        }
+    void ba_solver::reserve_roots() {
         m_root_vars.reserve(s().num_vars(), false);
         for (unsigned i = m_roots.size(); i < 2 * s().num_vars(); ++i) {
             m_roots.push_back(to_literal(i));
         }
+    }
+
+    bool ba_solver::set_root(literal l, literal r) { 
+        if (s().is_assumption(l.var())) {
+            return false;
+        }
+        reserve_roots();
         m_roots[l.index()] = r;
         m_roots[(~l).index()] = ~r;
         m_root_vars[l.var()] = true;
@@ -3175,7 +3179,7 @@ namespace sat {
 
     void ba_solver::flush_roots() {
         if (m_roots.empty()) return;
-
+        reserve_roots();
         // validate();
         m_visited.resize(s().num_vars()*2, false);
         m_constraint_removed = false;
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index cbbd49ebe..4fc439d71 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -328,6 +328,7 @@ namespace sat {
         void update_psm(constraint& c) const;
         void mutex_reduction();
         void update_pure();
+        void reserve_roots();
 
         unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); }