diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 1e02529222d..100d0046088 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -326,6 +326,7 @@ namespace euf {
         void collect_statistics(statistics& st) const;
 
         unsigned num_scopes() const { return m_scopes.size() + m_num_scopes; }
+        unsigned num_nodes() const { return m_nodes.size(); }
     };
 
     inline std::ostream& operator<<(std::ostream& out, egraph const& g) { return g.display(out); }
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 129026b34ea..89e079df443 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -427,9 +427,11 @@ namespace array {
             app_ref sel1(m), sel2(m);
             sel1 = a.mk_select(args1);
             sel2 = a.mk_select(args2);
+            prop |= !ctx.get_enode(sel1) || !ctx.get_enode(sel2);
             if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom()))
                 prop = true;
         }
+        prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2);
         if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()))
             prop = true;
         return prop;
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 07c269d48b1..76c154a4a02 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -714,6 +714,7 @@ namespace dt {
         if (v == euf::null_theory_var) 
             return false;
         euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
+        CTRACE("dt", !con, display(tout) << ctx.bpp(n) << "\n";);
         if (con->num_args() == 0)
             dep.insert(n, nullptr);
         for (enode* arg : euf::enode_args(con))
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index f66c4a33153..8efd3c9e4dc 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -449,8 +449,8 @@ namespace euf {
 
         if (!init_relevancy())
             give_up = true;
-
-
+        
+        unsigned num_nodes = m_egraph.num_nodes();
         for (auto* e : m_solvers) {
             if (!m.inc())
                 return sat::check_result::CR_GIVEUP;
@@ -468,6 +468,10 @@ namespace euf {
             return sat::check_result::CR_CONTINUE;
         if (give_up)
             return sat::check_result::CR_GIVEUP;
+        if (num_nodes < m_egraph.num_nodes()) {
+            IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
+            return sat::check_result::CR_CONTINUE;           
+        }
         if (m_qsolver)
             return m_qsolver->check();
         TRACE("after_search", s().display(tout););