mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

fix empty vector edge case in binary search

Browse source
This commit is contained in:
Murphy Berzish 2016-12-22 19:33:38 -05:00
parent 2dc9b486d3
commit 0a6c23148f
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -9229,7 +9229,7 @@ expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, bin
expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue) { expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
if (binary_search_len_tester_stack.contains(freeVar)) { if (binary_search_len_tester_stack.contains(freeVar) && !binary_search_len_tester_stack[freeVar].empty()) {
TRACE("t_str_binary_search", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl; TRACE("t_str_binary_search", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl;
for (ptr_vector<expr>::const_iterator it = binary_search_len_tester_stack[freeVar].begin(); for (ptr_vector<expr>::const_iterator it = binary_search_len_tester_stack[freeVar].begin();
it != binary_search_len_tester_stack[freeVar].end(); ++it) { it != binary_search_len_tester_stack[freeVar].end(); ++it) {