Fix elim-term-ite simplifier soundness: missing auxiliary variable constraints (#10244)

The `elim-term-ite` **simplifier** (via `set-simplifier` /
`addSimplifier`) was unsound: it reported `sat` with a spurious model on
trivially unsat inputs by replacing term-ITEs with fresh auxiliary
variables but never asserting their defining constraints, leaving them
unconstrained.

```smt2
(declare-const x Real)
(declare-const b Bool)
(set-simplifier elim-term-ite)
(assert (and (> x 10.0) (< x (ite b 1.0 2.0))))
(check-sat)
; was: sat (x=11 — spurious)
; now: unsat
```

## Changes

- **`src/ast/normal_forms/elim_term_ite.cpp` — `reduce_app`**: When
`defined_names::mk_name` returns `false` (name already cached for a
given ITE), the old code returned `BR_FAILED`, leaving the ITE
unreplaced in subsequent formulas. Now unconditionally sets `result =
new_r` and returns `BR_DONE`, mirroring the tactic version's behavior.

- **`src/ast/simplifiers/elim_term_ite.h` — `reduce()`**: After
rewriting each formula, the newly created definitions accumulated in
`m_rewriter.new_defs()` are now added to `m_fmls`. Previously these were
silently discarded, making auxiliary variables completely unconstrained.

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10239

---------

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

src/ast/simplifiers/elim_term_ite.h

@@ -34,11 +34,17 @@ public:
     void reduce() override {
         expr_ref r(m);
         proof_ref pr(m);
+        unsigned prev_defs_sz = m_rewriter.new_defs().size();
         for (unsigned idx : indices()) {
             auto const& d = m_fmls[idx];
             m_rewriter(d.fml(), r, pr);
             if (d.fml() != r)
                 m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep()));
+            for (unsigned i = prev_defs_sz; i < m_rewriter.new_defs().size(); ++i) {
+                auto const& def = m_rewriter.new_defs()[i];
+                m_fmls.add(dependent_expr(m, def.fml(), def.pr(), nullptr));
+            }
+            prev_defs_sz = m_rewriter.new_defs().size();
         }
     }