From 7f22eb594e437a4bcb5845b5f21b475893ea3a03 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 May 2020 20:04:43 -0700 Subject: [PATCH] don't pretend to handle new operators #4387 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2bf867cc0..4f376c9c6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3279,7 +3279,10 @@ 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_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)) { if (!m_unhandled_expr) { ctx.push_trail(value_trail(m_unhandled_expr)); m_unhandled_expr = n;