mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
enable pb theory always as pb terms can be introduced during transformations. Issue #884
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
256a0e2d82
commit
9cfd412cd0
|
@ -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() {
|
||||
|
|
|
@ -154,7 +154,6 @@ namespace sat {
|
|||
if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
|
||||
return;
|
||||
|
||||
|
||||
initialize();
|
||||
|
||||
CASSERT("sat_solver", s.check_invariant());
|
||||
|
|
Loading…
Reference in a new issue