diff --git a/SAW/proof/AES/AESNI-GCM.saw b/SAW/proof/AES/AESNI-GCM.saw
index c3e9c215..42097346 100644
--- a/SAW/proof/AES/AESNI-GCM.saw
+++ b/SAW/proof/AES/AESNI-GCM.saw
@@ -61,14 +61,14 @@ add_x86_preserved_reg "rax";
 enable_what4_hash_consing;
 
 aesni_gcm_encrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aesni_gcm_encrypt"
-  [ ("byte64_len_to_mask_table", 640) // We need .Lbswap_mask. Its location is <byte64_len_to_mask_table+0x240>. 640 bytes is an offset that would be large enough to contain the right bytes after alignment.
+[ ("aesni_gcm_encrypt", 1200) // we need .Lbswap_mask, which lives in .text after aesni_gcm_encrypt (1081 bytes itself). 1200 bytes is an arbitrary size that I guessed would be large enough to contain the right bytes after alignment.
   ]
   true
   (aesni_gcm_cipher_spec {{ 1 : [32] }} aesni_gcm_cipher_gcm_len aesni_gcm_cipher_len)
   aesni_gcm_cipher_tactic;
 
 aesni_gcm_decrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aesni_gcm_decrypt"
-  [ ("byte64_len_to_mask_table", 640)
+[ ("aesni_gcm_encrypt", 1200) // we need .Lbswap_mask, which lives in .text after aesni_gcm_encrypt (1081 bytes itself). 1200 bytes is an arbitrary size that I guessed would be large enough to contain the right bytes after alignment.
   ]
   true
   (aesni_gcm_cipher_spec {{ 0 : [32] }} aesni_gcm_cipher_gcm_len aesni_gcm_cipher_len)
diff --git a/SAW/proof/AES/GHASH.saw b/SAW/proof/AES/GHASH.saw
index 5c6829a3..303f506f 100644
--- a/SAW/proof/AES/GHASH.saw
+++ b/SAW/proof/AES/GHASH.saw
@@ -48,17 +48,7 @@ let gcm_ghash_avx_spec len = do {
 
 enable_what4_hash_consing;
 gcm_init_avx_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_init_avx"
-  // How to find clues for constructing the global symbol pair?
-  // 1. Find the location of the function "gcm_init_avx" in the assembly
-  //    using "nm crypto_test | grep gcm_init_avx"
-  // 2. Find the instruction that uses the constant L0x1c2_polynomial
-  //    using "objdump -S --start-address=... --stop-address=... crypto_test"
-  // 3. If there is a comment, then the comment tells us where that constant is;
-  //    else the address should be
-  //      %rip ( which is current_instruction_addr + current_instruction_size ) + the displacement offset
-  // 4. If one wants to confirm the location, try
-  //      objdump -s -j .rodata crypto_test
-  [ ("shufb_15_7", 384) // We need .L0x1c2_polynomial. Its location is <shufb_15_7+0x160>. 384 bytes is an offset that would be large enough to contain the right bytes after alignment.
+  [ ("gcm_ghash_avx", 1800) // similar hack to the one in AESNI-GCM.saw to grab .L0x1c2_polynomial, we need a better way to handle this
   ]
   true
   gcm_init_avx_spec
@@ -70,7 +60,7 @@ gcm_init_avx_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_i
 disable_what4_hash_consing;
 
 gcm_gmult_avx_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_gmult_avx"
-  [ ("shufb_15_7", 384)
+  [ ("gcm_ghash_avx", 1800)
   ]
   true
   gcm_gmult_avx_spec
@@ -92,14 +82,14 @@ let gcm_ghash_avx_tactic = do {
 };
 
 gcm_ghash_avx_encrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_ghash_avx"
-  [ ("shufb_15_7", 384)
+  [ ("gcm_ghash_avx", 1800)
   ]
   true
   (gcm_ghash_avx_spec GHASH_length_blocks_encrypt)
   gcm_ghash_avx_tactic;
 
 gcm_ghash_avx_decrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_ghash_avx"
-  [ ("shufb_15_7", 384)
+  [ ("gcm_ghash_avx", 1800)
   ]
   true
   (gcm_ghash_avx_spec GHASH_length_blocks_decrypt)
diff --git a/src b/src
index c7d7c74c..ec94d74a 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit c7d7c74caab5a15a9490e4f2cedee8cac6acd62b
+Subproject commit ec94d74a19b5a0aa738b436a95bb06ff87fc7ba9