Skip to content

fix(SMT): restrict get-value to primitive types for cvc5 #679

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
shigoel wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

fix(SMT): restrict get-value to primitive types for cvc5 #679

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9822761
fix(SMT): restrict get-value to primitive types to avoid cvc5 abort
shigoel Mar 26, 2026
a95640e
Merge branch 'main' into shilpi/cvc5-get-value-fix
shigoel Mar 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion Strata/Languages/Core/Verifier.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,8 +64,14 @@ def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit)
-- Encode the obligation term Q (not negated)
let (obligationId, estate) ← (encodeTerm False obligationTerm) |>.run estate

-- Only request get-value for nullary UFs with primitive output types.
-- cvc5 fatally aborts ("cannot get domain elements") when get-value targets
-- an uninterpreted sort after unsat. Restricting to primitive types avoids
-- this and still preserves model info for the most useful variables.
-- TODO: this is conservative - cvc5 handles datatypes fine after unsat,
-- so we could also include constr types that don't involve uninterpreted sorts.
let ids := estate.ufs.toList.filterMap fun (uf, id) =>
if uf.args.isEmpty then some id else none
if uf.args.isEmpty && uf.out.isPrimType then some id else none

-- Choose encoding strategy: use check-sat-assuming only when doing both checks
let bothChecks := satisfiabilityCheck && validityCheck
Expand Down
Loading