mcsat: gate preprocessor diag prints on YICES_PP_TRACE; trim windows CI

Two fixes / aids for the windows-latest|release|--enable-thread-safety
--enable-mcsat mcsat_tuples failure investigation:

1. Gate every preprocessor.c TEMP DIAG stderr print behind an env var
   YICES_PP_TRACE. The existing prints were unconditional, so they
   leaked into the regression-test stderr stream and broke ~21 mcsat
   regression tests (`make test`) that diff stderr against expected
   output. With the gate, the prints are silent unless the env var is
   set, so:

     - `make test` regressions are clean again on every CI config
     - the prints are still available when needed: set
       YICES_PP_TRACE=1 (any non-empty / non-"0" value) before running
       the failing binary.

   Implementation: a tiny static helper `pp_diag_enabled()` reads the
   env var once (cached in a static int -- benign one-time race under
   --enable-thread-safety), and a `PP_DIAG(...)` macro wraps
   fprintf(stderr,...)+fflush(stderr). All call sites switched in
   build_value_from_flat, preprocessor_build_tuple_model, and
   preprocessor_build_model.

   Verified locally:
     mcsat_tuples                          -> 0   "[pp_build|build_value" lines
     YICES_PP_TRACE=1 mcsat_tuples         -> 631 "[pp_build|build_value" lines

2. Trim Windows CI to only the failing config and only the API tests
   so each iteration takes ~10 minutes instead of an hour:

     - Matrix: mode=[release], config-opt=[--enable-thread-safety
       --enable-mcsat] (was 2x3=6 jobs, now 1).
     - Test step: just `make check-api` with YICES_PP_TRACE=1
       exported, so mcsat_tuples emits the full preprocessor trace.
       The `make test` regression sweep is dropped for now.

   Both changes are TEMP and clearly commented; the original matrix
   and test step are restored at the end of this debugging session.

Author: disteph

.github/workflows/windows_ci.yml

@@ -6,10 +6,15 @@ on:
 jobs:
   build:
     strategy:
+      # TEMP: while debugging the windows-latest|release|--enable-thread-safety
+      # --enable-mcsat failure in mcsat_tuples.exe, restrict the matrix to only
+      # the failing config so each iteration takes ~10 minutes instead of an hour.
+      # Restore the full matrix [debug, release] x [' ', --enable-thread-safety,
+      # --enable-thread-safety --enable-mcsat] once the failure is fixed.
       matrix:
         os: [windows-latest]
-        mode: [debug, release]
-        config-opt: [' ', --enable-thread-safety, --enable-thread-safety --enable-mcsat]
+        mode: [release]
+        config-opt: [--enable-thread-safety --enable-mcsat]
 
     name: ${{ matrix.os }}|${{ matrix.mode }}|${{ matrix.config-opt}}
     runs-on: ${{ matrix.os }}
@@ -94,11 +99,19 @@ jobs:
         export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH} &&
         make OPTION=mingw64 MODE=${{ matrix.mode }}
 
-    - name: Run Yices API Tests
+    # TEMP: while debugging the mcsat_tuples failure, run only check-api
+    # (the API tests, which include mcsat_tuples) with YICES_PP_TRACE=1 so
+    # the verbose MCSAT preprocessor diagnostics are emitted. We skip the
+    # `make test` regression suite (much slower and not relevant to this
+    # bug) to keep iteration time short. Restore the full
+    #   make OPTION=mingw64 MODE=... check-api &&
+    #   make OPTION=mingw64 MODE=... test
+    # step once the failure is fixed.
+    - name: Run Yices API Tests (with PP diagnostics)
       shell: bash
       env:
         CYGWIN: winsymlinks:native binmode
+        YICES_PP_TRACE: "1"
       run: >-
         export PATH=/tools/dynamic_gmp/bin:/tools/static_gmp/bin:$PATH &&
-        make OPTION=mingw64 MODE=${{ matrix.mode }} check-api &&
-        make OPTION=mingw64 MODE=${{ matrix.mode }} test
+        make OPTION=mingw64 MODE=${{ matrix.mode }} check-api

src/mcsat/preprocessor.c

@@ -40,6 +40,24 @@
 #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);
@@ -2461,43 +2479,35 @@ 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;
-  fprintf(stderr, "[build_value_from_flat] enter tau=%d idx=%u\n", (int) tau, (unsigned) *idx);
-  fflush(stderr);
+  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;
-    fprintf(stderr, "[build_value_from_flat] TUPLE n=%u\n", (unsigned) n);
-    fflush(stderr);
+    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) {
-        fprintf(stderr, "[build_value_from_flat] TUPLE elem %u null\n", (unsigned) i);
-        fflush(stderr);
+        PP_DIAG("[build_value_from_flat] TUPLE elem %u null\n", (unsigned) i);
         return null_value;
       }
     }
-    fprintf(stderr, "[build_value_from_flat] TUPLE calling vtbl_mk_tuple\n");
-    fflush(stderr);
+    PP_DIAG("[build_value_from_flat] TUPLE calling vtbl_mk_tuple\n");
     value_t r = vtbl_mk_tuple(vtbl, n, elem);
-    fprintf(stderr, "[build_value_from_flat] TUPLE vtbl_mk_tuple -> %d\n", (int) r);
-    fflush(stderr);
+    PP_DIAG("[build_value_from_flat] TUPLE vtbl_mk_tuple -> %d\n", (int) r);
     return r;
   } else if (type_kind(types, tau) == FUNCTION_TYPE) {
     uint32_t n = type_leaf_count(pre, tau);
-    fprintf(stderr, "[build_value_from_flat] FUNCTION n_leaves=%u\n", (unsigned) n);
-    fflush(stderr);
+    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;
-    fprintf(stderr, "[build_value_from_flat] FUNCTION merge -> %d new_idx=%u\n", (int) v, (unsigned) *idx);
-    fflush(stderr);
+    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)++;
-    fprintf(stderr, "[build_value_from_flat] LEAF v=%d new_idx=%u\n", (int) v, (unsigned) *idx);
-    fflush(stderr);
+    PP_DIAG("[build_value_from_flat] LEAF v=%d new_idx=%u\n", (int) v, (unsigned) *idx);
     return v;
   }
 }
@@ -2696,30 +2706,26 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
   uint32_t i;
 
   /* TEMP DIAG (windows release+thread-safety mcsat_tuples failure) */
-  fprintf(stderr, "[pp_build_tuple] enter, atoms=%u\n",
+  PP_DIAG("[pp_build_tuple] enter, atoms=%u\n",
           (unsigned) pre->tuple_blast_atoms.size);
-  fflush(stderr);
   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;
 
-    fprintf(stderr, "[pp_build_tuple] i=%u atom=%d tau=%d\n",
+    PP_DIAG("[pp_build_tuple] i=%u atom=%d tau=%d\n",
             (unsigned) i, (int) atom, (int) tau);
-    fflush(stderr);
 
     if (model_find_term_value(model, atom) != null_value) {
-      fprintf(stderr, "[pp_build_tuple]   atom already mapped, continue\n");
-      fflush(stderr);
+      PP_DIAG("[pp_build_tuple]   atom already mapped, continue\n");
       continue;
     }
 
     init_ivector(&leaves, 0);
     tuple_blast_get(pre, atom, &leaves);
     n = leaves.size;
-    fprintf(stderr, "[pp_build_tuple]   n_leaves=%u\n", (unsigned) n);
-    fflush(stderr);
+    PP_DIAG("[pp_build_tuple]   n_leaves=%u\n", (unsigned) n);
     if (n == 0) {
       delete_ivector(&leaves);
       continue;
@@ -2728,12 +2734,10 @@ 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) {
-      fprintf(stderr, "[pp_build_tuple]   j=%u leaf=%d\n",
+      PP_DIAG("[pp_build_tuple]   j=%u leaf=%d\n",
               (unsigned) j, (int) leaves.data[j]);
-      fflush(stderr);
       value_t v = model_get_term_value(model, leaves.data[j]);
-      fprintf(stderr, "[pp_build_tuple]     model_get_term_value -> %d\n", (int) v);
-      fflush(stderr);
+      PP_DIAG("[pp_build_tuple]     model_get_term_value -> %d\n", (int) v);
       if (v < 0) {
         /* The blasted leaf was never assigned a value by the mcsat
          * search (typical for unconstrained tuple components) and
@@ -2745,21 +2749,18 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
          * vtbl_make_object handles bool / arith / bv / tuple /
          * function / scalar uniformly. */
         type_t leaf_tau = term_type(pre->terms, leaves.data[j]);
-        fprintf(stderr, "[pp_build_tuple]     leaf_tau=%d, calling vtbl_make_object\n",
+        PP_DIAG("[pp_build_tuple]     leaf_tau=%d, calling vtbl_make_object\n",
                 (int) leaf_tau);
-        fflush(stderr);
         v = vtbl_make_object(vtbl, leaf_tau);
-        fprintf(stderr, "[pp_build_tuple]     vtbl_make_object -> %d\n", (int) v);
-        fflush(stderr);
+        PP_DIAG("[pp_build_tuple]     vtbl_make_object -> %d\n", (int) v);
         if (v < 0) {
           ok = false;
           break;
         }
       }
       leaf_vals[j] = v;
     }
-    fprintf(stderr, "[pp_build_tuple]   leaf loop done, ok=%d\n", (int) ok);
-    fflush(stderr);
+    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
@@ -2778,11 +2779,9 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
     }
 
     if (type_kind(types, tau) == FUNCTION_TYPE) {
-      fprintf(stderr, "[pp_build_tuple]   FUNCTION_TYPE branch\n");
-      fflush(stderr);
+      PP_DIAG("[pp_build_tuple]   FUNCTION_TYPE branch\n");
       value_t f = merge_blasted_function_value(pre, vtbl, tau, leaf_vals, n);
-      fprintf(stderr, "[pp_build_tuple]   merge_blasted_function_value -> %d\n", (int) f);
-      fflush(stderr);
+      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")) {
@@ -2793,20 +2792,16 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
         trace_term_ln(pre->tracer, pre->terms, atom);
       }
     } else {
-      fprintf(stderr, "[pp_build_tuple]   non-FUNCTION branch, calling build_value_from_flat\n");
-      fflush(stderr);
+      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);
-      fprintf(stderr, "[pp_build_tuple]   build_value_from_flat -> %d (idx=%u)\n",
+      PP_DIAG("[pp_build_tuple]   build_value_from_flat -> %d (idx=%u)\n",
               (int) v, (unsigned) idx);
-      fflush(stderr);
       if (v >= 0) {
-        fprintf(stderr, "[pp_build_tuple]   model_map_term(atom=%d, v=%d)\n",
+        PP_DIAG("[pp_build_tuple]   model_map_term(atom=%d, v=%d)\n",
                 (int) atom, (int) v);
-        fflush(stderr);
         model_map_term(model, atom, v);
-        fprintf(stderr, "[pp_build_tuple]   model_map_term OK\n");
-        fflush(stderr);
+        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 ");
@@ -2817,11 +2812,9 @@ void preprocessor_build_tuple_model(preprocessor_t* pre, model_t* model) {
     }
 
     delete_ivector(&leaves);
-    fprintf(stderr, "[pp_build_tuple]   end of iteration i=%u\n", (unsigned) i);
-    fflush(stderr);
+    PP_DIAG("[pp_build_tuple]   end of iteration i=%u\n", (unsigned) i);
   }
-  fprintf(stderr, "[pp_build_tuple] exit\n");
-  fflush(stderr);
+  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);
@@ -3065,15 +3058,13 @@ void preprocessor_build_model(preprocessor_t* pre, model_t* model) {
   evaluator_t eval;
   bool eval_inited = false;
   /* TEMP DIAG (windows release+thread-safety mcsat_tuples failure) */
-  fprintf(stderr, "[pp_build_model] enter, has_alias=%d, eqs=%u\n",
+  PP_DIAG("[pp_build_model] enter, has_alias=%d, eqs=%u\n",
           (int) model->has_alias, (unsigned) pre->equalities_list.size);
-  fflush(stderr);
   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);
-    fprintf(stderr, "[pp_build_model] i=%u eq=%d eq_var=%d\n",
+    PP_DIAG("[pp_build_model] i=%u eq=%d eq_var=%d\n",
             (unsigned) i, (int) eq, (int) eq_var);
-    fflush(stderr);
     if (trace_enabled(pre->tracer, "mcsat::preprocess")) {
       mcsat_trace_printf(pre->tracer, "eq = ");
       trace_term_ln(pre->tracer, pre->terms, eq);
@@ -3084,29 +3075,24 @@ 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) {
-      fprintf(stderr, "[pp_build_model]   already mapped, continue\n");
-      fflush(stderr);
+      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) {
-      fprintf(stderr, "[pp_build_model]   not solved, continue\n");
-      fflush(stderr);
+      PP_DIAG("[pp_build_model]   not solved, continue\n");
       continue;
     }
     term_kind_t eq_kind = term_kind(pre->terms, eq);
-    fprintf(stderr, "[pp_build_model]   eq_kind=%d\n", (int) eq_kind);
-    fflush(stderr);
+    PP_DIAG("[pp_build_model]   eq_kind=%d\n", (int) eq_kind);
     composite_term_t* eq_desc = get_composite(pre->terms, eq_kind, eq);
-    fprintf(stderr, "[pp_build_model]   eq_desc=%p arity=%u\n",
+    PP_DIAG("[pp_build_model]   eq_desc=%p arity=%u\n",
             (void*) eq_desc, eq_desc ? (unsigned) eq_desc->arity : 0u);
-    fflush(stderr);
     term_t eq_subst = eq_desc->arity > 1
       ? (eq_desc->arg[0] == eq_var ? eq_desc->arg[1] : eq_desc->arg[0])
       : zero_term;
-    fprintf(stderr, "[pp_build_model]   eq_subst=%d\n", (int) eq_subst);
-    fflush(stderr);
+    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). */
@@ -3125,31 +3111,25 @@ 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) {
-        fprintf(stderr, "[pp_build_model]   init_evaluator\n"); fflush(stderr);
+        PP_DIAG("[pp_build_model]   init_evaluator\n");
         init_evaluator(&eval, model);
         eval_inited = true;
-        fprintf(stderr, "[pp_build_model]   init_evaluator OK\n"); fflush(stderr);
+        PP_DIAG("[pp_build_model]   init_evaluator OK\n");
       }
-      fprintf(stderr, "[pp_build_model]   eval_in_model(%d)\n", (int) eq_subst);
-      fflush(stderr);
+      PP_DIAG("[pp_build_model]   eval_in_model(%d)\n", (int) eq_subst);
       value_t v = eval_in_model(&eval, eq_subst);
-      fprintf(stderr, "[pp_build_model]   eval_in_model -> v=%d\n", (int) v);
-      fflush(stderr);
+      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);
-        fprintf(stderr, "[pp_build_model]   vtbl_make_object(tau=%d)\n", (int) eq_var_tau);
-        fflush(stderr);
+        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);
-        fprintf(stderr, "[pp_build_model]   vtbl_make_object -> v=%d\n", (int) v);
-        fflush(stderr);
+        PP_DIAG("[pp_build_model]   vtbl_make_object -> v=%d\n", (int) v);
       }
       if (v >= 0) {
-        fprintf(stderr, "[pp_build_model]   model_map_term(eq_var=%d, v=%d)\n",
+        PP_DIAG("[pp_build_model]   model_map_term(eq_var=%d, v=%d)\n",
                 (int) eq_var, (int) v);
-        fflush(stderr);
         model_map_term(model, eq_var, v);
-        fprintf(stderr, "[pp_build_model]   model_map_term OK\n");
-        fflush(stderr);
+        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 ");
@@ -3159,15 +3139,14 @@ void preprocessor_build_model(preprocessor_t* pre, model_t* model) {
   }
 
   if (eval_inited) {
-    fprintf(stderr, "[pp_build_model] delete_evaluator\n"); fflush(stderr);
+    PP_DIAG("[pp_build_model] delete_evaluator\n");
     delete_evaluator(&eval);
-    fprintf(stderr, "[pp_build_model] delete_evaluator OK\n"); fflush(stderr);
+    PP_DIAG("[pp_build_model] delete_evaluator OK\n");
   }
 
-  fprintf(stderr, "[pp_build_model] calling preprocessor_build_tuple_model\n");
-  fflush(stderr);
+  PP_DIAG("[pp_build_model] calling preprocessor_build_tuple_model\n");
   preprocessor_build_tuple_model(pre, model);
-  fprintf(stderr, "[pp_build_model] exit\n"); fflush(stderr);
+  PP_DIAG("[pp_build_model] exit\n");
 }