mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
don't pretend to handle new operators #4387
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e525543bd0
commit
7f22eb594e
|
@ -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<context, expr*>(m_unhandled_expr));
|
||||
m_unhandled_expr = n;
|
||||
|
|
Loading…
Reference in a new issue