diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index b862781b7..75fb03c9e 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -1118,7 +1118,7 @@ namespace datalog {
             unsigned idx_dst = dstt.column_idx(col_dst);
             unsigned idx_src = srct.column_idx(col_src);
             unsigned num_tbits = dstt.column_num_bits(col_dst);
-            SASSERT(num_bits == srct.column_num_bits(col_src));
+            SASSERT(num_tbits == srct.column_num_bits(col_src));
             IF_VERBOSE(3, verbose_stream() << "copy column " << idx_src
                        << " to " << idx_dst << " " << num_tbits << "\n";);
             for (unsigned i = 0; i < num_tbits; ++i) {
diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp
index 41e4d12de..8ec385f9d 100644
--- a/src/opt/inc_sat_solver.cpp
+++ b/src/opt/inc_sat_solver.cpp
@@ -318,6 +318,18 @@ private:
             asm2dep.insert(it->m_value.index(), it->m_key);
         }
         sat::literal_vector const& core = m_solver.get_core();
+        TRACE("opt",
+              dep2asm_t::iterator it = dep2asm.begin();
+              dep2asm_t::iterator end = dep2asm.end();
+              for (; it != end; ++it) {
+                  tout << mk_pp(it->m_key, m) << " |-> " << sat::literal(it->m_value) << "\n";
+              }
+              tout << "core: ";
+              for (unsigned i = 0; i < core.size(); ++i) {
+                  tout << core[i] << " ";
+              }
+              tout << "\n";
+              );              
 
         m_core.reset();
         for (unsigned i = 0; i < core.size(); ++i) {
@@ -325,18 +337,6 @@ private:
             VERIFY (asm2dep.find(core[i].index(), e));
             m_core.push_back(e);
         }
-        TRACE("opt",
-              dep2asm_t::iterator it = dep2asm.begin();
-              dep2asm_t::iterator end = dep2asm.end();
-              for (; it != end; ++it) {
-                  tout << mk_pp(it->m_key, m) << " |-> " << it->m_value << "\n";
-              }
-              tout << "core: ";
-              for (unsigned i = 0; i < core.size(); ++i) {
-                  tout << core[i] << ": " << mk_pp(m_core[i].get(), m) << " ";
-              }
-              tout << "\n";
-              );              
 
 
     }