Solver configuration fixes - #180
Merged
Merged
Conversation
KContext.mkArrayConst is internalized as cvc5's STORE_ALL, which cvc5
refuses unless the arrays-exp option is set:
Cannot handle assertion with term of kind STORE_ALL in this
configuration. Try --arrays-exp.
So ksmt emitted terms its own solver rejects. It went unnoticed because
cvc5's rewriter eliminates the const array in most shapes: only a store
over a const array, read back at a symbolic index, survives to the check.
Set the option alongside fp-exp, which is the same kind of opt-in.
On the Linux natives ksmt ships, the rejection did not even surface as a
CVC5ApiException: libcvc5, libcvc5parser and libcvc5jni each statically
link their own libstdc++, so the exception could not be unwound across
the library boundary and the unwinder called abort(). The JVM does not
trap SIGABRT, so the process died at exit code 134 with no diagnostic.
That packaging issue is not addressed here and is why ConstArrayTest has
no negative test - a JUnit worker does not survive the unset case.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
fp-exp and arrays-exp were set on every solver, whether or not the query could contain a floating-point sort or a const array. Both are cvc5 experimental extensions, so enabling them unconditionally opts every query into behaviour it does not need. Gate them on the theory set passed to optimizeForTheories. A caller that does not call it declares nothing about the query, so both options are still set - that stays the default. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
KZ3ExprInternalizer keeps uninterpreted sort values distinct by mapping
each to a distinct value of a descriptor sort, so every query carries
constraints over that sort whichever theories the caller declared.
optimizeForTheories derived the logic from the caller's theory set alone,
so the declared logic and the actual benchmark disagreed, and Z3 failed
in one of two ways, neither naming the logic:
- UNKNOWN, "Benchmark constrains arithmetic, but specified logic does not
support it" - QF_UF, QF_LRA and QF_NRA;
- or SAT with the descriptor sort treated as uninterpreted, which put it
in Z3_model_get_sort and made KZ3Model.uninterpretedSorts throw
ClassCastException: KIntSort cannot be cast to KUninterpretedSort -
every logic containing bitvectors.
7 of the 26 emittable combinations were affected. {UF, Array, BV} is a
complete declaration of such a caller's own theories and still failed,
because the caller cannot declare a theory ksmt adds on its own behalf.
resolveLogic now picks the logic and the descriptor sort together: a
bitvector descriptor when the theory set has BV and no integer
arithmetic, otherwise an integer one, adding LIA only when neither LIA
nor NIA is present. Combinations with no specialized Z3 solver fall back
to the general solver, which accepts either descriptor.
21 of 26 keep a specialized logic. QF_AX, QF_LRA and QF_UF widen to
QF_ALIA, QF_LIRA and QF_UFLIA; QF_FP, QF_FPLRA, QF_UFLRA and QF_UFNRA
fall back, since whether a logic tolerates a sort it does not declare is
per-logic Z3 behaviour that cannot be derived from the theory set.
assert internalizes before it touches solver, so exprInternalizer now
forces solver creation to resolve the configuration first.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Same defect as the Z3 one, in KCvc5ExprInternalizer: uninterpreted sort values are kept distinct by mapping each to a distinct value of a descriptor sort, so every query carries constraints over that sort whichever theories the caller declared. optimizeForTheories derived the logic from the caller's theory set alone, and cvc5 then rejected the check under QF_UF, QF_UFBV, QF_AUFBV, QF_AX and QF_ABV among others. Worse than on Z3: cvc5 has no supported-combination filter, so any generated logic reaches setLogic, and the rejection cannot unwind out of the shipped Linux natives, so it killed the process at exit code 134 with no diagnostic instead of raising CVC5ApiException. optimizeForTheories now picks the logic and the descriptor sort together, with the same rule as Z3: a bitvector descriptor when the theory set has BV and no integer arithmetic, otherwise an integer one, adding LIA only when neither LIA nor NIA is present. An empty theory set keeps QF_SAT, since it declares no theory that could carry an uninterpreted sort. All 17 combinations under which an uninterpreted sort is legal now check and produce a readable model; previously 13 of 29 aborted. Sets that declare neither UF nor Array still fail, but there the query is outside the declared logic and cvc5 is right to reject it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Saloed
force-pushed
the
solver-configuration-fixes
branch
from
August 11, 2026 21:55
a7c2236 to
2af5e8f
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.
.