mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity

refresh length tester in theory_str::gen_len_val_options_for_free_var

Browse source 
fixes charAt-007.smt2
This commit is contained in:
Murphy Berzish 2016-09-20 00:28:29 -04:00
parent f1d7ffcdce
commit 447c6e4ce3
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_str.cpp
View file

@ -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);