diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 9e6a9fae6..2142ffae3 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -239,6 +239,7 @@ namespace opt {
                     terms[i] = m.mk_not(terms[i].get());
                 }
             }
+            id = symbol(index);
             return true;
         }
         if (is_maximize(fml, term, index) &&
@@ -260,6 +261,7 @@ namespace opt {
                 offset += weights[i];
             }
             neg = true;
+            id = symbol(index);
             return true;
         }
         return false;
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index e43db8dce..eecb1109b 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1121,6 +1121,7 @@ namespace smt {
             }
             else {                
                 if (lvl == m_conflict_lvl) {
+                    TRACE("pb", tout << "add mark: " << l << " " << coeff << "\n";);
                     ++m_num_marks;
                 }
                 set_mark(v, m_lemma.size());
@@ -1285,7 +1286,8 @@ namespace smt {
                 justification& j = *js.get_justification(); 
                 // only process pb justifications.
                 if (j.get_from_theory() != get_id()) {
-                    IF_VERBOSE(0, verbose_stream() << "skipping justification for " << conseq << "\n";);
+                    IF_VERBOSE(0, verbose_stream() << "skipping justification for theory " << conseq << "\n";);
+                    IF_VERBOSE(0, verbose_stream() << j.get_from_theory() << "\n";);
                     m_ineq_literals.push_back(conseq);
                     break;
                 }