Avoid z3 soundness issue #9550

[hanno-becker]

A soundness issue was reported in Z3Prover/z3#9550 which affects the version of Z3 we are using through CBMC.

At this point, it is unclear if the soundness issue is affecting our proofs, but we must either A) update Z3 to a fixed version, or B) update CBMC to a version avoiding the soundness bug, as soon as possible.

[hanno-becker]

• Relates to CBMC: Consider systematically employing multiple SMT solver backends for CBMC functions mlkem-native#1603

[mkannwischer]

Trying current z3 version from their master branch in #1127.

[mkannwischer]

• nix: Pin z3 to upstream commit 286b107 #1127 confirms that our proofs (at current main 4befe1f) still pass with the fixed z3. Hence, the soundsness issue does not affect us. So I don't see a reason to hold back the release due to this issue.

I think updating CBMC once a fixed version has been released is likely the more robust path forward and I hope we can do that before making any further (significant) changes to C code.