From 87c0a8136f501daaefb76f5276c2e792fb66706f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 5 May 2021 16:11:21 -0700
Subject: [PATCH] #5223

---
 src/sat/smt/dt_solver.cpp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 133510a84..07c269d48 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -249,7 +249,7 @@ namespace dt {
         SASSERT(!d->m_constructor);
         SASSERT(!recognizer || ctx.value(recognizer) == l_false || !is_final);
         
-        TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
+        TRACE("dt", tout << ctx.bpp(n) << " non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
 
         if (!recognizer && non_rec_c->get_arity() == 0) {
             sat::literal eq = eq_internalize(n->get_expr(), m.mk_const(non_rec_c));
@@ -474,7 +474,7 @@ namespace dt {
         var_data* d2 = m_var_data[v2];
         auto* con1 = d1->m_constructor;
         auto* con2 = d2->m_constructor;
-        TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";);
+        TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(var2enode(v1)) << " == " << ctx.bpp(var2enode(v2)) << " " << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";);
         if (con1 && con2 && con1->get_decl() != con2->get_decl())
             ctx.set_conflict(euf::th_explain::conflict(*this, con1, con2));
         else if (con2 && !con1) {
@@ -782,7 +782,6 @@ namespace dt {
                 }
             }
             mk_var(n);
-
         }
         else if (is_recognizer(term)) {
             mk_var(n);
@@ -794,6 +793,8 @@ namespace dt {
             SASSERT(is_accessor(term));
             SASSERT(n->num_args() == 1);
             mk_var(n->get_arg(0));
+            if (is_datatype(n))
+                mk_var(n);
         }
 
         return true;