mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
fix #5491
This commit is contained in:
parent
15e3e81cb5
commit
aa05298950
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue