From 982276120fd5c81409c88610283be5a647252a5f Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Thu, 26 Mar 2026 14:36:09 -0500 Subject: [PATCH] fix(SMT): restrict get-value to primitive types to avoid cvc5 abort MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit cvc5 fatally aborts ("cannot get domain elements") when get-value targets a variable of an uninterpreted sort after an unsat check-sat. This caused spurious "Internal error" results in pyAnalyzeLaurel with two-sided checking (--check-level full). Filter the get-value variable list to only include nullary UFs with primitive output types (Int, Bool, String, etc.), which are always safe. This is conservative — datatypes are also safe, but we leave that as a future refinement. Co-Authored-By: Claude Opus 4.6 (1M context) --- Strata/Languages/Core/Verifier.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean index 791d85604..dbbef33ab 100644 --- a/Strata/Languages/Core/Verifier.lean +++ b/Strata/Languages/Core/Verifier.lean @@ -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