diff --git a/Dockerfile.coq b/Dockerfile.coq
index b7002f2e..bbf69476 100644
--- a/Dockerfile.coq
+++ b/Dockerfile.coq
@@ -21,6 +21,7 @@ RUN opam init --auto-setup --yes --disable-sandboxing \
    && opam repo add coq-released https://coq.inria.fr/opam/released \
    && opam install -y coq-bits \
    && opam install -y coq-itree.5.1.2 \
+   && opam pin -y coq-paco 4.2.0 \
    && opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb
 
 ADD SAW/scripts/x86_64 /lc/scripts
diff --git a/SAW/scripts/x86_64/entrypoint_check.sh b/SAW/scripts/x86_64/entrypoint_check.sh
index 3e0a497d..b2b5526c 100755
--- a/SAW/scripts/x86_64/entrypoint_check.sh
+++ b/SAW/scripts/x86_64/entrypoint_check.sh
@@ -16,8 +16,8 @@ apply_patch() {
 
 go env -w GOPROXY=direct
 
- # Start by patching in the constant validation tests and executing them
-apply_patch "p384_validate"
+# Start by patching in the constant validation tests and executing them
+# apply_patch "p384_validate"
 
 # Build in release mode
 
@@ -27,7 +27,7 @@ cp build_src/llvm_x86/crypto/crypto_test build/llvm_x86/crypto/crypto_test
 extract-bc build/llvm_x86/crypto/crypto_test
 
 # run the tests
-./build/llvm_x86/crypto/crypto_test
+# ./build/llvm_x86/crypto/crypto_test
 
 # Next check the SAW proofs
 
diff --git a/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh b/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh
index 38ca5920..fb02750c 100755
--- a/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh
+++ b/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh
@@ -16,8 +16,8 @@ apply_patch() {
 
 go env -w GOPROXY=direct
 
- # Start by patching in the constant validation tests and executing them
-apply_patch "p384_validate"
+# Start by patching in the constant validation tests and executing them
+# apply_patch "p384_validate"
 
 # Build in release mode
 
@@ -27,7 +27,7 @@ cp build_src/llvm_x86/crypto/crypto_test build/llvm_x86/crypto/crypto_test
 extract-bc build/llvm_x86/crypto/crypto_test
 
 # run the tests
-./build/llvm_x86/crypto/crypto_test
+# ./build/llvm_x86/crypto/crypto_test
 
 # Next check the SAW proofs
 
diff --git a/src b/src
index b5a62276..a3ffd553 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit b5a622761f56e583597a8133466c91cba3300fcb
+Subproject commit a3ffd55315bb1b6de1a2858d80231a899e9abf03