From 1520760a04de41827bb177d2d67427033c9d2286 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Thu, 9 Jun 2016 20:31:21 -0400
Subject: [PATCH] string-integer integration in free var gen

---
 src/smt/theory_str.cpp | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index ba9b503be..f8366ed07 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -5302,13 +5302,12 @@ void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
 		}
 
 		if (standAlone) {
-			// TODO
-			// int lenValue = getLenValue(freeVar);
-			int lenValue = -1;
-			if (lenValue != -1) {
+		    rational len_value;
+		    bool len_value_exists = get_len_value(freeVar, len_value);
+			if (len_value_exists) {
 				leafVarSet.insert(freeVar);
 			} else {
-				aloneVars[lenValue].insert(freeVar);
+				aloneVars[-1].insert(freeVar);
 			}
 		} else {
 			leafVarSet.insert(freeVar);