mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 13:47:01 +00:00
Code Activity

fix typo'ed set reference in handle_equality

Browse source
This commit is contained in:
Murphy Berzish 2016-09-13 18:16:21 -04:00
parent aea0032aa7
commit 8f636e1f57
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_str.cpp
View file

@ -6231,14 +6231,14 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) {
if (eqc_const_lhs.size() != 0) { if (eqc_const_lhs.size() != 0) {
expr * conStr = *(eqc_const_lhs.begin()); expr * conStr = *(eqc_const_lhs.begin());
std::set<expr*>::iterator itor2 = eqc_const_rhs.begin(); std::set<expr*>::iterator itor2 = eqc_concat_rhs.begin();
for (; itor2 != eqc_const_rhs.end(); itor2++) { for (; itor2 != eqc_concat_rhs.end(); itor2++) {
solve_concat_eq_str(*itor2, conStr); solve_concat_eq_str(*itor2, conStr);
} }
} else if (eqc_const_rhs.size() != 0) { } else if (eqc_const_rhs.size() != 0) {
expr* conStr = *(eqc_const_rhs.begin()); expr* conStr = *(eqc_const_rhs.begin());
std::set<expr*>::iterator itor1 = eqc_const_lhs.begin(); std::set<expr*>::iterator itor1 = eqc_concat_lhs.begin();
for (; itor1 != eqc_const_lhs.end(); itor1++) { for (; itor1 != eqc_concat_lhs.end(); itor1++) {
solve_concat_eq_str(*itor1, conStr); solve_concat_eq_str(*itor1, conStr);
} }
} }