Repository navigation
[TS] Use Yices for all TypeScript machines - #417
Merged
Merged
Conversation
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-v4
branch
from
October 13, 2026 03:10
eec98e9 to
da16021
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-yices
branch
from
October 13, 2026 03:16
5736a5b to
6f03fe8
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-v4
branch
from
October 13, 2026 03:27
da16021 to
30a2182
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-yices
branch
from
October 13, 2026 03:31
6f03fe8 to
85c8e98
Compare
CaelmBleidd
marked this pull request as ready for review
October 13, 2026 03:44
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-yices
branch
from
October 13, 2026 21:31
85c8e98 to
72e3520
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-v4
branch
from
October 13, 2026 21:31
30a2182 to
350fbd4
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-v4
branch
3 times, most recently
from
October 13, 2026 22:24
42cf036 to
7c7029e
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-yices
branch
from
October 13, 2026 22:39
72e3520 to
f46dd82
Compare
CaelmBleidd
changed the title
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-yices
branch
from
October 13, 2026 23:01
f46dd82 to
44370a3
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/iccq-coverage-yices
branch
from
October 13, 2026 23:03
44370a3 to
425e335
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
All TypeScript symbolic execution now uses Yices with SymFPU. The shared TypeScript solver factory creates only Yices, and TsMachine records Yices in its effective options even when a caller supplies the general machine options' Z3 selection. Other machine settings are preserved. Calls and PBT entry points also select Yices explicitly; Calls manifests reject any other solver so recorded experiment identity matches execution.
Coverage cells bind the solver, build revision and frontend revision to their persisted identity. They reject mismatched builds, frontends, solvers and prior cell schemas before search or replay. Based on current main, including merged #416.
Local validation on JDK 21:
GitHub CI for the new head is still running. These checks do not establish a completed coverage measurement campaign.