diff --git a/Makefile.examples b/Makefile.examples
index ef62196e2b..ac29748146 100644
--- a/Makefile.examples
+++ b/Makefile.examples
@@ -108,9 +108,13 @@ INVALID_GO_BASE_FILES := $(BASE_FILES_NEEDING_INT128)
 GO_EXTRA_UNSATURATED_SOLINAS_FUNCTIONS := carry_add carry_sub carry_opp
 GO_EXTRA_WORD_BY_WORD_MONTGOMERY_FUNCTIONS :=
 
+# We add a test for --fancy-and-powerful-but-exponentially-slow-bounds-analysis so that it's not dead code.
+# It doesn't really matter which curve we add this flag to, as long as it's fast.
+FANCY_BOUNDS_ANALYSIS_FLAG := --fancy-and-powerful-but-exponentially-slow-bounds-analysis
+
 $(foreach bw,64 32,$(eval $(call add_curve_keys,curve25519_$(bw),UNSATURATED_SOLINAS,'25519',$(bw),'(auto)' '2^255 - 19',$(FUNCTIONS_FOR_25519),UNSATURATED_SOLINAS)))
-$(eval $(call add_curve_keys,poly1305_64,UNSATURATED_SOLINAS,'poly1305',64,'3' '2^130 - 5',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
-$(eval $(call add_curve_keys,poly1305_32,UNSATURATED_SOLINAS,'poly1305',32,'(auto)' '2^130 - 5',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
+$(eval $(call add_curve_keys,poly1305_64,UNSATURATED_SOLINAS,'poly1305',64,'3' '2^130 - 5' $(FANCY_BOUNDS_ANALYSIS_FLAG),$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
+$(eval $(call add_curve_keys,poly1305_32,UNSATURATED_SOLINAS,'poly1305',32,'(auto)' '2^130 - 5' $(FANCY_BOUNDS_ANALYSIS_FLAG),$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
 $(foreach bw,64 32,$(eval $(call add_curve_keys,p521_$(bw),UNSATURATED_SOLINAS,'p521',$(bw),'(auto)' '2^521 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS)))
 ## 2^224 - 2^96 + 1 ## does not bounds check
 #$(eval $(call add_curve_keys,p224_solinas_64,UNSATURATED_SOLINAS,'p224',64,'4' '2^224 - 2^96 + 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
diff --git a/fiat-bedrock2/src/poly1305_32.c b/fiat-bedrock2/src/poly1305_32.c
index 4b8aa9d9bf..c27187f206 100644
--- a/fiat-bedrock2/src/poly1305_32.c
+++ b/fiat-bedrock2/src/poly1305_32.c
@@ -1,4 +1,4 @@
-/* Autogenerated: 'src/ExtractionOCaml/bedrock2_unsaturated_solinas' --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select --no-field-element-typedefs poly1305 32 '(auto)' '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
+/* Autogenerated: 'src/ExtractionOCaml/bedrock2_unsaturated_solinas' --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select --no-field-element-typedefs poly1305 32 '(auto)' '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
 /* curve description: poly1305 */
 /* machine_wordsize = 32 (from "32") */
 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax */
diff --git a/fiat-bedrock2/src/poly1305_64.c b/fiat-bedrock2/src/poly1305_64.c
index 92ecb99a93..0de53ca73a 100644
--- a/fiat-bedrock2/src/poly1305_64.c
+++ b/fiat-bedrock2/src/poly1305_64.c
@@ -1,4 +1,4 @@
-/* Autogenerated: 'src/ExtractionOCaml/bedrock2_unsaturated_solinas' --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select --no-field-element-typedefs poly1305 64 3 '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
+/* Autogenerated: 'src/ExtractionOCaml/bedrock2_unsaturated_solinas' --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select --no-field-element-typedefs poly1305 64 3 '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
 /* curve description: poly1305 */
 /* machine_wordsize = 64 (from "64") */
 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax */
diff --git a/fiat-c/src/poly1305_32.c b/fiat-c/src/poly1305_32.c
index 9811d84a1a..bf0020fbd5 100644
--- a/fiat-c/src/poly1305_32.c
+++ b/fiat-c/src/poly1305_32.c
@@ -1,4 +1,4 @@
-/* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier poly1305 32 '(auto)' '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
+/* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier poly1305 32 '(auto)' '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
 /* curve description: poly1305 */
 /* machine_wordsize = 32 (from "32") */
 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax */
diff --git a/fiat-c/src/poly1305_64.c b/fiat-c/src/poly1305_64.c
index ca9097170e..cc4935646f 100644
--- a/fiat-c/src/poly1305_64.c
+++ b/fiat-c/src/poly1305_64.c
@@ -1,4 +1,4 @@
-/* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier poly1305 64 3 '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
+/* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier poly1305 64 3 '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
 /* curve description: poly1305 */
 /* machine_wordsize = 64 (from "64") */
 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax */
diff --git a/fiat-go/32/poly1305/poly1305.go b/fiat-go/32/poly1305/poly1305.go
index 6232d4f6f5..0333c7d367 100644
--- a/fiat-go/32/poly1305/poly1305.go
+++ b/fiat-go/32/poly1305/poly1305.go
@@ -1,6 +1,6 @@
 // Code generated by Fiat Cryptography. DO NOT EDIT.
 //
-// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Go --relax-primitive-carry-to-bitwidth 32,64 --cmovznz-by-mul --internal-static --package-case flatcase --public-function-case UpperCamelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case camelCase --no-prefix-fiat --doc-newline-in-typedef-bounds --doc-prepend-header 'Code generated by Fiat Cryptography. DO NOT EDIT.' --doc-text-before-function-name '' --doc-text-before-type-name '' --package-name poly1305 '' 32 '(auto)' '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_add carry_sub carry_opp
+// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Go --relax-primitive-carry-to-bitwidth 32,64 --cmovznz-by-mul --internal-static --package-case flatcase --public-function-case UpperCamelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case camelCase --no-prefix-fiat --doc-newline-in-typedef-bounds --doc-prepend-header 'Code generated by Fiat Cryptography. DO NOT EDIT.' --doc-text-before-function-name '' --doc-text-before-type-name '' --package-name poly1305 '' 32 '(auto)' '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_add carry_sub carry_opp
 //
 // curve description (via package name): poly1305
 //
diff --git a/fiat-go/64/poly1305/poly1305.go b/fiat-go/64/poly1305/poly1305.go
index 21bfaa6024..8164e6b3aa 100644
--- a/fiat-go/64/poly1305/poly1305.go
+++ b/fiat-go/64/poly1305/poly1305.go
@@ -1,6 +1,6 @@
 // Code generated by Fiat Cryptography. DO NOT EDIT.
 //
-// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Go --no-wide-int --relax-primitive-carry-to-bitwidth 32,64 --cmovznz-by-mul --internal-static --package-case flatcase --public-function-case UpperCamelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case camelCase --no-prefix-fiat --doc-newline-in-typedef-bounds --doc-prepend-header 'Code generated by Fiat Cryptography. DO NOT EDIT.' --doc-text-before-function-name '' --doc-text-before-type-name '' --package-name poly1305 '' 64 3 '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_add carry_sub carry_opp
+// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Go --no-wide-int --relax-primitive-carry-to-bitwidth 32,64 --cmovznz-by-mul --internal-static --package-case flatcase --public-function-case UpperCamelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case camelCase --no-prefix-fiat --doc-newline-in-typedef-bounds --doc-prepend-header 'Code generated by Fiat Cryptography. DO NOT EDIT.' --doc-text-before-function-name '' --doc-text-before-type-name '' --package-name poly1305 '' 64 3 '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_add carry_sub carry_opp
 //
 // curve description (via package name): poly1305
 //
diff --git a/fiat-java/src/FiatPoly1305.java b/fiat-java/src/FiatPoly1305.java
index 7871e5993c..4964542a4b 100644
--- a/fiat-java/src/FiatPoly1305.java
+++ b/fiat-java/src/FiatPoly1305.java
@@ -1,4 +1,4 @@
-/* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Java --cmovznz-by-mul --widen-carry --widen-bytes --internal-static --package-name fiat_crypto --class-case UpperCamelCase --no-field-element-typedefs Poly1305 32 '(auto)' '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
+/* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Java --cmovznz-by-mul --widen-carry --widen-bytes --internal-static --package-name fiat_crypto --class-case UpperCamelCase --no-field-element-typedefs Poly1305 32 '(auto)' '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax */
 /* curve description: Poly1305 */
 /* machine_wordsize = 32 (from "32") */
 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax */
diff --git a/fiat-rust/src/poly1305_32.rs b/fiat-rust/src/poly1305_32.rs
index 7ed22837dd..bf6ccf7af9 100644
--- a/fiat-rust/src/poly1305_32.rs
+++ b/fiat-rust/src/poly1305_32.rs
@@ -1,4 +1,4 @@
-//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline poly1305 32 '(auto)' '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
+//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline poly1305 32 '(auto)' '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
 //! curve description: poly1305
 //! machine_wordsize = 32 (from "32")
 //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
diff --git a/fiat-rust/src/poly1305_64.rs b/fiat-rust/src/poly1305_64.rs
index 81fe43b567..83ef96068f 100644
--- a/fiat-rust/src/poly1305_64.rs
+++ b/fiat-rust/src/poly1305_64.rs
@@ -1,4 +1,4 @@
-//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline poly1305 64 3 '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
+//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline poly1305 64 3 '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
 //! curve description: poly1305
 //! machine_wordsize = 64 (from "64")
 //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
diff --git a/fiat-zig/src/poly1305_32.zig b/fiat-zig/src/poly1305_32.zig
index 708df9e03a..78998e33d6 100644
--- a/fiat-zig/src/poly1305_32.zig
+++ b/fiat-zig/src/poly1305_32.zig
@@ -1,4 +1,4 @@
-// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Zig --internal-static --public-function-case camelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case UpperCamelCase --no-prefix-fiat --package-name poly1305 '' 32 '(auto)' '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
+// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Zig --internal-static --public-function-case camelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case UpperCamelCase --no-prefix-fiat --package-name poly1305 '' 32 '(auto)' '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
 // curve description (via package name): poly1305
 // machine_wordsize = 32 (from "32")
 // requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
diff --git a/fiat-zig/src/poly1305_64.zig b/fiat-zig/src/poly1305_64.zig
index fd058b74b8..350937d329 100644
--- a/fiat-zig/src/poly1305_64.zig
+++ b/fiat-zig/src/poly1305_64.zig
@@ -1,4 +1,4 @@
-// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Zig --internal-static --public-function-case camelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case UpperCamelCase --no-prefix-fiat --package-name poly1305 '' 64 3 '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
+// Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Zig --internal-static --public-function-case camelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case UpperCamelCase --no-prefix-fiat --package-name poly1305 '' 64 3 '2^130 - 5' --fancy-and-powerful-but-exponentially-slow-bounds-analysis carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
 // curve description (via package name): poly1305
 // machine_wordsize = 64 (from "64")
 // requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax