diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index b117ac1e3..073d164be 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -302,7 +302,7 @@ namespace euf {
             if (mval != sval) {
                 if (r->bool_var() != sat::null_bool_var)
                     out << "b" << r->bool_var() << " ";
-                out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << mval << "\n";
+                out << bpp(r) << " :=\nvalue obtained from model:  " << sval << "\nvalue of the root expression:  " << mval << "\n";
                 continue;
             }
             if (!m.is_bool(val))
@@ -310,7 +310,7 @@ namespace euf {
             auto bval = s().value(r->bool_var());
             bool tt = l_true == bval;
             if (tt != m.is_true(sval))
-                out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << bval << "\n";
+                out << bpp(r) << " :=\nvalue according to model:  " << sval << "\nvalue of Boolean literal:  " << bval << "\n";
         }
         for (euf::enode* r : nodes)
             if (r)
@@ -357,6 +357,7 @@ namespace euf {
             if (!tt && !mdl.is_true(e))
                 continue;
             CTRACE("euf", first, display_validation_failure(tout, mdl, n););
+            CTRACE("euf", first, display(tout));
             IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
             (void)first;
             first = false;
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 0a38597e2..a6fd38213 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -93,18 +93,17 @@ namespace intblast {
 
         for (auto const& [src, vi] : m_vars) {
             auto const& [v, b] = vi;
-            verbose_stream() << "asserting " << mk_pp(v, m) << " < " << b << "\n";
             m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
             m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
         }
 
-        verbose_stream() << "check\n";
-        m_solver->display(verbose_stream());
-        verbose_stream() << es << "\n";
+        IF_VERBOSE(10, verbose_stream() << "check\n";
+            m_solver->display(verbose_stream());
+            verbose_stream() << es << "\n");
                
         lbool r = m_solver->check_sat(es);
 
-        verbose_stream() << "result " << r << "\n";
+        IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
 
         if (r == l_false) {
             expr_ref_vector core(m);
@@ -112,8 +111,13 @@ namespace intblast {
             obj_map<expr, unsigned> e2index;
             for (unsigned i = 0; i < es.size(); ++i)
                 e2index.insert(es.get(i), i);
-            for (auto e : core)
-                m_core.push_back(literals[e2index[e]]);
+            for (auto e : core) {
+                unsigned idx = e2index[e];
+                if (idx < literals.size())
+                    m_core.push_back(literals[idx]);
+                else
+                    m_core.push_back(ctx.mk_literal(e));                
+            }
         }
 
         return r;
@@ -128,7 +132,7 @@ namespace intblast {
         return any_of(subterms::all(expr_ref(e, m)), [&](auto* p) { return bv.is_bv_sort(p->get_sort()); });
     }
 
-    void solver::sorted_subterms(expr_ref_vector const& es, ptr_vector<expr>& sorted) {
+    void solver::sorted_subterms(expr_ref_vector& es, ptr_vector<expr>& sorted) {
         expr_fast_mark1 visited;
         for (expr* e : es) {
             sorted.push_back(e);
@@ -144,6 +148,28 @@ namespace intblast {
                         sorted.push_back(arg);
                     }
                 }
+
+                //
+                // Add ground equalities to ensure the model is valid with respect to the current case splits.
+                // This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal
+                // assignment from complete level.
+                // E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment.
+                // If intblast is SAT, then force the model and literal assignment on the rest of the literals.
+                // 
+                if (!is_ground(e))
+                    continue;
+                euf::enode* n = ctx.get_enode(e);
+                if (!n)
+                    continue;
+                if (n == n->get_root())
+                    continue;
+                expr* r = n->get_root()->get_expr();
+                es.push_back(m.mk_eq(e, r));
+                r = es.back();
+                if (!visited.is_marked(r)) {
+                    visited.mark(r);
+                    sorted.push_back(r);
+                }
             }
             else if (is_quantifier(e)) {
                 quantifier* q = to_quantifier(e);
@@ -163,6 +189,7 @@ namespace intblast {
         expr_ref_vector args(m);
         
         sorted_subterms(es, todo);
+
         for (expr* e : todo) {
             if (is_quantifier(e)) {
                 quantifier* q = to_quantifier(e);
@@ -402,8 +429,8 @@ namespace intblast {
         }
 
         TRACE("bv",
-            for (unsigned i = 0; i < es.size(); ++i)
-                tout << mk_pp(es.get(i), m) << " -> " << mk_pp(translated[es.get(i)], m) << "\n";
+            for (expr* e : es)
+                tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated[e], m) << "\n";
         );
 
         for (unsigned i = 0; i < es.size(); ++i) 
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index 33d024be5..c165e1562 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -53,7 +53,8 @@ namespace intblast {
 
         bool is_bv(sat::literal lit);
         void translate(expr_ref_vector& es);
-        void sorted_subterms(expr_ref_vector const& es, ptr_vector<expr>& sorted);
+        void add_root_equations(expr_ref_vector& es, ptr_vector<expr>& sorted);
+        void sorted_subterms(expr_ref_vector& es, ptr_vector<expr>& sorted);
 
     public:
         solver(euf::solver& ctx);
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 4eeec3da4..46c1e293f 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -347,13 +347,13 @@ namespace polysat {
         unsigned sz2 = sz - arg_sz;
         var2pdd(expr2enode(e)->get_th_var(get_id()));
         if (arg_sz == sz) 
-            add_clause(eq_internalize(e, arg), false);            
+            add_clause(eq_internalize(e, arg), nullptr);
         else {
             sat::literal lt0 = ctx.mk_literal(bv.mk_slt(arg, bv.mk_numeral(0, arg_sz)));
             // arg < 0 ==> e = concat(arg, 1...1)
             // arg >= 0 ==> e = concat(arg, 0...0)
-            add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), false);
-            add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);
+            add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), nullptr);
+            add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr);
         }
     }
 
@@ -364,10 +364,10 @@ namespace polysat {
         unsigned sz2 = sz - arg_sz;
         var2pdd(expr2enode(e)->get_th_var(get_id()));
         if (arg_sz == sz)
-            add_clause(eq_internalize(e, arg), false);
+            add_clause(eq_internalize(e, arg), nullptr);
         else 
             // e = concat(arg, 0...0)
-            add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);        
+            add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr);
     }
 
     void solver::internalize_div_rem(app* e, bool is_div) {