diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index f7e3f6293..eb0af0c69 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -561,6 +561,9 @@ namespace arith {
     void solver::dbg_finalize_model(model& mdl) {
         if (m_not_handled)
             return;
+
+        // this is already handled in general in euf_model.cpp
+        return;
         bool found_bad = false;
         for (unsigned v = 0; v < get_num_vars(); ++v) {
             if (!is_bool(v))
@@ -583,35 +586,8 @@ namespace arith {
             if (!found_bad && value == get_phase(n->bool_var()))
                 continue;
 
-            TRACE("arith",
-                ptr_vector<expr> nodes;
-                expr_mark marks;
-                nodes.push_back(n->get_expr());
-                for (unsigned i = 0; i < nodes.size(); ++i) {
-                    expr* r = nodes[i];
-                    if (marks.is_marked(r))
-                        continue;
-                    marks.mark(r);
-                    if (is_app(r))
-                        for (expr* arg : *to_app(r))
-                            nodes.push_back(arg);
-                    expr_ref rval(m);                    
-                    expr_ref mval = mdl(r);
-                    if (ctx.get_egraph().find(r))
-                        rval = mdl(ctx.get_egraph().find(r)->get_root()->get_expr());
-                    tout << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << " := " << mval;
-                    if (rval != mval) tout << " " << rval;
-                    tout << "\n";
-                });
-            TRACE("arith",
-                tout << eval << " " << value << " " << ctx.bpp(n) << "\n";
-                tout << mdl << "\n";
-                s().display(tout););
-            IF_VERBOSE(0, 
-                       verbose_stream() << eval << " " << value << " " << ctx.bpp(n) << "\n";
-                       verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
-                       verbose_stream() << *b << "\n";);
-            IF_VERBOSE(0, ctx.display_validation_failure(verbose_stream(), mdl, n));
+            TRACE("arith", ctx.display_validation_failure(tout << *b << "\n", mdl, n));
+            IF_VERBOSE(0, ctx.display_validation_failure(verbose_stream() << *b << "\n", mdl, n));
             UNREACHABLE();
         }
     }
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index c22c46322..54a3d63d8 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -287,17 +287,20 @@ namespace euf {
         nodes.push_back(n);
         for (unsigned i = 0; i < nodes.size(); ++i) {
             euf::enode* r = nodes[i];
-            if (r->is_marked1())
+            if (!r || r->is_marked1())
                 continue;
             r->mark1();
-            for (auto* arg : euf::enode_args(r))
-                nodes.push_back(arg);           
+            if (is_app(r->get_expr()))
+                for (auto* arg : *r->get_app())
+                    nodes.push_back(get_enode(arg));
             expr_ref val = mdl(r->get_expr());
             expr_ref sval(m);
             th_rewriter rw(m);
             rw(val, sval);
             expr_ref mval = mdl(r->get_root()->get_expr());
             if (mval != sval) {
+                if (r->bool_var() != sat::null_bool_var)
+                    out << "b" << r->bool_var() << " ";
                 out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << mval << "\n";
                 continue;
             }
@@ -309,7 +312,8 @@ namespace euf {
                 out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << bval << "\n";
         }
         for (euf::enode* r : nodes)
-            r->unmark1();
+            if (r)
+                r->unmark1();
         out << mdl << "\n";
     }