Use custom Z3 switch in proof of this function.

1. Adds Z3 wrapper z3_no_bv_extract that adds the
   rewriter.bv_le2extract=false option when invoking Z3.
   See Z3 Issue 7991 for recommendation to use this.
2. Updates Makefile for this function to use
   that wrapper.

Signed-off-by: Rod Chapman <[email protected]>

Author: rod-chapman

proofs/cbmc/attempt_signature_generation/Makefile

@@ -50,7 +50,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
+CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
 CBMCFLAGS += --slice-formula
 CBMCFLAGS += --no-array-field-sensitivity
 

proofs/cbmc/lib/z3_no_bv_extract

@@ -0,0 +1,7 @@
+#!/bin/bash
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+# Disable re-writing of bit-vector expressions within quantifiers.
+# Such re-writing can cause quantifier e-matching to fail in complex cases.
+z3 rewriter.bv_le2extract=false "$@"