• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

SRI-CSL / yices2 / 25365016246
67%
master: 67%

Build:
Build:
LAST BUILD BRANCH: mcsat-supplement-cdclt
DEFAULT BRANCH: master
Ran 05 May 2026 08:16AM UTC
Jobs 1
Files 486
Run time 2min
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

05 May 2026 08:06AM UTC coverage: 66.883% (+0.2%) from 66.687%
25365016246

Pull #606

github

disteph
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 value in the trail,
  2. the function-type merge in merge_blasted_function_value returns
     null_value for one of several structural reasons (leaf value is
     neither a function nor an update object, a map's arity does not
     match the flattened domain, or a sub-call to build_value_from_flat
     could not rebuild a codomain / domain / default value),
  3. the non-function tuple merge in build_value_from_flat itself
     returns null_value.

Under the previous code each of these branches just `continue`'d or
returned null_value and the caller conditionally invoked
model_map_term only on success. A user inspecting (show-model) would
see the atom missing with no signal anywhere as to why.

Emit a short line under the existing "mcsat::preprocess" trace tag at
each drop site:

  - the leaf-missing case in preprocessor_build_tuple_model names the
    atom and the leaf index that is unassigned;
  - merge_blasted_function_value records a short reason string at each
    of its five `goto done` exits (via a local fail_reason variable
    set immediately before the jump), and emits it from the single
    cleanup label; the caller then adds the concrete atom term;
  - the tuple (non-function) branch in preprocessor_build_tuple_model
    names the atom and notes that the leaves did not decompose.

trace_enabled is a no-op in NDEBUG, so release builds pay nothing at
runtime. mcsat_trace_printf and trace_term_ln are already used from
this file under the same tag, so no new headers or dependencies.

No semantic change to the rebuilt model; the 31 api tests and the 8
tuple .ys regressions still pass in debug, sanitize, and release.
Pull Request #606: MCSAT: add support for tuples (incl. nested with function types); blasts tuples in input constraints + reconstitutes them in models and interpolants

721 of 967 new or added lines in 3 files covered. (74.56%)

65 existing lines in 1 file now uncovered.

84342 of 126103 relevant lines covered (66.88%)

1633298.86 hits per line

Uncovered Changes

Lines Coverage ∆ File
246
81.26
-9.19% src/mcsat/preprocessor.c

Coverage Regressions

Lines Coverage ∆ File
65
81.26
-9.19% src/mcsat/preprocessor.c
Jobs
ID Job ID Ran Files Coverage
1 25365016246.1 05 May 2026 08:16AM UTC 486
66.88
GitHub Action Run
Source Files on build 25365016246
  • Tree
  • List 486
  • Changed 12
  • Source Changed 0
  • Coverage Changed 12
Coverage ∆ File Lines Relevant Covered Missed Hits/Line
  • Back to Repo
  • Pull Request #606
  • PR Base - master (#25307519190)
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc