diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index e59ba7f10..e8149c183 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -1137,11 +1137,23 @@ namespace smt {
     };
 
     model_value_proc * theory_datatype::mk_value(enode * n, model_generator & mg) {
+        auto mk_fallback = [&]() -> model_value_proc * {
+            app* val = to_app(m_factory->get_some_value(n->get_sort()));
+            TRACE(datatype,
+                  tout << "fallback datatype value for " << pp(n, m)
+                       << " = " << mk_pp(val, m) << "\n";);
+            return alloc(expr_wrapper_proc, val);
+        };
         theory_var v = n->get_th_var(get_id());
+        // Guard before using union-find: null_theory_var is not a valid index for m_find.
+        if (v == null_theory_var)
+            return mk_fallback();
         v            = m_find.find(v);
-        SASSERT(v != null_theory_var);
+        if (v == null_theory_var || static_cast<unsigned>(v) >= m_var_data.size() || m_var_data[v] == nullptr)
+            return mk_fallback();
         var_data * d = m_var_data[v];
-        SASSERT(d->m_constructor);
+        if (d->m_constructor == nullptr)
+            return mk_fallback();
         func_decl * c_decl = d->m_constructor->get_decl();
         datatype_value_proc * result = alloc(datatype_value_proc, c_decl);
         for (enode* arg : enode::args(d->m_constructor)) 
diff --git a/src/test/api_datalog.cpp b/src/test/api_datalog.cpp
index 45422d515..6e88a8ade 100644
--- a/src/test/api_datalog.cpp
+++ b/src/test/api_datalog.cpp
@@ -64,5 +64,31 @@ void tst_api_datalog() {
         Z3_fixedpoint_dec_ref(ctx, fp);
     }
 
+    // Regression test for Spacer model construction on ADT CHCs
+    {
+        char const* chc =
+            "(set-logic HORN)\n"
+            "(set-option :fp.engine spacer)\n"
+            "(set-option :fp.spacer.random_seed 51)\n"
+            "(set-option :timeout 2000)\n"
+            "(declare-datatypes ((L 0)) (((cons (hd Int) (tl L)) (nil))))\n"
+            "(declare-fun reva (L L L) Bool)\n"
+            "(assert (forall ((a L)) (reva nil a a)))\n"
+            "(assert (forall ((x L) (acc L) (r L) (h Int))\n"
+            "  (=> (reva x (cons h acc) r)\n"
+            "      (reva (cons h x) acc r))))\n"
+            "(assert (forall ((B L) (C L) (D L) (E L) (F L))\n"
+            "  (=> (and (reva B C D)\n"
+            "           (reva D nil E)\n"
+            "           (reva C B F)\n"
+            "           (not (= E F)))\n"
+            "      false)))\n"
+            "(check-sat)\n";
+
+        Z3_string response = Z3_eval_smtlib2_string(ctx, chc);
+        ENSURE(response != nullptr);
+        ENSURE(Z3_get_error_code(ctx) == Z3_OK);
+    }
+
     Z3_del_context(ctx);
-}
\ No newline at end of file
+}