From 50353168ef008a87bc38d37de305bfdfe43627e1 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 14 Sep 2016 15:36:36 -0400
Subject: [PATCH] fix semantics of get_concats_in_eqc and get_var_in_eqc

---
 src/smt/theory_str.cpp | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index ce5aabb6c..a773e0d6d 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8649,9 +8649,7 @@ void theory_str::get_concats_in_eqc(expr * n, std::set<expr*> & concats) {
         if (is_concat(to_app(eqcNode))) {
             concats.insert(eqcNode);
         }
-        enode * e_eqc = ctx.get_enode(eqcNode);
-        eqcNode = e_eqc->get_next()->get_owner();
-        // eqcNode = Z3_theory_get_eqc_next(t, eqcNode);
+        eqcNode = get_eqc_next(eqcNode);
     } while (eqcNode != n);
 }
 
@@ -8663,9 +8661,7 @@ void theory_str::get_var_in_eqc(expr * n, std::set<expr*> & varSet) {
 		if (variable_set.find(eqcNode) != variable_set.end()) {
 			varSet.insert(eqcNode);
 		}
-		enode * e_eqc = ctx.get_enode(eqcNode);
-		eqcNode = e_eqc->get_next()->get_owner();
-		// eqcNode = Z3_theory_get_eqc_next(t, eqcNode);
+		eqcNode = get_eqc_next(eqcNode);
 	} while (eqcNode != n);
 }