mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 23:33:41 +00:00
Code Activity

relax unhandled condition

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-14 14:58:43 -08:00
parent 49a0266c6a
commit 98db260a93
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/seq_regex.cpp
View file

@ -323,6 +323,7 @@ namespace smt {
literal is_nullable_lit = th.mk_literal(is_nullable); literal is_nullable_lit = th.mk_literal(is_nullable);
ctx.mark_as_relevant(is_nullable_lit); ctx.mark_as_relevant(is_nullable_lit);
th.add_axiom(~lit, ~len_s_le_i, is_nullable_lit); th.add_axiom(~lit, ~len_s_le_i, is_nullable_lit);
if (str().is_in_re(is_nullable))
th.add_unhandled_expr(is_nullable); th.add_unhandled_expr(is_nullable);
} }
} }