Add notes on choosing Z3 or Bitwuzla, and note on setting EXTERNAL_SAT_SOLVER

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

Author: rod-chapman

cbmc/proofs/proof_guide.md

@@ -218,12 +218,28 @@ Edit the Makefile and update the definition of the following variables:
 * PROJECT_SOURCES - should the files containing the source code of XXX
 * CHECK_FUNCTION_CONTRACTS - set to the `XXX`, but _with_ the `$(MLKEM_NAMESPACE)` prefix if required
 * USE_FUNCTION_CONTRACTS - a list of functions that `XXX` calls where you want CBMC to use the contracts of the called function for proof, rather than 'inlining' the called function for proof. Include the `$(MLKEM_NAMESPACE)` prefix if required
+* EXTERNAL_SAT_SOLVER - should _always_ be "nothing" to prevent CBMC selecting a SAT backend over the selected SMT backend.
 * CBMCFLAGS - additional flags to pass to the final run of CBMC. This is normally set to `--smt2` which tells cbmc to run Z3 as its underlying solver. Can also be set to `--bitwuzla` which is sometimes better at generaing counter-examples when Z3 fails.
 * FUNCTION_NAME - set to `XXX` with the `$(MLKEM_NAMESPACE)` prefix if required
 * CBMC_OBJECT_BITS. Normally set to 8, but might need to be increased if CBMC runs out of memory for this proof.
 
 For documentation of these (and the other) options, see the `cbmc/proofs/Makefile.common` file.
 
+#### Z3 or Bitwuzla?
+
+I have found that it's better to use Bitwuzla in the initial stages of developing and debugging a new proof.
+
+When Z3 finds that a proof is "sat" (i.e. not true), it tries to produce a counter-example to show you what's wrong. Unfortunately, recent versions of Z3 can produce quantified expressions as output that cannot be currently understood by CBMC. This leads CBMC to fail with an error such as
+
+```
+SMT2 solver returned non-constant value for variable Bxxx
+```
+
+This is not helpful when trying to understand a failed proof. Bitwuzla works better and produces reliable counter-examples.
+
+Once a proof is working OK, I revert to Z3 to check it _also_ works with Z3. If it does, then I keep Z3 as the selected prover. If not, then stick with Bitwuzla.
+
+
 ### Update harness function
 
 The file `XXX_harness.c` should declare a single function called `XXX_harness()` that calls `XXX` exactly one, with appropriately typed parameters. Using contracts, this harness function should not need to contain any CBMC `ASSUME` or `ASSERT` statements at all.