diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index a9910852e..5cb300725 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1806,6 +1806,8 @@ namespace sat {
     */
     bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) {
         CTRACE("resolve_bug", !c1.contains(l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";);
+        if (m_visited.size() <= 2*s.num_vars())
+            m_visited.resize(2*s.num_vars(), false);
         SASSERT(c1.contains(l));
         SASSERT(c2.contains(~l));
         bool res = true;
@@ -1825,6 +1827,10 @@ namespace sat {
             literal l2 = c2[i];
             if (not_l == l2)
                 continue;
+            if ((~l2).index() >= m_visited.size()) {
+                s.display(std::cout << l2 << " " << s.num_vars() << " " << m_visited.size() << "\n");
+                exit(0);
+            }
             if (m_visited[(~l2).index()]) {
                 res = false;
                 break;