mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
temporarily disable elim_pure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c75a57731f
commit
ca25e482e5
|
@ -2991,7 +2991,7 @@ namespace sat {
|
|||
init_use_lists();
|
||||
remove_unused_defs();
|
||||
set_non_external();
|
||||
if (get_config().m_elim_vars && !s().get_config().m_incremental && !s().tracking_assumptions()) elim_pure();
|
||||
//if (get_config().m_elim_vars && !s().get_config().m_incremental && !s().tracking_assumptions()) elim_pure();
|
||||
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
|
||||
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
|
||||
unit_strengthen();
|
||||
|
|
Loading…
Reference in a new issue