SRI-CSL / yices2 / 25528891542

67%

master: 71%

Build Type

Pull #606

github

Committed by disteph

Commit Message

tests: TEMP diagnostic to pinpoint Windows mcsat_tuples failure

CI fails on windows-latest|release|--enable-thread-safety --enable-mcsat
with `mcsat_tuples.exe FAIL` and no further detail. The failure does not
reproduce on Linux/macOS, debug/release, with or without thread-safety,
and there is no usable log surfaced by the test runner because
tests/api/run_test.sh saves the captured output to ${shortname}.log
in the build dir and CI does not upload that artifact.

This commit is purely diagnostic and is intended to be reverted (or
folded into the actual fix) once the failure is pinpointed:

  1. tests/api/mcsat_tuples.c: wrap each test invocation in a RUN_TEST
     macro that prints "[mcsat_tuples] START <name>" and "OK <name>"
     to stderr (with explicit fflush). The next CI run on Windows will
     show which test was the last to print START before the abort.

  2. tests/api/run_test.sh: on FAIL, dump the captured outfile to
     stderr surrounded by markers. Without this, the START/OK trace
     in (1) would still be invisible in the GitHub Actions log because
     the runner only writes it to a file. Also useful for any future
     test failure under this harness.

Once the failing test is identified from the next CI run, replace this
commit with the actual fix.

Pull Request Pull Request #606: MCSAT: add support for tuples (incl. nested with function types); blasts tuples in input constraints + reconstitutes them in models and interpolants

Coverage Stats

784 of 1059 new or added lines in 3 files covered. (74.03%)

6 existing lines in 1 file now uncovered.

84648 of 126192 relevant lines covered (67.08%)

1642603.15 hits per line