Fix sat.smt=true model reconstruction for QF_UFBV with Bool-valued UF predicates (#9519)

`sat.smt=true` could return `sat` with an invalid model for QF_UFBV
formulas combining Bool-valued UFs and BV range constraints. The failure
came from broken model-trail reconstruction in `elim_unconstrained`,
where `ADD` entries were effectively turned into identity substitutions.

- **Root-cause fix: restore model-trail substitution composition**
- In `elim_unconstrained::update_model_trail`,
`generic_model_converter::ADD` entries now use `entry.m_def` (rewritten
through accumulated substitutions) instead of creating self-referential
const-to-const mappings.
- This re-enables correct back-substitution for eliminated unconstrained
terms during witness reconstruction.

- **Regression coverage: QF_UFBV + `sat.smt=true` + model validation**
  - Added a focused unit test in `src/test/simplifier.cpp` for:
    - Bool-valued UF predicate over BV vars
    - split BV range constraints (`bvuge` / `bvult`)
    - `:sat.smt true` and `:model_validate true`
- The test asserts the solver returns `sat` without emitting an
invalid-model error.

```cpp
// before (effectively no-op back-mapping)
new_def = m.mk_const(entry.m_f);
sub->insert(new_def, new_def, nullptr, nullptr);

// after (compose and apply recorded definition)
new_def = entry.m_def;
(*rp)(new_def);
sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
```

---------

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

src/ast/simplifiers/elim_unconstrained.cpp

@@ -413,10 +413,9 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
         case generic_model_converter::instruction::HIDE:
             break;
         case generic_model_converter::instruction::ADD:
-            //            new_def = entry.m_def;
-            // (*rp)(new_def);
-            new_def = m.mk_const(entry.m_f);
-            sub->insert(new_def, new_def, nullptr, nullptr);
+            new_def = entry.m_def;
+            (*rp)(new_def);
+            sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
             break;
         }
     }

src/test/simplifier.cpp

@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "api/z3.h"
 #include "api/z3_private.h"
+#include <cstring>
 #include <iostream>
 #include "util/util.h"
 #include "util/trace.h"
@@ -211,6 +212,26 @@ static void test_array() {
     Z3_del_context(ctx);
 }
 
+static void test_sat_smt_ufbv_predicate_model_validation() {
+    Z3_context ctx = Z3_mk_context(nullptr);
+    const char* result =
+        Z3_eval_smtlib2_string(ctx,
+            "(set-logic QF_UFBV)\n"
+            "(set-option :sat.smt true)\n"
+            "(set-option :model_validate true)\n"
+            "(declare-fun p ((_ BitVec 4)) Bool)\n"
+            "(declare-const x (_ BitVec 4))\n"
+            "(declare-const y (_ BitVec 4))\n"
+            "(assert (xor (p x) (p y)))\n"
+            "(assert (bvuge x (_ bv1 4)))\n"
+            "(assert (bvult y (_ bv1 4)))\n"
+            "(check-sat)\n"
+            "(get-model)\n");
+    ENSURE(std::strstr(result, "sat") != nullptr);
+    ENSURE(std::strstr(result, "invalid model") == nullptr);
+    Z3_del_context(ctx);
+}
+
 void tst_simplifier() {
 
     test_array();
@@ -218,4 +239,5 @@ void tst_simplifier() {
     test_datatypes();
     test_bool();
     test_skolemize_bug();
+    test_sat_smt_ufbv_predicate_model_validation();
 }