Use z3_smt_only for this proof.

This stabilizes proof time for all parameter sets, with and without
MLD_CONDIG_REDUCE_RAM, and on all platforms.

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

Author: rod-chapman

proofs/cbmc/poly_ntt_c/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=--bitwuzla
+CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3
 
 FUNCTION_NAME = mld_poly_ntt_c