From 1061cdf58ab4f3a95675fc13530df3b1aa259136 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 22 Sep 2016 15:40:43 -0400 Subject: [PATCH] fix value tester theory var reuse in theory_str fixes release regression in charAt-007 --- src/smt/theory_str.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 59db86212..ab6a9f229 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8131,6 +8131,7 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, if (!anEqcHasValue) { TRACE("t_str_detail", tout << "value tester " << mk_ismt2_pp(aTester, m) << " doesn't have an equivalence class value." << std::endl;); + refresh_theory_var(aTester); expr * makeupAssert = gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i); @@ -8147,6 +8148,7 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, expr * valTester = NULL; if (i + 1 < testerTotal) { valTester = fvar_valueTester_map[freeVar][len][i + 1].second; + refresh_theory_var(valTester); } else { valTester = mk_internal_valTest_var(freeVar, len, i + 1); valueTester_fvar_map[valTester] = freeVar;