edits

jakemas · jakemas · commit 8ffcfca2e568 · 2025-05-22T04:20:05.000Z
Signed-off-by: Jake Massimo &lt;jakemas@amazon.com&gt;
diff --git a/mldsa/sign.h b/mldsa/sign.h
@@ -12,7 +12,7 @@
 #include "poly.h"
 #include "polyvec.h"
 
-#define crypto_sign_keypair_internal MLD_NAMESPACE(keypair_internal)
+#define crypto_sign_keypair_internal MLD_NAMESPACE(crypto_sign_keypair_internal)
 /*************************************************
  * Name:        crypto_sign_keypair_internal
  *
diff --git a/proofs/cbmc/crypto_sign_keypair_internal/Makefile b/proofs/cbmc/crypto_sign_keypair_internal/Makefile
@@ -27,13 +27,12 @@ USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256 $(MLD_NAMESPACE)polyvec_matr
 					   $(MLD_NAMESPACE)polyveck_add $(MLD_NAMESPACE)polyveck_caddq \
 					   $(MLD_NAMESPACE)polyveck_power2round $(MLD_NAMESPACE)pack_pk \
 					   $(MLD_NAMESPACE)pack_sk
-					   
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--bitwuzla
+CBMCFLAGS=--smt2
 
 FUNCTION_NAME = crypto_sign_keypair_internal
 

Original file line number	Diff line number	Diff line change
`@@ -12,7 +12,7 @@`
`12`	`12`	`#include "poly.h"`
`13`	`13`	`#include "polyvec.h"`
`14`	`14`
`15`		`-#define crypto_sign_keypair_internal MLD_NAMESPACE(keypair_internal)`
	`15`	`+#define crypto_sign_keypair_internal MLD_NAMESPACE(crypto_sign_keypair_internal)`
`16`	`16`	`/*************************************************`
`17`	`17`	`* Name: crypto_sign_keypair_internal`
`18`	`18`	`*`