mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

z3str3: rewrite strong arrangement axiom to avoid assertion violation

Browse source
This commit is contained in:
Murphy Berzish 2019-11-28 12:36:49 -05:00 • committed by Nikolaj Bjorner
parent a257ec0cc1
commit b8f2cf5b0b
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_str.cpp
View file

@ -4184,6 +4184,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, mk_and(r_items)), mgr);
ctx.get_rewriter()(ax_strong);
assert_axiom(ax_strong);
} else {
assert_implication(ax_l, mk_and(r_items));