From 34dc65515041928c4ef5116871c959a55f42fc08 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 13 Sep 2016 18:24:59 -0400
Subject: [PATCH] z3str2 eqc semantics for theory_str unroll checks

---
 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 c3ae176b7..6d4fb1aab 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8883,9 +8883,7 @@ void theory_str::get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> &
         unrollFuncSet.insert(curr);
       }
     }
-    enode * e_curr = ctx.get_enode(curr);
-    curr = e_curr->get_next()->get_owner();
-    // curr = get_eqc_next(t, curr);
+    curr = get_eqc_next(curr);
   } while (curr != n);
 }
 
@@ -8907,9 +8905,7 @@ void theory_str::get_eqc_simpleUnroll(expr * n, expr * &constStr, std::set<expr*
 				}
 			}
 		}
-		enode * e_curr = ctx.get_enode(curr);
-		curr = e_curr->get_next()->get_owner();
-		// curr = get_eqc_next(t, curr);
+		curr = get_eqc_next(curr);
 	} while (curr != n);
 }