From 2e6ae8cfd24bea46bbc9c2fd54ce7eb611d12caa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 15 Nov 2017 23:06:05 -0800
Subject: [PATCH] fix crash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_str.cpp | 15 ++++++++-------
 src/smt/theory_str.h   |  2 +-
 src/util/union_find.h  |  1 +
 3 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 2ed8c578f..ed926a50d 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -63,8 +63,8 @@ namespace smt {
         cacheHitCount(0),
         cacheMissCount(0),
         m_fresh_id(0),
-        m_find(*this),
-        m_trail_stack(*this)
+        m_trail_stack(*this),
+        m_find(*this)
     {
         initialize_charset();
     }
@@ -281,7 +281,7 @@ namespace smt {
         } else {
             theory_var v = theory::mk_var(n);
             m_find.mk_var();
-            TRACE("str", tout << "new theory var v#" << v << std::endl;);
+            TRACE("str", tout << "new theory var v#" << v << " find " << m_find.find(v) << std::endl;);
             get_context().attach_th_var(n, this, v);
             get_context().mark_as_relevant(n);
             return v;
@@ -1905,8 +1905,8 @@ namespace smt {
 
     // support for user_smt_theory-style EQC handling
 
-    app * theory_str::get_ast(theory_var i) {
-        return get_enode(i)->get_owner();
+    app * theory_str::get_ast(theory_var v) {
+        return get_enode(v)->get_owner();
     }
 
     theory_var theory_str::get_var(expr * n) const {
@@ -4650,9 +4650,10 @@ namespace smt {
     // We only check m_find for a string constant.
 
     expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
-        theory_var curr = m_find.find(get_var(n));
-        theory_var first = curr;
+        theory_var curr = get_var(n);
         if (curr != null_theory_var) {
+            curr = m_find.find(curr);
+            theory_var first = curr;
             do {
                 expr* a = get_ast(curr);
                 if (u.str.is_string(a)) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index b478808d2..03fd31162 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -362,8 +362,8 @@ protected:
     // cache mapping each string S to Length(S)
     obj_map<expr, app*> length_ast_map;
 
-    th_union_find m_find;
     th_trail_stack m_trail_stack;
+    th_union_find m_find;
     theory_var get_var(expr * n) const;
     expr * get_eqc_next(expr * n);
     app * get_ast(theory_var i);
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 7a99b149e..416b653af 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -102,6 +102,7 @@ public:
 
     unsigned find(unsigned v) const {
         while (true) {
+            SASSERT(v < m_find.size());
             unsigned new_v = m_find[v];
             if (new_v == v)
                 return v;