mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-15 21:19:22 -08:00
parent c3f67f3b5f
commit c3364f17fa
1 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_str.cpp
View file

@ -4652,15 +4652,17 @@ namespace smt {
expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
theory_var curr = m_find.find(get_var(n)); theory_var curr = m_find.find(get_var(n));
theory_var first = curr; theory_var first = curr;
do { if (curr != null_theory_var) {
expr* a = get_ast(curr); do {
if (u.str.is_string(a)) { expr* a = get_ast(curr);
hasEqcValue = true; if (u.str.is_string(a)) {
return a; hasEqcValue = true;
return a;
}
curr = m_find.next(curr);
} }
curr = m_find.next(curr); while (curr != first && curr != null_theory_var);
} }
while (curr != first && curr != null_theory_var);
hasEqcValue = false; hasEqcValue = false;
return n; return n;
} }