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

SRI-CSL / yices2 / 25267023082
69%

Build:
DEFAULT BRANCH: master
Ran 03 May 2026 01:56AM UTC
Jobs 1
Files 486
Run time 1min
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

03 May 2026 01:47AM UTC coverage: 66.685% (+0.1%) from 66.539%
25267023082

push

github

web-flow
Fix #613 MCSAT curried function model reconstruction (#614)

* Fix MCSAT curried function model reconstruction

* Fix both-regression baseline solver invocation

* Make curried MCSAT API test NDEBUG-safe

* Enable asserts in curried MCSAT API test

* Add MCSAT SMT2 regression for issue 613

* Fix use-after-free and related issues in MCSAT curried function model

Builds on b2c49c80 (Fix MCSAT curried function model reconstruction) with
several independent fixes in uf_model_builder_get_function_value,
uf_plugin_build_model, and the concrete-value printer.

1. uf_model_builder_get_function_value: use-after-free on int_hmap_pair_t*

   The function cached `find = int_hmap_get(function_value, fid)` before
   recursing into uf_model_builder_get_term_value, then wrote
   `find->val = f_value` after the recursion returned. The recursive call
   can reach int_hmap_get again for a different function id; when that
   call crosses the load-factor threshold, int_hmap_extend reallocates
   (and free()s) the bucket array, invalidating any previously held
   int_hmap_pair_t*. Writing through the stale pointer is a classic
   heap-use-after-free.

   ASan confirms this on tests/regress/mcsat/arrays/issue613_many_curried.smt2:

     ERROR: AddressSanitizer: heap-use-after-free
     WRITE of size 4 at 0x61100001fca4
       #0 uf_model_builder_get_function_value (stale find->val write)
     freed by thread T0:
       #1 int_hmap_extend int_hash_map.c:173
       #2 int_hmap_get   int_hash_map.c:265
       #3 uf_model_builder_get_function_value (recursive call)

   Fix: after the recursion, re-fetch the pair with int_hmap_get and
   assign directly; null out the stale `find` to document the invariant
   and prevent future reuse.

2. uf_model_builder_get_function_value: finite-domain null_value assert

   make_fresh_function can legitimately return null_value when the
   domain/range types are both finite and already saturated in the
   value table. The previous code had as... (continued)

179 of 195 new or added lines in 4 files covered. (91.79%)

9 existing lines in 6 files now uncovered.

83429 of 125109 relevant lines covered (66.69%)

1695673.88 hits per line

Uncovered Changes

Lines Coverage ∆ File
6
91.32
2.81% src/mcsat/uf/uf_plugin.c
4
86.18
0.66% src/frontend/smt2/smt2_printer.c
4
35.4
24.58% src/io/concrete_value_printer.c
2
92.01
-0.26% src/mcsat/preprocessor.c

Coverage Regressions

Lines Coverage ∆ File
2
91.32
2.81% src/mcsat/uf/uf_plugin.c
2
68.48
-0.61% src/mcsat/value.c
2
67.19
0.66% src/model/concrete_values.c
1
86.18
0.66% src/frontend/smt2/smt2_printer.c
1
35.4
24.58% src/io/concrete_value_printer.c
1
92.01
-0.26% src/mcsat/preprocessor.c
Jobs
ID Job ID Ran Files Coverage
1 25267023082.1 03 May 2026 01:56AM UTC 486
66.69
GitHub Action Run
Source Files on build 25267023082
  • Tree
  • List 486
  • Changed 10
  • Source Changed 0
  • Coverage Changed 10
Coverage ∆ File Lines Relevant Covered Missed Hits/Line
  • Back to Repo
  • 485acafd on github
  • Prev Build on master (#23861667837)
  • Next Build on master (#25302889838)
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