Apply and demo --external-smt2-solver in CBMC proof of polyvec_add()

1. Adds new Z3 "wrapper" scripts z3_smt_only and z3_bv_sort in
   proofs/cbmc/lib
2. Update the Makefile for the proof of polyvec_add() to
   select "z3_bv_sort" prover wrapper.
3. Update Proof Guide to explain how --external-smt2-solver works.

On r7g instance, proof time when K=4 reduces from 300 to 100s.

Signed-off-by: Rod Chapman <rodchap@amazon.com>
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: rod-chapman

proofs/cbmc/lib/z3_bv_sort

@@ -0,0 +1,4 @@
+#!/bin/bash
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+z3 rewriter.bv_sort_ac=true "$@"

proofs/cbmc/lib/z3_smt_only

@@ -0,0 +1,4 @@
+#!/bin/bash
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+z3 tactic.default_tactic=smt "$@"

proofs/cbmc/polyvec_add/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=--smt2
+CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_bv_sort --z3
 
 # For this proof we tell CBMC to
 #  - not decompose arrays into their individual cells

proofs/cbmc/proof_guide.md

@@ -357,6 +357,40 @@ This is not helpful when trying to understand a failed proof. Bitwuzla works bet
 Once a proof is working OK, you may revert to Z3 to check if it _also_ passes with Z3, and perhaps faster. If it does,
 then keep Z3 as the selected prover. If not, then stick with Bitwuzla.
 
+#### Selecting custom options for Z3 or Bitwuzla
+
+By default, CBMC invokes provers with no special command-line options. If you want to pass additional flags to the prover,
+e.g. to improve proof performance, you can create a small wrapper script and pass it to CBMC via `--external-smt2-solver XXX` (introduced in 6.8.0).
+
+An example of such a script is [lib/z3_smt_only](lib/z3_smt_only) which looks like this:
+
+```
+#!/bin/bash
+z3 tactic.default_tactic=smt "$@"
+```
+
+There is also a script [lib/z3_bv_sort](lib/z3_bv_sort) which looks like this:
+
+```
+#!/bin/bash
+z3 rewriter.bv_sort_ac "$@"
+```
+
+Both these extra options have been found to be effective in improving Z3's performance in some cases.
+
+To select the special prover, we update the proof `Makefile` for a particular function, replacing the
+`--smt2` or `--bitwuzla` option with `--external-smt2-solver`.  For example, the proof of
+`polyvec_add()` is much faster using the `z3_bv_sort` wrapper, so we change the `Makefile`, replacing
+
+```
+CBMCFLAGS=--smt2
+```
+with
+```
+CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_bv_sort --z3
+```
+Note that we still need the ``--z3`` option now to inform CBMC to generate SMTLib specifically for Z3.
+
 ### Update harness function
 
 The file `XXX_harness.c` should declare a single function called `XXX_harness()` that calls `XXX` exactly once, with