SRI-CSL / yices2
67%
master: 71%

LAST BUILD BRANCH: fix-417-smt2-string-escape
DEFAULT BRANCH: master
Repo Added
Files 496
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst

LAST BUILD ON BRANCH mcsat-tuples-support
branch: mcsat-tuples-support
CHANGE BRANCH
x

coverage: 67.079% (+0.4%) from 66.687%
25541287601

Pull #606

github

web-flow 
Merge 9f29aab3b into 7878664a0
Pull Request #606: MCSAT: add support for tuples (incl. nested with function types); blasts tuples in input constraints + reconstitutes them in models and interpolants

788 of 1063 new or added lines in 3 files covered. (74.13%)

84651 of 126196 relevant lines covered (67.08%)

1631915.28 hits per line

Relevant lines Covered
126196 RELEVANT LINES 84651 COVERED LINES
1631915.28 HITS PER LINE
Source Files on mcsat-tuples-support

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
25541287601 mcsat-tuples-support Merge 9f29aab3b into 7878664a0 Pull #606 web-flow github
67.08
25541286667 mcsat-tuples-support mcsat: fix stale lifetime comment on label-substitution helper The comment claimed the substitution runs 'before popping the temporary context frame', but the caller in context_solver.c pops first, then calls this helper. Rewrite the comment to m... push disteph github
67.08
25538560463 mcsat-tuples-support mcsat: avoid evaluating unmapped tuple-blast leaves Pull #606 disteph github
67.08
25536264253 mcsat-tuples-support Merge f7f89fbdb into 7878664a0 Pull #606 web-flow github
67.09
25536263059 mcsat-tuples-support 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... push disteph github
67.09
25530974729 mcsat-tuples-support tests: TEMP per-step trace inside test_partial_tuple_model_no_keep_subst The previous instrumentation pinpointed test_partial_tuple_model_no_keep_subst as the test that aborts on windows-latest|release|--enable-thread-safety --enable-mcsat. The c... Pull #606 disteph github
67.08
25528891542 mcsat-tuples-support 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/rele... Pull #606 disteph github
67.08
25524988749 mcsat-tuples-support tests: actually exercise ARITH_CEIL dispatch in tuple_unary_arith.ys The previous header claimed the .ys file covered ARITH_CEIL alongside ARITH_FLOOR / ARITH_IS_INT_ATOM / ARITH_ABS, but no ceil assertion was present. The original assumption was... Pull #606 disteph github
67.08
25366656949 mcsat-tuples-support mcsat: extend zero-copy peek to all read-only single-leaf sites (L4) Convert the remaining tuple_blast_get call sites whose only use of the returned snapshot is a (size==1, data[0]) read to tuple_blast_peek: NOT, SELECT, OR/XOR, POWER_PRODUCT, AR... Pull #606 disteph github
66.95
25365016246 mcsat-tuples-support mcsat: trace dropped atoms in preprocessor_build_tuple_model preprocessor_build_tuple_model has three paths along which a tuple-blasted atom can quietly fail to appear in the reconstructed model: 1. one of the blasted leaf variables has no val... Pull #606 disteph github
66.88
See All Builds (2105)