fix #5491

Z3Prover · Aug 20, 2021 · aa05298 · aa05298
1 parent 15e3e81
commit aa05298
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -3191,10 +3191,8 @@ void theory_seq::relevant_eh(app* n) {
 
     if (m_util.str.is_replace_all(n) ||
         m_util.str.is_replace_re(n) ||
-        m_util.str.is_replace_re_all(n) ||
-        // m_util.str.is_from_code(n) ||
-        // m_util.str.is_to_code(n) ||
-        m_util.str.is_is_digit(n)) {
+        m_util.str.is_replace_re_all(n)
+        ) {
         add_unhandled_expr(n);
     }
 }