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

z3str3: missed instance of rewrite-then-assert

Browse source
This commit is contained in:
Murphy Berzish 2019-12-04 16:41:51 -05:00 • committed by Nikolaj Bjorner
parent 7e415c1b69
commit 32e5c6ffd1
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -3638,7 +3638,7 @@ namespace smt {
expr_ref conclusion(mk_or(arrangement_disjunction), mgr);
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom(premise, conclusion), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(premise, conclusion);
}