5 files changed, 5 insertions, 0 deletions
diff --git a/test/data/formulas/ladd-boringssl-x25519 b/test/data/formulas/ladd-boringssl-x25519
index 416b245..a1ed9a9 100644
--- a/test/data/formulas/ladd-boringssl-x25519
+++ b/test/data/formulas/ladd-boringssl-x25519
@@ -1,4 +1,5 @@
 source BoringSSL bfa8369 https://github.com/google/boringssl/blob/bfa8369795b7533a222a72b7a1bc928941cd66bf/crypto/curve25519/curve25519.c#L624
 parameter a24
 assume a24 = (a+2)/4
+assume Z1 = 1
 coords xz
diff --git a/test/data/formulas/ladd-go-1214 b/test/data/formulas/ladd-go-1214
index 6756685..c6ca9da 100644
--- a/test/data/formulas/ladd-go-1214
+++ b/test/data/formulas/ladd-go-1214
@@ -1,4 +1,5 @@
 source go crypto/ecdh/x25519 https://github.com/golang/go/blob/go1.21.4/src/crypto/ecdh/x25519.go#L86
 parameter a24
 assume a24 = (a+2)/4
+assume Z1 = 1
 coords xz
diff --git a/test/data/formulas/ladd-hacl-x25519 b/test/data/formulas/ladd-hacl-x25519
index 1dbe8cc..ece09fc 100644
--- a/test/data/formulas/ladd-hacl-x25519
+++ b/test/data/formulas/ladd-hacl-x25519
@@ -1,4 +1,5 @@
 source HACL* https://github.com/hacl-star/hacl-star/blob/v0.3.0/specs/Spec.Curve25519.fst#L56
 parameter am24
 assume am24 = (a-2)/4
+assume Z1 = 1
 coords xz
diff --git a/test/data/formulas/ladd-openssl-x25519 b/test/data/formulas/ladd-openssl-x25519
index a40fdc7..5f94535 100644
--- a/test/data/formulas/ladd-openssl-x25519
+++ b/test/data/formulas/ladd-openssl-x25519
@@ -1,4 +1,5 @@
 source OpenSSL 3.1.4 https://github.com/openssl/openssl/blob/openssl-3.1.4/crypto/ec/curve25519.c#L211
 parameter a24
 assume a24 = (a+2)/4
+assume Z1 = 1
 coords xz
diff --git a/test/data/formulas/ladd-rfc7748 b/test/data/formulas/ladd-rfc7748
index 70c69e3..18fd36c 100644
--- a/test/data/formulas/ladd-rfc7748
+++ b/test/data/formulas/ladd-rfc7748
@@ -1,4 +1,5 @@
 source RFC 7748
 parameter am24
 assume am24 = (a-2)/4
+assume Z1 = 1
 coords xz