CBMC: Stabilize proof of polyvecl_pointwise_acc_montgomery

1. Introduce z3_smt_only wrapper that sets tactic.default_tactic=smt
2. Use that script in CBMC proof of polyvecl_pointwise_acc_montgomery

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

proofs/cbmc/lib/z3_smt_only

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Copyright (c) The mldsa-native project authors
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+# Disable initial simplify tactic and go straight to main SMT tactic
+# This can prevent divergence of Z3 on different platforms
+z3 tactic.default_tactic=smt "$@"

proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile

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