mcsat: avoid eval_in_model longjmp on unmapped uninterpreted blasted leaf

Fixes the windows-latest|release|--enable-thread-safety --enable-mcsat
failure in tests/api/mcsat_tuples.c::test_partial_tuple_model_no_keep_subst.

Root cause (confirmed by the unbuffered Windows CI trace):

In preprocessor_build_tuple_model, when reconstructing the value of a
tuple-blasted atom, we call model_get_term_value() on each blasted
leaf. With keep_subst=0 the model has no alias table
(model->has_alias == 0), so eval_uninterpreted -- invoked transitively
on an *unmapped* uninterpreted leaf -- raises MDL_EVAL_UNKNOWN_TERM via
longjmp() to the setjmp() inside eval_in_model().

That longjmp path returns cleanly on macOS/Linux, but on MinGW x86_64
under -O3 -fomit-frame-pointer with THREAD_SAFE (TLS) enabled it
crashes inside the unwind. setjmp/longjmp on mingw-w64 x86_64 is
implemented via SEH and is sensitive to omitted frame pointers and TLS
interactions; this configuration is exactly the one that breaks.

The crash is reproducible and Windows-only because only this test
exercises all three triggers simultaneously: keep_subst=0 (no alias
table), an *unmapped* tuple-blasted leaf (the second component of the
unconstrained tuple x is never assigned during search), and that leaf
being an UNINTERPRETED_TERM (never substituted away by an equality).

Captured Windows CI trace (excerpt, before this fix):

  [mcsat_tuples] START test_partial_tuple_model_no_keep_subst
  [pp_build_model] enter, has_alias=0, eqs=1
  ...
  [pp_build_tuple] i=0 atom=774 tau=21
  [pp_build_tuple]   n_leaves=2
  [pp_build_tuple]   j=0 leaf=780
  [pp_build_tuple]     model_get_term_value -> 2     <- mapped, fine
  [pp_build_tuple]   j=1 leaf=782                    <- unmapped uninterp
  <crash inside model_get_term_value>

Fix:

In the per-leaf loop of preprocessor_build_tuple_model, first try the
direct lookup model_find_term_value(). Only fall through to
model_get_term_value() (which can invoke eval_in_model) when there is
either an alias table to consult or the leaf is not an uninterpreted
term -- i.e., when the evaluator can plausibly produce a value. For
the remaining case (no alias + unmapped + uninterpreted), v stays at
null_value (< 0) and the existing fallback path mints a fresh default
via vtbl_make_object(leaf_tau), which is sound: an unmapped
uninterpreted leaf is unconstrained, so any value of the right type
preserves model correctness.

This avoids the longjmp/SEH unwind path entirely on the only execution
path where it could fire, fixing the Windows crash without changing
semantics on Linux/macOS.

The accompanying revert of TEMP-DIAG stderr prints (in preprocessor.c
and tests/api/mcsat_tuples.c) removes the now-unneeded instrumentation
that pinned the bug.

Author: disteph

src/mcsat/preprocessor.c

@@ -40,24 +40,6 @@
 #include "yices.h"
 #include "api/yices_api_lock_free.h"
 
-#include <stdlib.h>
-
-/* TEMP DIAG: stderr trace macro, gated on env var YICES_PP_TRACE so the
- * diagnostic prints don't pollute regression-test stderr (regression
- * tests diff stderr against expected output). Set YICES_PP_TRACE=1 in CI
- * runs that need to debug the Windows MinGW release+thread-safety
- * failure. To be removed along with every PP_DIAG call site once the
- * failure is pinpointed. */
-static int pp_diag_enabled(void) {
-  static int cached = -1;
-  if (cached < 0) {
-    const char* s = getenv("YICES_PP_TRACE");
-    cached = (s != NULL && s[0] != '\0' && s[0] != '0') ? 1 : 0;
-  }
-  return cached;
-}
-#define PP_DIAG(...) do { if (pp_diag_enabled()) { fprintf(stderr, __VA_ARGS__); fflush(stderr); } } while (0)
-
 void preprocessor_construct(preprocessor_t* pre, term_table_t* terms, jmp_buf* handler, const mcsat_options_t* options) {
   pre->terms = terms;
   init_term_manager(&pre->tm, terms);
@@ -2479,35 +2461,26 @@ static value_t merge_blasted_function_value(preprocessor_t* pre, value_table_t*
 static
 value_t build_value_from_flat(preprocessor_t* pre, value_table_t* vtbl, type_t tau, const value_t* flat, uint32_t* idx) {
   type_table_t* types = pre->terms->types;
-  PP_DIAG("[build_value_from_flat] enter tau=%d idx=%u\n", (int) tau, (unsigned) *idx);
 
   if (type_kind(types, tau) == TUPLE_TYPE) {
     tuple_type_t* tuple = tuple_type_desc(types, tau);
     uint32_t i, n = tuple->nelem;
-    PP_DIAG("[build_value_from_flat] TUPLE n=%u\n", (unsigned) n);
     value_t elem[n];
     for (i = 0; i < n; ++i) {
       elem[i] = build_value_from_flat(pre, vtbl, tuple->elem[i], flat, idx);
       if (elem[i] == null_value) {
-        PP_DIAG("[build_value_from_flat] TUPLE elem %u null\n", (unsigned) i);
         return null_value;
       }
     }
-    PP_DIAG("[build_value_from_flat] TUPLE calling vtbl_mk_tuple\n");
-    value_t r = vtbl_mk_tuple(vtbl, n, elem);
-    PP_DIAG("[build_value_from_flat] TUPLE vtbl_mk_tuple -> %d\n", (int) r);
-    return r;
+    return vtbl_mk_tuple(vtbl, n, elem);
   } else if (type_kind(types, tau) == FUNCTION_TYPE) {
     uint32_t n = type_leaf_count(pre, tau);
-    PP_DIAG("[build_value_from_flat] FUNCTION n_leaves=%u\n", (unsigned) n);
     value_t v = merge_blasted_function_value(pre, vtbl, tau, flat + *idx, n);
     *idx += n;
-    PP_DIAG("[build_value_from_flat] FUNCTION merge -> %d new_idx=%u\n", (int) v, (unsigned) *idx);
     return v;
   } else {
     value_t v = flat[*idx];
     (*idx)++;
-    PP_DIAG("[build_value_from_flat] LEAF v=%d new_idx=%u\n", (int) v, (unsigned) *idx);
     return v;
   }
 }
@@ -2705,27 +2678,19 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
   type_table_t* types = pre->terms->types;
   uint32_t i;
 
-  /* TEMP DIAG (windows release+thread-safety mcsat_tuples failure) */
-  PP_DIAG("[pp_build_tuple] enter, atoms=%u\n",
-          (unsigned) pre->tuple_blast_atoms.size);
   for (i = 0; i < pre->tuple_blast_atoms.size; ++i) {
     term_t atom = pre->tuple_blast_atoms.data[i];
     ivector_t leaves;
     type_t tau = term_type(pre->terms, atom);
     uint32_t n, j;
 
-    PP_DIAG("[pp_build_tuple] i=%u atom=%d tau=%d\n",
-            (unsigned) i, (int) atom, (int) tau);
-
     if (model_find_term_value(model, atom) != null_value) {
-      PP_DIAG("[pp_build_tuple]   atom already mapped, continue\n");
       continue;
     }
 
     init_ivector(&leaves, 0);
     tuple_blast_get(pre, atom, &leaves);
     n = leaves.size;
-    PP_DIAG("[pp_build_tuple]   n_leaves=%u\n", (unsigned) n);
     if (n == 0) {
       delete_ivector(&leaves);
       continue;
@@ -2734,10 +2699,12 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
     value_t leaf_vals[n];
     bool ok = true;
     for (j = 0; j < n; ++j) {
-      PP_DIAG("[pp_build_tuple]   j=%u leaf=%d\n",
-              (unsigned) j, (int) leaves.data[j]);
-      value_t v = model_get_term_value(model, leaves.data[j]);
-      PP_DIAG("[pp_build_tuple]     model_get_term_value -> %d\n", (int) v);
+      term_t leaf = leaves.data[j];
+      value_t v = model_find_term_value(model, leaf);
+      if (v == null_value &&
+          (model->has_alias || term_kind(pre->terms, leaf) != UNINTERPRETED_TERM)) {
+        v = model_get_term_value(model, leaf);
+      }
       if (v < 0) {
         /* The blasted leaf was never assigned a value by the mcsat
          * search (typical for unconstrained tuple components) and
@@ -2748,19 +2715,15 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
          * so the original tuple atom can still be reconstructed.
          * vtbl_make_object handles bool / arith / bv / tuple /
          * function / scalar uniformly. */
-        type_t leaf_tau = term_type(pre->terms, leaves.data[j]);
-        PP_DIAG("[pp_build_tuple]     leaf_tau=%d, calling vtbl_make_object\n",
-                (int) leaf_tau);
+        type_t leaf_tau = term_type(pre->terms, leaf);
         v = vtbl_make_object(vtbl, leaf_tau);
-        PP_DIAG("[pp_build_tuple]     vtbl_make_object -> %d\n", (int) v);
         if (v < 0) {
           ok = false;
           break;
         }
       }
       leaf_vals[j] = v;
     }
-    PP_DIAG("[pp_build_tuple]   leaf loop done, ok=%d\n", (int) ok);
     if (!ok) {
       /* vtbl_make_object failed for some leaf: the type cannot be
        * inhabited concretely (extremely unusual -- e.g. a malformed
@@ -2779,9 +2742,7 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
     }
 
     if (type_kind(types, tau) == FUNCTION_TYPE) {
-      PP_DIAG("[pp_build_tuple]   FUNCTION_TYPE branch\n");
       value_t f = merge_blasted_function_value(pre, vtbl, tau, leaf_vals, n);
-      PP_DIAG("[pp_build_tuple]   merge_blasted_function_value -> %d\n", (int) f);
       if (f >= 0) {
         model_map_term(model, atom, f);
       } else if (trace_enabled(pre->tracer, "mcsat::preprocess")) {
@@ -2792,16 +2753,10 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
         trace_term_ln(pre->tracer, pre->terms, atom);
       }
     } else {
-      PP_DIAG("[pp_build_tuple]   non-FUNCTION branch, calling build_value_from_flat\n");
       uint32_t idx = 0;
       value_t v = build_value_from_flat(pre, vtbl, tau, leaf_vals, &idx);
-      PP_DIAG("[pp_build_tuple]   build_value_from_flat -> %d (idx=%u)\n",
-              (int) v, (unsigned) idx);
       if (v >= 0) {
-        PP_DIAG("[pp_build_tuple]   model_map_term(atom=%d, v=%d)\n",
-                (int) atom, (int) v);
         model_map_term(model, atom, v);
-        PP_DIAG("[pp_build_tuple]   model_map_term OK\n");
       } else if (trace_enabled(pre->tracer, "mcsat::preprocess")) {
         mcsat_trace_printf(pre->tracer,
                            "preprocessor_build_tuple_model: dropping tuple atom ");
@@ -2812,9 +2767,7 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
     }
 
     delete_ivector(&leaves);
-    PP_DIAG("[pp_build_tuple]   end of iteration i=%u\n", (unsigned) i);
   }
-  PP_DIAG("[pp_build_tuple] exit\n");
 }
 
 static term_t build_term_from_flat(preprocessor_t* pre, type_t tau, const term_t* flat, uint32_t* idx);
@@ -3057,14 +3010,9 @@ void preprocessor_build_model(preprocessor_t* pre, model_t* model) {
    * touched and the alias-based lazy resolution handles everything. */
   evaluator_t eval;
   bool eval_inited = false;
-  /* TEMP DIAG (windows release+thread-safety mcsat_tuples failure) */
-  PP_DIAG("[pp_build_model] enter, has_alias=%d, eqs=%u\n",
-          (int) model->has_alias, (unsigned) pre->equalities_list.size);
   for (i = 0; i < pre->equalities_list.size; ++ i) {
     term_t eq = pre->equalities_list.data[i];
     term_t eq_var = preprocessor_get_eq_solved_var(pre, eq);
-    PP_DIAG("[pp_build_model] i=%u eq=%d eq_var=%d\n",
-            (unsigned) i, (int) eq, (int) eq_var);
     if (trace_enabled(pre->tracer, "mcsat::preprocess")) {
       mcsat_trace_printf(pre->tracer, "eq = ");
       trace_term_ln(pre->tracer, pre->terms, eq);
@@ -3075,24 +3023,18 @@ void preprocessor_build_model(preprocessor_t* pre, model_t* model) {
     // Some equalities are solved, but then reasserted in the solver
     // these already have a model
     if (model_find_term_value(model, eq_var) != null_value) {
-      PP_DIAG("[pp_build_model]   already mapped, continue\n");
       continue;
     }
     // Some equalities are marked, but not solved. These we skip as they
     // are already set in the model
     if (preprocessor_get(pre, eq_var) == eq_var) {
-      PP_DIAG("[pp_build_model]   not solved, continue\n");
       continue;
     }
     term_kind_t eq_kind = term_kind(pre->terms, eq);
-    PP_DIAG("[pp_build_model]   eq_kind=%d\n", (int) eq_kind);
     composite_term_t* eq_desc = get_composite(pre->terms, eq_kind, eq);
-    PP_DIAG("[pp_build_model]   eq_desc=%p arity=%u\n",
-            (void*) eq_desc, eq_desc ? (unsigned) eq_desc->arity : 0u);
     term_t eq_subst = eq_desc->arity > 1
       ? (eq_desc->arg[0] == eq_var ? eq_desc->arg[1] : eq_desc->arg[0])
       : zero_term;
-    PP_DIAG("[pp_build_model]   eq_subst=%d\n", (int) eq_subst);
     if (model->has_alias) {
       /* Standard path: record the substitution and let the model
        * evaluator resolve eq_var lazily via eval_term(eq_subst). */
@@ -3111,25 +3053,16 @@ void preprocessor_build_model(preprocessor_t* pre, model_t* model) {
        * If eval fails (e.g., eq_subst transitively depends on another
        * not-yet-mapped eq_var), fall back to a fresh default value. */
       if (!eval_inited) {
-        PP_DIAG("[pp_build_model]   init_evaluator\n");
         init_evaluator(&eval, model);
         eval_inited = true;
-        PP_DIAG("[pp_build_model]   init_evaluator OK\n");
       }
-      PP_DIAG("[pp_build_model]   eval_in_model(%d)\n", (int) eq_subst);
       value_t v = eval_in_model(&eval, eq_subst);
-      PP_DIAG("[pp_build_model]   eval_in_model -> v=%d\n", (int) v);
       if (v < 0) {
         type_t eq_var_tau = term_type(pre->terms, eq_var);
-        PP_DIAG("[pp_build_model]   vtbl_make_object(tau=%d)\n", (int) eq_var_tau);
         v = vtbl_make_object(model_get_vtbl(model), eq_var_tau);
-        PP_DIAG("[pp_build_model]   vtbl_make_object -> v=%d\n", (int) v);
       }
       if (v >= 0) {
-        PP_DIAG("[pp_build_model]   model_map_term(eq_var=%d, v=%d)\n",
-                (int) eq_var, (int) v);
         model_map_term(model, eq_var, v);
-        PP_DIAG("[pp_build_model]   model_map_term OK\n");
       } else if (trace_enabled(pre->tracer, "mcsat::preprocess")) {
         mcsat_trace_printf(pre->tracer,
                            "preprocessor_build_model: failed to bind eq_var ");
@@ -3139,14 +3072,10 @@ void preprocessor_build_model(preprocessor_t* pre, model_t* model) {
   }
 
   if (eval_inited) {
-    PP_DIAG("[pp_build_model] delete_evaluator\n");
     delete_evaluator(&eval);
-    PP_DIAG("[pp_build_model] delete_evaluator OK\n");
   }
 
-  PP_DIAG("[pp_build_model] calling preprocessor_build_tuple_model\n");
   preprocessor_build_tuple_model(pre, model);
-  PP_DIAG("[pp_build_model] exit\n");
 }