From 804009a75754864c26e19adffdefc0d31c4016cd Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 14 Sep 2016 15:37:48 -0400
Subject: [PATCH] use z3str2 eqc semantics for get_eqc_value

---
 src/smt/theory_str.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index a773e0d6d..c3c8a50cf 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -3967,6 +3967,7 @@ void theory_str::unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr) {
  * Return that constant if it is found, and set hasEqcValue to true.
  * Otherwise, return n, and set hasEqcValue to false.
  */
+/*
 expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
 	context & ctx = get_context();
 	// I hope this works
@@ -3985,6 +3986,12 @@ expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
 	hasEqcValue = false;
 	return n;
 }
+*/
+
+expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
+    return z3str2_get_eqc_value(n, hasEqcValue);
+}
+
 
 // Simulate the behaviour of get_eqc_value() from Z3str2.
 // We only check m_find for a string constant.