Prevent Spacer segfault on ADT CHCs by hardening datatype model-value construction (#9571)

Spacer can crash on small HORN/ADT benchmarks when model construction
reaches datatype enodes without a fully populated constructor state. The
failure manifested as a null/invalid-path dereference inside datatype
model value generation.

- **Root cause area: datatype model extraction path**
- Hardened `theory_datatype::mk_value` to handle incomplete theory state
safely instead of assuming constructor metadata is always present.
  - Added guarded fallback to a factory-provided datatype value when:
    - `th_var` is missing,
    - union-find lookup is invalid,
    - var data/constructor is unavailable.

- **Behavioral change**
- Missing constructor state now degrades to a safe model value
(`expr_wrapper_proc`) instead of crashing during model generation.

- **Regression coverage**
- Added a focused API regression in `src/test/api_datalog.cpp` using a
Spacer + ADT HORN script (with reproducing seed) to ensure the code path
executes without parser/runtime failure.

```cpp
// theory_datatype::mk_value fallback shape
if (v == null_theory_var || invalid_var_data || d->m_constructor == nullptr) {
    app* val = to_app(m_factory->get_some_value(n->get_sort()));
    return alloc(expr_wrapper_proc, val);
}
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

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)) 

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);
-}
+}