Do not use as const with Z3 due to soundness issue#9011
Conversation
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Disables the SMT2 as const array constant construct for the Z3 backend due to a soundness bug in Z3 (Z3Prover/z3#9550) that causes incorrect results.
Changes:
- Set
use_as_const = falsefor the Z3 solver path insmt2_convt's constructor.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #9011 +/- ##
===========================================
- Coverage 80.56% 80.56% -0.01%
===========================================
Files 1707 1707
Lines 189134 189152 +18
Branches 73 73
===========================================
+ Hits 152385 152398 +13
- Misses 36749 36754 +5 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
mlkem-native test results using patched CBMC (and standard Z3 4.15.3) look good. No regressions. A bit slower at K=4, but not too bad. A bit faster for K=2 and K=3. |
|
mldsa-native test results using patched CBMC (and standard Z3 4.15.3) look good. No regressions. A bit faster too for all parameter sets. |
|
I have re-built and re-tested the latest commit on this branch for all parameter set of mlkem-native and mldsa-native. All results are good. Please proceed. |
The unflatten() function reconstructs an SMT-array from a bit-vector by storing each element. It previously required `(as const T)` to build the base constant array, which is unavailable when use_as_const is disabled (as done for Z3 in the next commit due to a soundness issue). Replace with a lambda expression `(lambda ((idx T)) elem0)` that produces the same constant-array value without `as const`. Since Z3 rejects `get-value` on terms containing lambdas, also switch from `define-fun` to `declare-fun` + `assert` for SSA symbol definitions when `use_as_const` is false. This makes the symbol opaque to `get-value` while preserving the same logical constraint. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Disable `as const` for Z3 as it produces wrong results per Z3Prover/z3#9550.
Disable
as constfor Z3 as it produces wrong results per Z3Prover/z3#9550.