From c3364f17fa5058903ce4e606da21a9d0e781d23a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 21:19:22 -0800 Subject: [PATCH] fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 17f889946..2ed8c578f 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4652,15 +4652,17 @@ namespace smt { expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { theory_var curr = m_find.find(get_var(n)); theory_var first = curr; - do { - expr* a = get_ast(curr); - if (u.str.is_string(a)) { - hasEqcValue = true; - return a; - } - curr = m_find.next(curr); - } - while (curr != first && curr != null_theory_var); + if (curr != null_theory_var) { + do { + expr* a = get_ast(curr); + if (u.str.is_string(a)) { + hasEqcValue = true; + return a; + } + curr = m_find.next(curr); + } + while (curr != first && curr != null_theory_var); + } hasEqcValue = false; return n; }