From 8f636e1f57be63f2cdb071b44fc7baae0d05e924 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 13 Sep 2016 18:16:21 -0400 Subject: [PATCH] fix typo'ed set reference in handle_equality --- src/smt/theory_str.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 939a63160..c3ae176b7 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6231,14 +6231,14 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { if (eqc_const_lhs.size() != 0) { expr * conStr = *(eqc_const_lhs.begin()); - std::set::iterator itor2 = eqc_const_rhs.begin(); - for (; itor2 != eqc_const_rhs.end(); itor2++) { + std::set::iterator itor2 = eqc_concat_rhs.begin(); + for (; itor2 != eqc_concat_rhs.end(); itor2++) { solve_concat_eq_str(*itor2, conStr); } } else if (eqc_const_rhs.size() != 0) { expr* conStr = *(eqc_const_rhs.begin()); - std::set::iterator itor1 = eqc_const_lhs.begin(); - for (; itor1 != eqc_const_lhs.end(); itor1++) { + std::set::iterator itor1 = eqc_concat_lhs.begin(); + for (; itor1 != eqc_concat_lhs.end(); itor1++) { solve_concat_eq_str(*itor1, conStr); } }