diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 45641ffbf..7ef1ea273 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -214,7 +214,7 @@ public:
         unsigned j = null_lpvar;
         if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) 
             return;
-        TRACE("cheap_eq", tout << "found j=" << j << " for v=";
+        TRACE("cheap_eq", tout << "found j = " << j << " v_j = " << v_j << " for v = ";
               print(tout, v) << "\n in lp.fixed tables\n";);
         vector<edge> path;
         find_path_on_tree(path, v, m_fixed_vertex);
@@ -281,11 +281,11 @@ public:
         m_fixed_vertex_explanation = get_explanation_from_path(path);
         explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
         set_fixed_vertex(v);
-        TRACE("cheap_eq", tout << "polarity switch between: v = "; print(tout , v) << "\nand u = "; print(tout, u) << "\n";);
-        TRACE("cheap_eq", tout << "fixed vertex explanation\n";
-              for (auto p : m_fixed_vertex_explanation) {
-                  lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
-              });
+        TRACE("cheap_eq", 
+              tout << "polarity switch: " << polarity << "\nv = "; print(tout , v) << "\nu = "; print(tout, u) << "\n";
+              tout << "fixed vertex explanation\n";
+              for (auto p : m_fixed_vertex_explanation) 
+                  lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci()););
 
     }
     
@@ -379,7 +379,7 @@ public:
     }
 
     void check_for_eq_and_add_to_val_table(vertex* v,  map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>>& table) {
-        TRACE("cheap_eq", tout << "v="; print(tout, v) << "\n";);
+        TRACE("cheap_eq", tout << "v = "; print(tout, v) << "\n";);
         const vertex *k; // the other vertex
         if (table.find(val(v), k)) {
             TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";);
@@ -447,7 +447,9 @@ public:
         SASSERT(j != k);
         unsigned je = lp().column_to_reported_index(j);
         unsigned ke = lp().column_to_reported_index(k);
-        TRACE("cheap_eq", tout << "reporting eq " << j << ", " << k << "\n";
+        TRACE("cheap_eq", 
+              tout << "reporting eq " << j  << ", " << k << "\n";
+              tout << "reported idx " << je << ", " << ke << "\n";
               for (auto p : exp) {
                   lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
               }
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index e87d1122c..63688fe77 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -220,12 +220,22 @@ namespace smt {
     void context::display_assignment(std::ostream & out) const {
         if (!m_assigned_literals.empty()) {
             out << "current assignment:\n";
+            unsigned level = 0;
             for (literal lit : m_assigned_literals) {
-                display_literal(out, lit);
+                if (level < get_assign_level(lit.var())) {
+                    level = get_assign_level(lit.var());
+                    out << "level " << level << "\n";
+                }
+                display_literal(out << lit << " ", lit);
                 if (!is_relevant(lit)) out << " n ";
                 out << ": ";
                 display_verbose(out, m, 1, &lit, m_bool_var2expr.c_ptr());
-                out << "\n";
+                if (level > 0) {
+                    auto j = get_justification(lit.var());
+                    display(out << " ", j);
+                }
+                else 
+                    out << "\n";
             }
         }
     }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 4baa1f476..bb3fb1431 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2811,6 +2811,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     expr_ref f(m);
     literal lit(v, !is_true);
     TRACE("seq", tout << (is_true?"":"not ") << mk_bounded_pp(e, m) << "\n";);
+    TRACE("seq", tout << (is_true?"":"not ") << mk_bounded_pp(e, m) << " " << ctx.get_scope_level() << " " << lit << "\n";);
 
     if (m_util.str.is_prefix(e, e1, e2)) {
         if (is_true) {