From 8ca2de41db79a266b58124c4849fd61d4a8f6c1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Feb 2021 09:59:21 -0800 Subject: [PATCH] turn on from/to code handling #5007 samples --- src/smt/theory_seq.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 6fb4b3128..ca3efa157 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3099,8 +3099,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_from_code(n) || + // m_util.str.is_to_code(n) || m_util.str.is_is_digit(n)) { add_unhandled_expr(n); }