From 2d409c6042318e74d6d1b8adfc5c36225b53a691 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@hotmail.com>
Date: Fri, 29 May 2015 14:32:24 -0700
Subject: [PATCH] revert bug introduced to avoid stack overflow in arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
---
 src/smt/theory_array_full.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index f2d1527c0..4e169a8be 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -785,7 +785,10 @@ namespace smt {
         else {
             m_eqs.insert(v1, v2, true);
             literal eq(mk_eq(v1, v2, true));
-            m_eqsv.push_back(eq);
+            get_context().mark_as_relevant(eq);            
+            assert_axiom(eq);
+
+            // m_eqsv.push_back(eq);
             return true;
         }
     }