From eeb79e1c3c9343f3dcf7a5ec09c2e503abdeec6a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2017 19:30:54 -0700 Subject: [PATCH] update to retain original behavior Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 2 +- src/test/cnf_backbones.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1310727aa..d486dfd11 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -406,7 +406,7 @@ namespace opt { if (r == l_true && !get_lower_as_num(i).is_finite()) { return r; } - if (r == l_true && i + 1 < m_objectives.size()) { + if (r == l_true && i + 1 < m_objectives.size() && get_lower_as_num(i).is_finite()) { update_lower(); } } diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 07edabece..14fc594b6 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -252,12 +252,12 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { vector tracking_clauses; track_clauses(solver, solver2, assumptions, tracking_clauses); } - + // remove this line to limit variables to exclude assumptions + num_vars = g_solver->num_vars(); for (unsigned i = 1; i < num_vars; ++i) { vars.push_back(i); g_solver->set_external(i); } - num_vars = g_solver->num_vars(); lbool r; if (use_chunk) { r = core_chunking(*g_solver, vars, assumptions, conseq, 100);