From d3e1f8054370ddd5327a8d0e5efdf4a5ee565995 Mon Sep 17 00:00:00 2001
From: l-kent <l.kent@uq.edu.au>
Date: Mon, 22 Jan 2024 14:02:49 +1000
Subject: [PATCH] update expected

---
 .../malloc_memcpy_strlen_memset_free.expected | 549 +++---------------
 .../malloc_memcpy_strlen_memset_free.expected | 549 +++---------------
 .../malloc_memcpy_strlen_memset_free.expected | 549 +++---------------
 .../malloc_memcpy_strlen_memset_free.expected | 549 +++---------------
 4 files changed, 268 insertions(+), 1928 deletions(-)

diff --git a/src/test/correct/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/correct/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
index 0bd0a291a..212e558c4 100644
--- a/src/test/correct/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
+++ b/src/test/correct/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
@@ -82,43 +82,17 @@ procedure {:extern} rely();
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure {:extern} rely_transitive()
+procedure {:extern} rely_transitive();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
 {
   call rely();
   call rely();
@@ -136,76 +110,20 @@ procedure #free();
   free requires (memory_load8_le(mem, 2477bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2478bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2476bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure main()
+procedure main();
   modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R19, Gamma_R2, Gamma_R20, Gamma_R21, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_malloc_base, Gamma_malloc_count, Gamma_malloc_end, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R19, R2, R20, R21, R29, R30, R31, malloc_base, malloc_count, malloc_end, mem, stack;
   requires (gamma_load8(Gamma_mem, $password_addr) == false);
   requires malloc_count == 0;
@@ -243,38 +161,10 @@ procedure main()
   free requires (memory_load8_le(mem, 2477bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2478bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (Gamma_R19 == old(Gamma_R19));
   free ensures (Gamma_R20 == old(Gamma_R20));
   free ensures (Gamma_R21 == old(Gamma_R21));
@@ -289,38 +179,12 @@ procedure main()
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+
+implementation main()
 {
   var #4: bv64;
   var #5: bv64;
@@ -420,38 +284,10 @@ procedure malloc();
   free requires (memory_load8_le(mem, 2477bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2478bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures Gamma_R0 == true;
   ensures malloc_count == old(malloc_count) + 1;
   ensures bvugt64(malloc_end[malloc_count], malloc_base[malloc_count]);
@@ -465,38 +301,10 @@ procedure malloc();
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memcpy();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -504,76 +312,20 @@ procedure memcpy();
   free requires (memory_load8_le(mem, 2477bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2478bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i, bvadd64(R0, R2))) then gamma_load8((Gamma_mem), bvadd64(bvsub64(i, R0), R1)) else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le((mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i))));
   free ensures (memory_load8_le(mem, 2476bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memset();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -582,38 +334,10 @@ procedure memset();
   free requires (memory_load8_le(mem, 2477bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2478bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then Gamma_R1 else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i))));
@@ -621,38 +345,10 @@ procedure memset();
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure puts();
   modifies Gamma_R16, Gamma_R17, R16, R17;
@@ -660,74 +356,18 @@ procedure puts();
   free requires (memory_load8_le(mem, 2477bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2478bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2476bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure strlen();
   modifies Gamma_R0, Gamma_R16, Gamma_R17, R0, R16, R17;
@@ -735,38 +375,10 @@ procedure strlen();
   free requires (memory_load8_le(mem, 2477bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2478bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures Gamma_R0 == true;
   ensures (forall i: bv64 :: (bvule64(old(R0), i)) && (bvult64(i, bvadd64(old(R0), R0))) ==> mem[i] != 0bv8);
   ensures (memory_load8_le(mem, bvadd64(old(R0), R0)) == 0bv8);
@@ -775,35 +387,8 @@ procedure strlen();
   free ensures (memory_load8_le(mem, 2477bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2478bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2479bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+
diff --git a/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
index e24a49e85..2181a0d83 100644
--- a/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
+++ b/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
@@ -82,43 +82,17 @@ procedure {:extern} rely();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure {:extern} rely_transitive()
+procedure {:extern} rely_transitive();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
 {
   call rely();
   call rely();
@@ -136,76 +110,20 @@ procedure #free();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2472bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure main()
+procedure main();
   modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R19, Gamma_R2, Gamma_R20, Gamma_R21, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_malloc_base, Gamma_malloc_count, Gamma_malloc_end, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R19, R2, R20, R21, R29, R30, R31, malloc_base, malloc_count, malloc_end, mem, stack;
   requires (gamma_load8(Gamma_mem, $password_addr) == false);
   requires malloc_count == 0;
@@ -243,38 +161,10 @@ procedure main()
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (Gamma_R19 == old(Gamma_R19));
   free ensures (Gamma_R20 == old(Gamma_R20));
   free ensures (Gamma_R21 == old(Gamma_R21));
@@ -289,38 +179,12 @@ procedure main()
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+
+implementation main()
 {
   var #1: bv64;
   var #2: bv64;
@@ -420,38 +284,10 @@ procedure malloc();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures Gamma_R0 == true;
   ensures malloc_count == old(malloc_count) + 1;
   ensures bvugt64(malloc_end[malloc_count], malloc_base[malloc_count]);
@@ -465,38 +301,10 @@ procedure malloc();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memcpy();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -504,76 +312,20 @@ procedure memcpy();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i, bvadd64(R0, R2))) then gamma_load8((Gamma_mem), bvadd64(bvsub64(i, R0), R1)) else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le((mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i))));
   free ensures (memory_load8_le(mem, 2472bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memset();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -582,38 +334,10 @@ procedure memset();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then Gamma_R1 else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i))));
@@ -621,38 +345,10 @@ procedure memset();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure puts();
   modifies Gamma_R16, Gamma_R17, R16, R17;
@@ -660,74 +356,18 @@ procedure puts();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2472bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure strlen();
   modifies Gamma_R0, Gamma_R16, Gamma_R17, R0, R16, R17;
@@ -735,38 +375,10 @@ procedure strlen();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures Gamma_R0 == true;
   ensures (forall i: bv64 :: (bvule64(old(R0), i)) && (bvult64(i, bvadd64(old(R0), R0))) ==> mem[i] != 0bv8);
   ensures (memory_load8_le(mem, bvadd64(old(R0), R0)) == 0bv8);
@@ -775,35 +387,8 @@ procedure strlen();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+
diff --git a/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
index 8296ed8eb..9a6191d97 100644
--- a/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
+++ b/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
@@ -92,43 +92,17 @@ procedure {:extern} rely();
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure {:extern} rely_transitive()
+procedure {:extern} rely_transitive();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
 {
   call rely();
   call rely();
@@ -146,76 +120,20 @@ procedure #free();
   free requires (memory_load8_le(mem, 2485bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2486bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2484bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure main()
+procedure main();
   modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R19, Gamma_R2, Gamma_R20, Gamma_R21, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_malloc_base, Gamma_malloc_count, Gamma_malloc_end, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R19, R2, R20, R21, R29, R30, R31, R8, malloc_base, malloc_count, malloc_end, mem, stack;
   requires (gamma_load8(Gamma_mem, $password_addr) == false);
   requires malloc_count == 0;
@@ -253,38 +171,10 @@ procedure main()
   free requires (memory_load8_le(mem, 2485bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2486bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (Gamma_R19 == old(Gamma_R19));
   free ensures (Gamma_R20 == old(Gamma_R20));
   free ensures (Gamma_R21 == old(Gamma_R21));
@@ -299,38 +189,12 @@ procedure main()
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+
+implementation main()
 {
   var #4: bv64;
   var #5: bv64;
@@ -436,38 +300,10 @@ procedure malloc();
   free requires (memory_load8_le(mem, 2485bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2486bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures Gamma_R0 == true;
   ensures malloc_count == old(malloc_count) + 1;
@@ -482,38 +318,10 @@ procedure malloc();
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memcpy();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -521,38 +329,10 @@ procedure memcpy();
   free requires (memory_load8_le(mem, 2485bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2486bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i, bvadd64(R0, R2))) then gamma_load8((Gamma_mem), bvadd64(bvsub64(i, R0), R1)) else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le((mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i))));
@@ -560,38 +340,10 @@ procedure memcpy();
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memset();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -600,38 +352,10 @@ procedure memset();
   free requires (memory_load8_le(mem, 2485bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2486bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then Gamma_R1 else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i))));
@@ -639,38 +363,10 @@ procedure memset();
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure puts();
   modifies Gamma_R16, Gamma_R17, R16, R17;
@@ -678,74 +374,18 @@ procedure puts();
   free requires (memory_load8_le(mem, 2485bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2486bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2484bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure strlen();
   modifies Gamma_R0, Gamma_R16, Gamma_R17, R0, R16, R17;
@@ -753,38 +393,10 @@ procedure strlen();
   free requires (memory_load8_le(mem, 2485bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2486bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free requires (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free requires (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free requires (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures (((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr)))) && (memory_load8_le(mem, $stext_addr) == old(memory_load8_le(mem, $stext_addr))));
   ensures Gamma_R0 == true;
   ensures (forall i: bv64 :: (bvule64(old(R0), i)) && (bvult64(i, bvadd64(old(R0), R0))) ==> mem[i] != 0bv8);
@@ -794,35 +406,8 @@ procedure strlen();
   free ensures (memory_load8_le(mem, 2485bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2486bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2487bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130488bv64) == 16bv8);
-  free ensures (memory_load8_le(mem, 130489bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130490bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130491bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130492bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130493bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130494bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130495bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130496bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 130497bv64) == 8bv8);
-  free ensures (memory_load8_le(mem, 130498bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130499bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130500bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130501bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130502bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130503bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 20bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130488bv64) == 2320bv64);
+  free ensures (memory_load64_le(mem, 130496bv64) == 2240bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 2324bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+
diff --git a/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
index a05348e17..b5e8b4dec 100644
--- a/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
+++ b/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
@@ -90,43 +90,17 @@ procedure {:extern} rely();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure {:extern} rely_transitive()
+procedure {:extern} rely_transitive();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
 {
   call rely();
   call rely();
@@ -144,76 +118,20 @@ procedure #free();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2472bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
-procedure main()
+procedure main();
   modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R19, Gamma_R2, Gamma_R20, Gamma_R21, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_malloc_base, Gamma_malloc_count, Gamma_malloc_end, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R19, R2, R20, R21, R29, R30, R31, malloc_base, malloc_count, malloc_end, mem, stack;
   requires (gamma_load8(Gamma_mem, $password_addr) == false);
   requires malloc_count == 0;
@@ -251,38 +169,10 @@ procedure main()
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (Gamma_R19 == old(Gamma_R19));
   free ensures (Gamma_R20 == old(Gamma_R20));
   free ensures (Gamma_R21 == old(Gamma_R21));
@@ -297,38 +187,12 @@ procedure main()
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+
+implementation main()
 {
   var #1: bv64;
   var #2: bv64;
@@ -434,38 +298,10 @@ procedure malloc();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures Gamma_R0 == true;
   ensures malloc_count == old(malloc_count) + 1;
@@ -480,38 +316,10 @@ procedure malloc();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memcpy();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -519,38 +327,10 @@ procedure memcpy();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i, bvadd64(R0, R2))) then gamma_load8((Gamma_mem), bvadd64(bvsub64(i, R0), R1)) else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le((mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i))));
@@ -558,38 +338,10 @@ procedure memcpy();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure memset();
   modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
@@ -598,38 +350,10 @@ procedure memset();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))));
   ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then Gamma_R1 else old(gamma_load8(Gamma_mem, i))));
   ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i))));
@@ -637,38 +361,10 @@ procedure memset();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure puts();
   modifies Gamma_R16, Gamma_R17, R16, R17;
@@ -676,74 +372,18 @@ procedure puts();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   free ensures (memory_load8_le(mem, 2472bv64) == 1bv8);
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
 
 procedure strlen();
   modifies Gamma_R0, Gamma_R16, Gamma_R17, R0, R16, R17;
@@ -751,38 +391,10 @@ procedure strlen();
   free requires (memory_load8_le(mem, 2473bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2474bv64) == 2bv8);
   free requires (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free requires (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free requires (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free requires (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free requires (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free requires (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free requires (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free requires (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free requires (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free requires (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free requires (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free requires (memory_load64_le(mem, 131160bv64) == 131160bv64);
   ensures (((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr)))) && (memory_load8_le(mem, $stext_addr) == old(memory_load8_le(mem, $stext_addr))));
   ensures Gamma_R0 == true;
   ensures (forall i: bv64 :: (bvule64(old(R0), i)) && (bvult64(i, bvadd64(old(R0), R0))) ==> mem[i] != 0bv8);
@@ -792,35 +404,8 @@ procedure strlen();
   free ensures (memory_load8_le(mem, 2473bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 2474bv64) == 2bv8);
   free ensures (memory_load8_le(mem, 2475bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130504bv64) == 144bv8);
-  free ensures (memory_load8_le(mem, 130505bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130506bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130507bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130508bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130509bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130510bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130511bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130512bv64) == 64bv8);
-  free ensures (memory_load8_le(mem, 130513bv64) == 9bv8);
-  free ensures (memory_load8_le(mem, 130514bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130515bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130516bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130517bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130518bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 130519bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131032bv64) == 192bv8);
-  free ensures (memory_load8_le(mem, 131033bv64) == 7bv8);
-  free ensures (memory_load8_le(mem, 131034bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131035bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131036bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131037bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131038bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131039bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131160bv64) == 88bv8);
-  free ensures (memory_load8_le(mem, 131161bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131162bv64) == 2bv8);
-  free ensures (memory_load8_le(mem, 131163bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131164bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131165bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131166bv64) == 0bv8);
-  free ensures (memory_load8_le(mem, 131167bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 130504bv64) == 2448bv64);
+  free ensures (memory_load64_le(mem, 130512bv64) == 2368bv64);
+  free ensures (memory_load64_le(mem, 131032bv64) == 1984bv64);
+  free ensures (memory_load64_le(mem, 131160bv64) == 131160bv64);
+