diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 351141a3f..8ae4e467f 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -50,6 +50,7 @@ namespace opt {
         if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
             m_params.m_relevancy_lvl = 0;
         }
+        // m_params.m_auto_config = false;
     }
 
     unsigned opt_solver::m_dump_count = 0;
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 877d4f659..628eeea83 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -901,7 +901,7 @@ namespace smt {
         objective_term const& objective = m_objectives[v];
         has_shared = false;
         
-        IF_VERBOSE(1,
+        IF_VERBOSE(4,
                    for (unsigned i = 0; i < objective.size(); ++i) {
                        verbose_stream() << objective[i].second 
                                         << " * v" << objective[i].first << " ";
@@ -991,9 +991,12 @@ namespace smt {
                 if (num_nodes <= v && v < num_nodes + num_edges) {
                     unsigned edge_id = v - num_nodes;
                     literal lit = m_edges[edge_id].m_justification;
-                    get_context().literal2expr(lit, tmp);
-                    core.push_back(tmp);
+                    if (lit != null_literal) {
+                        get_context().literal2expr(lit, tmp);
+                        core.push_back(tmp);
+                    }
                 }
+                TRACE("opt", tout << core << "\n";);
             }
             for (unsigned i = 0; i < num_nodes; ++i) {
                 mpq_inf const& val = S.get_value(i);