diff --git a/src/ast/rewriter/seq_regex_bisim.cpp b/src/ast/rewriter/seq_regex_bisim.cpp index 5e849017c7..9e1a8e4986 100644 --- a/src/ast/rewriter/seq_regex_bisim.cpp +++ b/src/ast/rewriter/seq_regex_bisim.cpp @@ -102,9 +102,7 @@ namespace seq { expr* e = work.back(); work.pop_back(); expr* c = nullptr, * t = nullptr, * f = nullptr; - if (m.is_ite(e, c, t, f) || - m_util.re.is_union(e, t, f) || - m_util.re.is_antimirov_union(e, t, f)) { + if (m.is_ite(e, c, t, f)) { if (seen.insert_if_not_there(t)) work.push_back(t); if (seen.insert_if_not_there(f)) diff --git a/src/test/main.cpp b/src/test/main.cpp index b10446aa92..6314296e46 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -114,7 +114,6 @@ X(api_special_relations) \ X(arith_rewriter) \ X(range_predicate) \ - X(range_predicate_translator) \ X(regex_range_collapse) \ X(check_assumptions) \ X(smt_context) \