Update to tagged build of CBMC 6.10.0

1. Update NIX config for CBMC 6.10.0
2. Revert to Z3 with default options for proof of sign_verify_internal()
   owing to proof performance regressions using z3_no_bv_extract following
   CBMC fix for Z3 soundness issue.

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

Author: rod-chapman

nix/cbmc/default.nix

@@ -15,12 +15,12 @@ buildEnv {
   paths =
     builtins.attrValues {
       cbmc = cbmc.overrideAttrs (_: {
-        version = "6.9.0";
+        version = "6.10.0";
         src = fetchFromGitHub {
           owner = "diffblue";
           repo = "cbmc";
-          hash = "sha256-SMJBnzoyTwcwJa9L2X1iX2W4Z/Mwoirf8EXfoyG0dRI=";
-          tag = "cbmc-6.9.0";
+          hash = "sha256-GCagpb2TFhOEH+lzMth+PWiJxlEw0L+H1DYUEQoMF3g=";
+          tag = "cbmc-6.10.0";
         };
       });
       litani = callPackage ./litani.nix { }; # 1.29.0

proofs/cbmc/sign_verify_internal/Makefile

@@ -46,7 +46,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=--smt2
 
 FUNCTION_NAME = sign_verify_internal