From 447c6e4ce362a71f2c2b31f1a1eff7a2a4b91213 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 20 Sep 2016 00:28:29 -0400
Subject: [PATCH] refresh length tester in
 theory_str::gen_len_val_options_for_free_var fixes charAt-007.smt2

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 44a4b0d7c..9f0975609 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8786,6 +8786,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe
 			} else {
 			    // TODO make absolutely sure this is safe to do if 'indicator' is technically out of scope
 				indicator = fvar_lenTester_map[freeVar][i];
+				refresh_theory_var(indicator);
 				testNum = i + 1;
 			}
 			expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);