fix #4389 fix #4859

The bugs are duplicates
Z3Prover · Dec 7, 2020 · 9f6a0a8 · 9f6a0a8
1 parent 409414c
commit 9f6a0a8
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
@@ -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);