From ca25e482e53f739aa374f531d9c4b0c86df7551c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jul 2019 19:01:23 -0700 Subject: [PATCH] temporarily disable elim_pure Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index eaa088e85..63387c866 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -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();