mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

fix #4389 fix #4859

Browse source 
The bugs are duplicates
This commit is contained in:
Nikolaj Bjorner 2020-12-07 14:57:50 -08:00
parent 409414c5b3
commit 9f6a0a868a
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/opt/opt_context.cpp
View file

@ -820,7 +820,14 @@ namespace opt {
mk_simplify_tactic(m));
opt_params optp(m_params);
tactic_ref tac1, tac2, tac3, tac4;
if (optp.elim_01() && m_logic.is_null()) {
bool has_dep = false;
for (unsigned i = 0; !has_dep && i < g->size(); ++i) {
ptr_vector<expr> deps;
expr_dependency_ref core(g->dep(i), m);
m.linearize(core, deps);
has_dep |= !deps.empty();
}
if (optp.elim_01() && m_logic.is_null() && !has_dep) {
tac1 = mk_dt2bv_tactic(m);
tac2 = mk_lia2card_tactic(m);
tac3 = mk_eq2bv_tactic(m);