From 87d61d6d6ed4a685df7d0364e5f37f1297d54175 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 14 Sep 2016 15:35:37 -0400 Subject: [PATCH] fix semantics of in_same_eqc --- src/smt/theory_str.cpp | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 3727e15e1..ce5aabb6c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4178,22 +4178,13 @@ bool theory_str::in_same_eqc(expr * n1, expr * n2) { ctx.internalize(n2, false); } - enode * n1Node = ctx.get_enode(n1); - enode * n2Node = ctx.get_enode(n2); - - // here's what the old Z3str2 would have done; we can do something much better - /* - n1Node->get_root(); - enode * curr = n1Node->get_next(); - while (curr != n1Node) { - if (curr == n2Node) { + expr * curr = get_eqc_next(n1); + while (curr != n1) { + if (curr == n2) return true; - } - curr = curr->get_next(); + curr = get_eqc_next(curr); } return false; - */ - return n1Node->get_root() == n2Node->get_root(); } expr * theory_str::collect_eq_nodes(expr * n, expr_ref_vector & eqcSet) {