From 9cfd412cd0f2fbc389eaed51cc585604304f143e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2017 15:28:29 -0800 Subject: [PATCH] enable pb theory always as pb terms can be introduced during transformations. Issue #884 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 8 ++++---- src/sat/sat_simplifier.cpp | 1 - 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 46122d619..56b152caa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -570,11 +570,11 @@ namespace opt { m_opt_solver = alloc(opt_solver, m, m_params, m_fm); m_opt_solver->set_logic(m_logic); m_solver = m_opt_solver.get(); + m_opt_solver->ensure_pb(); - if (opt_params(m_params).priority() == symbol("pareto") || - (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) { - m_opt_solver->ensure_pb(); - } + //if (opt_params(m_params).priority() == symbol("pareto") || + // (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) { + //} } void context::setup_arith_solver() { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 62fb99a11..bd975115b 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -154,7 +154,6 @@ namespace sat { if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) return; - initialize(); CASSERT("sat_solver", s.check_invariant());