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<sat::literal_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);