From e4628d3b7e3a14363924d34ae9b0616dbb829a12 Mon Sep 17 00:00:00 2001
From: l-kent <l.kent@uq.edu.au>
Date: Mon, 9 Oct 2023 10:45:11 +1000
Subject: [PATCH] missed a few expected files

---
 .../basic_function_call_caller.expected       | 428 ++++++++++++++++++
 .../basic_function_call_caller.expected       | 424 +++++++++++++++++
 .../gcc_pic/basic_lock_read.expected          | 301 ++++++++++++
 .../basic_lock_security_write.expected        | 303 +++++++++++++
 .../basic_lock_security_write.expected        | 303 +++++++++++++
 .../clang_pic/basic_sec_policy_write.expected | 298 ++++++++++++
 .../gcc_pic/basic_sec_policy_write.expected   | 298 ++++++++++++
 .../clang_pic/secret_write.expected           | 335 ++++++++++++++
 .../gcc_pic/secret_write.expected             | 341 ++++++++++++++
 9 files changed, 3031 insertions(+)
 create mode 100644 src/test/correct/basic_function_call_caller/clang_pic/basic_function_call_caller.expected
 create mode 100644 src/test/correct/basic_function_call_caller/gcc_pic/basic_function_call_caller.expected
 create mode 100644 src/test/correct/basic_lock_read/gcc_pic/basic_lock_read.expected
 create mode 100644 src/test/correct/basic_lock_security_write/clang_pic/basic_lock_security_write.expected
 create mode 100644 src/test/correct/basic_lock_security_write/gcc_pic/basic_lock_security_write.expected
 create mode 100644 src/test/correct/basic_sec_policy_write/clang_pic/basic_sec_policy_write.expected
 create mode 100644 src/test/correct/basic_sec_policy_write/gcc_pic/basic_sec_policy_write.expected
 create mode 100644 src/test/correct/secret_write/clang_pic/secret_write.expected
 create mode 100644 src/test/correct/secret_write/gcc_pic/secret_write.expected

diff --git a/src/test/correct/basic_function_call_caller/clang_pic/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/clang_pic/basic_function_call_caller.expected
new file mode 100644
index 000000000..3a4e3c9e7
--- /dev/null
+++ b/src/test/correct/basic_function_call_caller/clang_pic/basic_function_call_caller.expected
@@ -0,0 +1,428 @@
+var Gamma_R0: bool;
+var Gamma_R29: bool;
+var Gamma_R30: bool;
+var Gamma_R31: bool;
+var Gamma_R8: bool;
+var Gamma_R9: bool;
+var Gamma_mem: [bv64]bool;
+var Gamma_stack: [bv64]bool;
+var R0: bv64;
+var R29: bv64;
+var R30: bv64;
+var R31: bv64;
+var R8: bv64;
+var R9: bv64;
+var mem: [bv64]bv8;
+var stack: [bv64]bv8;
+const $x_addr: bv64;
+axiom ($x_addr == 69684bv64);
+const $y_addr: bv64;
+axiom ($y_addr == 69688bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $y_addr) then (memory_load32_le(memory, $x_addr) == 1bv32) else (if (index == $x_addr) then true else false))
+}
+
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function gamma_store64(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value][bvadd64(index, 4bv64) := value][bvadd64(index, 5bv64) := value][bvadd64(index, 6bv64) := value][bvadd64(index, 7bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function memory_store64_le(memory: [bv64]bv8, index: bv64, value: bv64) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]][bvadd64(index, 4bv64) := value[40:32]][bvadd64(index, 5bv64) := value[48:40]][bvadd64(index, 6bv64) := value[56:48]][bvadd64(index, 7bv64) := value[64:56]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr)));
+  ensures (memory_load32_le(mem, $y_addr) == old(memory_load32_le(mem, $y_addr)));
+  free ensures (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 92bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69063bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr)));
+  ensures (memory_load32_le(mem, $y_addr) == old(memory_load32_le(mem, $y_addr)));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert (memory_load32_le(mem, $x_addr) == memory_load32_le(mem, $x_addr));
+  assert (memory_load32_le(mem, $y_addr) == memory_load32_le(mem, $y_addr));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert ((memory_load32_le(mem, $x_addr) == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
+  assert (gamma_load32(Gamma_mem, $y_addr) ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R29, R30, R31, R8, R9, mem, stack;
+  requires (Gamma_R0 == false);
+  free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69667bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69668bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69669bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69670bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69671bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free requires (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free requires (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 92bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69063bv64) == 0bv8);
+  free ensures (Gamma_R29 == old(Gamma_R29));
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R29 == old(R29));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 92bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69063bv64) == 0bv8);
+{
+  var #4: bv64;
+  var #5: bv64;
+  var Gamma_#4: bool;
+  var Gamma_#5: bool;
+  var Gamma_y_old: bool;
+  var x_old: bv32;
+  lmain:
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
+    #4, Gamma_#4 := bvadd64(R31, 16bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29);
+    stack, Gamma_stack := memory_store64_le(stack, bvadd64(#4, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#4, 8bv64), Gamma_R30);
+    R29, Gamma_R29 := bvadd64(R31, 16bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R29, 18446744073709551612bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R29, 18446744073709551612bv64), Gamma_R0);
+    R30, Gamma_R30 := 1904bv64, true;
+    call zero();
+    goto l00000329;
+  l00000329:
+    R8, Gamma_R8 := 65536bv64, true;
+    R8, Gamma_R8 := memory_load64_le(mem, bvadd64(R8, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R8, 4032bv64)) || L(mem, bvadd64(R8, 4032bv64)));
+    call rely();
+    assert (L(mem, R8) ==> Gamma_R0);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_y_old := (gamma_load32(Gamma_mem, $y_addr) || L(mem, $y_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R8, R0[32:0]), gamma_store32(Gamma_mem, R8, Gamma_R0);
+    assert ((R8 == $x_addr) ==> (L(mem, $y_addr) ==> Gamma_y_old));
+    assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
+    assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
+    R8, Gamma_R8 := zero_extend32_32(memory_load32_le(mem, bvadd64(R29, 18446744073709551612bv64))), (gamma_load32(Gamma_mem, bvadd64(R29, 18446744073709551612bv64)) || L(mem, bvadd64(R29, 18446744073709551612bv64)));
+    R9, Gamma_R9 := 65536bv64, true;
+    R9, Gamma_R9 := memory_load64_le(mem, bvadd64(R9, 4048bv64)), (gamma_load64(Gamma_mem, bvadd64(R9, 4048bv64)) || L(mem, bvadd64(R9, 4048bv64)));
+    call rely();
+    assert (L(mem, R9) ==> Gamma_R8);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_y_old := (gamma_load32(Gamma_mem, $y_addr) || L(mem, $y_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
+    assert ((R9 == $x_addr) ==> (L(mem, $y_addr) ==> Gamma_y_old));
+    assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
+    assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
+    R0, Gamma_R0 := 0bv64, true;
+    #5, Gamma_#5 := bvadd64(R31, 16bv64), Gamma_R31;
+    R29, Gamma_R29 := memory_load64_le(mem, #5), (gamma_load64(Gamma_mem, #5) || L(mem, #5));
+    R30, Gamma_R30 := memory_load64_le(mem, bvadd64(#5, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(#5, 8bv64)) || L(mem, bvadd64(#5, 8bv64)));
+    R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    return;
+}
+
+procedure zero()
+  modifies Gamma_R0, R0;
+  free requires (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free requires (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free requires (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 92bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69063bv64) == 0bv8);
+  ensures ((R0[32:0] == 0bv32) && Gamma_R0);
+  free ensures (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 92bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69063bv64) == 0bv8);
+{
+  lzero:
+    R0, Gamma_R0 := 0bv64, true;
+    return;
+}
diff --git a/src/test/correct/basic_function_call_caller/gcc_pic/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/gcc_pic/basic_function_call_caller.expected
new file mode 100644
index 000000000..f88d56db3
--- /dev/null
+++ b/src/test/correct/basic_function_call_caller/gcc_pic/basic_function_call_caller.expected
@@ -0,0 +1,424 @@
+var Gamma_R0: bool;
+var Gamma_R1: bool;
+var Gamma_R29: bool;
+var Gamma_R30: bool;
+var Gamma_R31: bool;
+var Gamma_mem: [bv64]bool;
+var Gamma_stack: [bv64]bool;
+var R0: bv64;
+var R1: bv64;
+var R29: bv64;
+var R30: bv64;
+var R31: bv64;
+var mem: [bv64]bv8;
+var stack: [bv64]bv8;
+const $x_addr: bv64;
+axiom ($x_addr == 69652bv64);
+const $y_addr: bv64;
+axiom ($y_addr == 69656bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $y_addr) then (memory_load32_le(memory, $x_addr) == 1bv32) else (if (index == $x_addr) then true else false))
+}
+
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function gamma_store64(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value][bvadd64(index, 4bv64) := value][bvadd64(index, 5bv64) := value][bvadd64(index, 6bv64) := value][bvadd64(index, 7bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function memory_store64_le(memory: [bv64]bv8, index: bv64, value: bv64) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]][bvadd64(index, 4bv64) := value[40:32]][bvadd64(index, 5bv64) := value[48:40]][bvadd64(index, 6bv64) := value[56:48]][bvadd64(index, 7bv64) := value[64:56]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr)));
+  ensures (memory_load32_le(mem, $y_addr) == old(memory_load32_le(mem, $y_addr)));
+  free ensures (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69608bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 92bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr)));
+  ensures (memory_load32_le(mem, $y_addr) == old(memory_load32_le(mem, $y_addr)));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert (memory_load32_le(mem, $x_addr) == memory_load32_le(mem, $x_addr));
+  assert (memory_load32_le(mem, $y_addr) == memory_load32_le(mem, $y_addr));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert ((memory_load32_le(mem, $x_addr) == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
+  assert (gamma_load32(Gamma_mem, $y_addr) ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, mem, stack;
+  requires (Gamma_R0 == false);
+  free requires (memory_load8_le(mem, 69632bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69633bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69634bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69635bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69636bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69637bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69638bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69639bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69608bv64) == 24bv8);
+  free requires (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69616bv64) == 92bv8);
+  free requires (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 20bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69007bv64) == 0bv8);
+  free ensures (Gamma_R29 == old(Gamma_R29));
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R29 == old(R29));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69608bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 92bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+{
+  var #4: bv64;
+  var Gamma_#4: bool;
+  var Gamma_y_old: bool;
+  var x_old: bv32;
+  lmain:
+    #4, Gamma_#4 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29);
+    stack, Gamma_stack := memory_store64_le(stack, bvadd64(#4, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#4, 8bv64), Gamma_R30);
+    R31, Gamma_R31 := #4, Gamma_#4;
+    R29, Gamma_R29 := R31, Gamma_R31;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R0);
+    R30, Gamma_R30 := 1900bv64, true;
+    call zero();
+    goto l00000323;
+  l00000323:
+    R1, Gamma_R1 := zero_extend32_32(R0[32:0]), Gamma_R0;
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_y_old := (gamma_load32(Gamma_mem, $y_addr) || L(mem, $y_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $x_addr) ==> (L(mem, $y_addr) ==> Gamma_y_old));
+    assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
+    assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4072bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4072bv64)) || L(mem, bvadd64(R0, 4072bv64)));
+    R1, Gamma_R1 := zero_extend32_32(memory_load32_le(mem, bvadd64(R31, 28bv64))), (gamma_load32(Gamma_mem, bvadd64(R31, 28bv64)) || L(mem, bvadd64(R31, 28bv64)));
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_y_old := (gamma_load32(Gamma_mem, $y_addr) || L(mem, $y_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $x_addr) ==> (L(mem, $y_addr) ==> Gamma_y_old));
+    assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
+    assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
+    R0, Gamma_R0 := 0bv64, true;
+    R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
+    R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
+    R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    return;
+}
+
+procedure zero()
+  modifies Gamma_R0, R0;
+  free requires (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69608bv64) == 24bv8);
+  free requires (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69616bv64) == 92bv8);
+  free requires (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 20bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69007bv64) == 0bv8);
+  ensures ((R0[32:0] == 0bv32) && Gamma_R0);
+  free ensures (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69608bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 92bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+{
+  lzero:
+    R0, Gamma_R0 := 0bv64, true;
+    return;
+}
diff --git a/src/test/correct/basic_lock_read/gcc_pic/basic_lock_read.expected b/src/test/correct/basic_lock_read/gcc_pic/basic_lock_read.expected
new file mode 100644
index 000000000..b6ba1412c
--- /dev/null
+++ b/src/test/correct/basic_lock_read/gcc_pic/basic_lock_read.expected
@@ -0,0 +1,301 @@
+var Gamma_R0: bool;
+var Gamma_R31: bool;
+var Gamma_mem: [bv64]bool;
+var Gamma_stack: [bv64]bool;
+var R0: bv64;
+var R31: bv64;
+var mem: [bv64]bv8;
+var stack: [bv64]bv8;
+const $x_addr: bv64;
+axiom ($x_addr == 69652bv64);
+const $z_addr: bv64;
+axiom ($z_addr == 69656bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $x_addr) then true else (if (index == $z_addr) then true else false))
+}
+
+function {:bvbuiltin "bvadd"} bvadd32(bv32, bv32) returns (bv32);
+function {:bvbuiltin "bvadd"} bvadd33(bv33, bv33) returns (bv33);
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:bvbuiltin "bvcomp"} bvcomp1(bv1, bv1) returns (bv1);
+function {:bvbuiltin "bvcomp"} bvcomp32(bv32, bv32) returns (bv1);
+function {:bvbuiltin "bvcomp"} bvcomp33(bv33, bv33) returns (bv1);
+function {:bvbuiltin "bvnot"} bvnot1(bv1) returns (bv1);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:bvbuiltin "sign_extend 1"} sign_extend1_32(bv32) returns (bv33);
+function {:bvbuiltin "zero_extend 1"} zero_extend1_32(bv32) returns (bv33);
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures ((old(memory_load32_le(mem, $z_addr)) == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr))) && (memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr)))));
+  free ensures (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures ((old(memory_load32_le(mem, $z_addr)) == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr))) && (memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr)))));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert ((memory_load32_le(mem, $z_addr) == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == memory_load32_le(mem, $x_addr)) && (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr))));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R31, Gamma_mem, Gamma_stack, R0, R31, mem, stack;
+  free requires (memory_load8_le(mem, 69632bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69633bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69634bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69635bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69636bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69637bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69638bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69639bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free requires (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free requires (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69007bv64) == 0bv8);
+  ensures (R0[32:0] == 0bv32);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1964bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1965bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1966bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1967bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+{
+  var #4: bv32;
+  var CF: bv1;
+  var Gamma_#4: bool;
+  var Gamma_CF: bool;
+  var Gamma_NF: bool;
+  var Gamma_VF: bool;
+  var Gamma_ZF: bool;
+  var NF: bv1;
+  var VF: bv1;
+  var ZF: bv1;
+  var z_old: bv32;
+  lmain:
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), 0bv32), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), true);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    #4, Gamma_#4 := bvadd32(R0[32:0], 4294967295bv32), Gamma_R0;
+    VF, Gamma_VF := bvnot1(bvcomp33(sign_extend1_32(bvadd32(#4, 1bv32)), bvadd33(sign_extend1_32(R0[32:0]), 0bv33))), (Gamma_R0 && Gamma_#4);
+    CF, Gamma_CF := bvnot1(bvcomp33(zero_extend1_32(bvadd32(#4, 1bv32)), bvadd33(zero_extend1_32(R0[32:0]), 4294967296bv33))), (Gamma_R0 && Gamma_#4);
+    ZF, Gamma_ZF := bvcomp32(bvadd32(#4, 1bv32), 0bv32), Gamma_#4;
+    NF, Gamma_NF := bvadd32(#4, 1bv32)[32:31], Gamma_#4;
+    assert Gamma_ZF;
+    if ((bvnot1(bvcomp1(ZF, 1bv1)) != 0bv1)) {
+      goto l00000328;
+    }
+    goto l0000033f;
+  l0000033f:
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));
+    call rely();
+    assert (L(mem, R0) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    mem, Gamma_mem := memory_store32_le(mem, R0, 0bv32), gamma_store32(Gamma_mem, R0, true);
+    assert (memory_load32_le(mem, $z_addr) == z_old);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));
+    R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), Gamma_R0);
+    goto l00000328;
+  l00000328:
+    R0, Gamma_R0 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 12bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 12bv64));
+    R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    return;
+}
diff --git a/src/test/correct/basic_lock_security_write/clang_pic/basic_lock_security_write.expected b/src/test/correct/basic_lock_security_write/clang_pic/basic_lock_security_write.expected
new file mode 100644
index 000000000..acb290d63
--- /dev/null
+++ b/src/test/correct/basic_lock_security_write/clang_pic/basic_lock_security_write.expected
@@ -0,0 +1,303 @@
+var Gamma_R0: bool;
+var Gamma_R10: bool;
+var Gamma_R31: bool;
+var Gamma_R8: bool;
+var Gamma_R9: bool;
+var Gamma_mem: [bv64]bool;
+var Gamma_stack: [bv64]bool;
+var R0: bv64;
+var R10: bv64;
+var R31: bv64;
+var R8: bv64;
+var R9: bv64;
+var mem: [bv64]bv8;
+var stack: [bv64]bv8;
+const $x_addr: bv64;
+axiom ($x_addr == 69688bv64);
+const $z_addr: bv64;
+axiom ($z_addr == 69684bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $x_addr) then (memory_load32_le(memory, $z_addr) == 0bv32) else (if (index == $z_addr) then true else false))
+}
+
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures ((memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr))) && (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr))));
+  free ensures (memory_load8_le(mem, 1956bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1957bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1958bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1959bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69576bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69577bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69578bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69579bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69580bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69581bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69582bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69583bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69063bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures ((memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr))) && (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr))));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert ((memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr)) && (memory_load32_le(mem, $x_addr) == memory_load32_le(mem, $x_addr)));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert ((memory_load32_le(mem, $z_addr) == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == memory_load32_le(mem, $x_addr)) && (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr))));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R10, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R10, R31, R8, R9, mem, stack;
+  requires (memory_load32_le(mem, $z_addr) != 0bv32);
+  requires (Gamma_R0 == false);
+  free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69667bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69668bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69669bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69670bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69671bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1956bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1957bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1958bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1959bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69576bv64) == 56bv8);
+  free requires (memory_load8_le(mem, 69577bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69578bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69579bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69580bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69581bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69582bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69583bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free requires (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69063bv64) == 0bv8);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1956bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1957bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1958bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1959bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69576bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69577bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69578bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69579bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69580bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69581bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69582bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69583bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69063bv64) == 0bv8);
+{
+  var Gamma_x_old: bool;
+  var x_old: bv32;
+  var z_old: bv32;
+  lmain:
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), Gamma_R0);
+    R8, Gamma_R8 := 65536bv64, true;
+    R8, Gamma_R8 := memory_load64_le(mem, bvadd64(R8, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R8, 4032bv64)) || L(mem, bvadd64(R8, 4032bv64)));
+    R9, Gamma_R9 := 1bv64, true;
+    call rely();
+    assert (L(mem, R8) ==> Gamma_R9);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R8, R9[32:0]), gamma_store32(Gamma_mem, R8, Gamma_R9);
+    assert ((R8 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    R10, Gamma_R10 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 12bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 12bv64));
+    R9, Gamma_R9 := 65536bv64, true;
+    R9, Gamma_R9 := memory_load64_le(mem, bvadd64(R9, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R9, 4040bv64)) || L(mem, bvadd64(R9, 4040bv64)));
+    call rely();
+    assert (L(mem, R9) ==> Gamma_R10);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, R10[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R10);
+    assert ((R9 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    R0, Gamma_R0 := 0bv64, true;
+    call rely();
+    assert (L(mem, R9) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, 0bv32), gamma_store32(Gamma_mem, R9, true);
+    assert ((R9 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    call rely();
+    assert (L(mem, R8) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R8, 0bv32), gamma_store32(Gamma_mem, R8, true);
+    assert ((R8 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    return;
+}
diff --git a/src/test/correct/basic_lock_security_write/gcc_pic/basic_lock_security_write.expected b/src/test/correct/basic_lock_security_write/gcc_pic/basic_lock_security_write.expected
new file mode 100644
index 000000000..12667d063
--- /dev/null
+++ b/src/test/correct/basic_lock_security_write/gcc_pic/basic_lock_security_write.expected
@@ -0,0 +1,303 @@
+var Gamma_R0: bool;
+var Gamma_R1: bool;
+var Gamma_R31: bool;
+var Gamma_mem: [bv64]bool;
+var Gamma_stack: [bv64]bool;
+var R0: bv64;
+var R1: bv64;
+var R31: bv64;
+var mem: [bv64]bv8;
+var stack: [bv64]bv8;
+const $x_addr: bv64;
+axiom ($x_addr == 69652bv64);
+const $z_addr: bv64;
+axiom ($z_addr == 69656bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $x_addr) then (memory_load32_le(memory, $z_addr) == 0bv32) else (if (index == $z_addr) then true else false))
+}
+
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures ((memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr))) && (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr))));
+  free ensures (memory_load8_le(mem, 1972bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1973bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1974bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1975bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures ((memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr))) && (memory_load32_le(mem, $x_addr) == old(memory_load32_le(mem, $x_addr))));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert ((memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr)) && (memory_load32_le(mem, $x_addr) == memory_load32_le(mem, $x_addr)));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert ((memory_load32_le(mem, $z_addr) == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == memory_load32_le(mem, $x_addr)) && (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr))));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R1, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R31, mem, stack;
+  requires (memory_load32_le(mem, $z_addr) != 0bv32);
+  requires (Gamma_R0 == false);
+  free requires (memory_load8_le(mem, 69632bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69633bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69634bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69635bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69636bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69637bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69638bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69639bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1972bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1973bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1974bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1975bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free requires (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free requires (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69007bv64) == 0bv8);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1972bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1973bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1974bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1975bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+{
+  var Gamma_x_old: bool;
+  var x_old: bv32;
+  var z_old: bv32;
+  lmain:
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), Gamma_R0);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    R1, Gamma_R1 := 1bv64, true;
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));
+    R1, Gamma_R1 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 12bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 12bv64));
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));
+    call rely();
+    assert (L(mem, R0) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, 0bv32), gamma_store32(Gamma_mem, R0, true);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    call rely();
+    assert (L(mem, R0) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    x_old := memory_load32_le(mem, $x_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, 0bv32), gamma_store32(Gamma_mem, R0, true);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old == 0bv32) ==> ((memory_load32_le(mem, $x_addr) == x_old) && (memory_load32_le(mem, $z_addr) == z_old)));
+    R0, Gamma_R0 := 0bv64, true;
+    R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    return;
+}
diff --git a/src/test/correct/basic_sec_policy_write/clang_pic/basic_sec_policy_write.expected b/src/test/correct/basic_sec_policy_write/clang_pic/basic_sec_policy_write.expected
new file mode 100644
index 000000000..7e7412b7b
--- /dev/null
+++ b/src/test/correct/basic_sec_policy_write/clang_pic/basic_sec_policy_write.expected
@@ -0,0 +1,298 @@
+var Gamma_R0: bool;
+var Gamma_R10: bool;
+var Gamma_R31: bool;
+var Gamma_R8: bool;
+var Gamma_R9: bool;
+var Gamma_mem: [bv64]bool;
+var Gamma_stack: [bv64]bool;
+var R0: bv64;
+var R10: bv64;
+var R31: bv64;
+var R8: bv64;
+var R9: bv64;
+var mem: [bv64]bv8;
+var stack: [bv64]bv8;
+const $x_addr: bv64;
+axiom ($x_addr == 69688bv64);
+const $z_addr: bv64;
+axiom ($z_addr == 69684bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $z_addr) then true else (if (index == $x_addr) then (memory_load32_le(memory, $z_addr) == 0bv32) else false))
+}
+
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures (old(memory_load32_le(mem, $z_addr)) == memory_load32_le(mem, $z_addr));
+  free ensures (memory_load8_le(mem, 1960bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1961bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1962bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1963bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69576bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69577bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69578bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69579bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69580bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69581bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69582bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69583bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69063bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures (old(memory_load32_le(mem, $z_addr)) == memory_load32_le(mem, $z_addr));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert ((memory_load32_le(mem, $z_addr) != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R10, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R10, R31, R8, R9, mem, stack;
+  requires (Gamma_R0 == false);
+  free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69667bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69668bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69669bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69670bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69671bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1960bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1961bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1962bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1963bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69576bv64) == 56bv8);
+  free requires (memory_load8_le(mem, 69577bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69578bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69579bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69580bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69581bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69582bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69583bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free requires (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69063bv64) == 0bv8);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1960bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1961bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1962bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1963bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69576bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69577bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69578bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69579bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69580bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69581bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69582bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69583bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69056bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69057bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69058bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69059bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69060bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69061bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69062bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69063bv64) == 0bv8);
+{
+  var Gamma_x_old: bool;
+  var z_old: bv32;
+  lmain:
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), Gamma_R0);
+    R9, Gamma_R9 := 65536bv64, true;
+    R9, Gamma_R9 := memory_load64_le(mem, bvadd64(R9, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R9, 4032bv64)) || L(mem, bvadd64(R9, 4032bv64)));
+    R8, Gamma_R8 := 1bv64, true;
+    call rely();
+    assert (L(mem, R9) ==> Gamma_R8);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
+    assert ((R9 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R10, Gamma_R10 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 12bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 12bv64));
+    R8, Gamma_R8 := 65536bv64, true;
+    R8, Gamma_R8 := memory_load64_le(mem, bvadd64(R8, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R8, 4040bv64)) || L(mem, bvadd64(R8, 4040bv64)));
+    call rely();
+    assert (L(mem, R8) ==> Gamma_R10);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R8, R10[32:0]), gamma_store32(Gamma_mem, R8, Gamma_R10);
+    assert ((R8 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R0, Gamma_R0 := 0bv64, true;
+    call rely();
+    assert (L(mem, R8) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R8, 0bv32), gamma_store32(Gamma_mem, R8, true);
+    assert ((R8 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R8, Gamma_R8 := 2bv64, true;
+    call rely();
+    assert (L(mem, R9) ==> Gamma_R8);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
+    assert ((R9 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    return;
+}
diff --git a/src/test/correct/basic_sec_policy_write/gcc_pic/basic_sec_policy_write.expected b/src/test/correct/basic_sec_policy_write/gcc_pic/basic_sec_policy_write.expected
new file mode 100644
index 000000000..43ae9ed97
--- /dev/null
+++ b/src/test/correct/basic_sec_policy_write/gcc_pic/basic_sec_policy_write.expected
@@ -0,0 +1,298 @@
+var Gamma_R0: bool;
+var Gamma_R1: bool;
+var Gamma_R31: bool;
+var Gamma_mem: [bv64]bool;
+var Gamma_stack: [bv64]bool;
+var R0: bv64;
+var R1: bv64;
+var R31: bv64;
+var mem: [bv64]bv8;
+var stack: [bv64]bv8;
+const $x_addr: bv64;
+axiom ($x_addr == 69652bv64);
+const $z_addr: bv64;
+axiom ($z_addr == 69656bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $z_addr) then true else (if (index == $x_addr) then (memory_load32_le(memory, $z_addr) == 0bv32) else false))
+}
+
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures (old(memory_load32_le(mem, $z_addr)) == memory_load32_le(mem, $z_addr));
+  free ensures (memory_load8_le(mem, 1976bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1977bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1978bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1979bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures (old(memory_load32_le(mem, $z_addr)) == memory_load32_le(mem, $z_addr));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert ((memory_load32_le(mem, $z_addr) != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R1, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R31, mem, stack;
+  requires (Gamma_R0 == false);
+  free requires (memory_load8_le(mem, 69632bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69633bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69634bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69635bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69636bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69637bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69638bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69639bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1976bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1977bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1978bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1979bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free requires (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free requires (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69007bv64) == 0bv8);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1976bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1977bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1978bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1979bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69600bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69601bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69602bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69603bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69604bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69605bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69606bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69607bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69008bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69009bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69010bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69012bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69013bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69014bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69015bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+{
+  var Gamma_x_old: bool;
+  var z_old: bv32;
+  lmain:
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), Gamma_R0);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    R1, Gamma_R1 := 1bv64, true;
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));
+    R1, Gamma_R1 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 12bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 12bv64));
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));
+    call rely();
+    assert (L(mem, R0) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, 0bv32), gamma_store32(Gamma_mem, R0, true);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    R1, Gamma_R1 := 2bv64, true;
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert ((z_old != 0bv32) ==> (memory_load32_le(mem, $z_addr) != 0bv32));
+    R0, Gamma_R0 := 0bv64, true;
+    R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    return;
+}
diff --git a/src/test/correct/secret_write/clang_pic/secret_write.expected b/src/test/correct/secret_write/clang_pic/secret_write.expected
new file mode 100644
index 000000000..2ee0be178
--- /dev/null
+++ b/src/test/correct/secret_write/clang_pic/secret_write.expected
@@ -0,0 +1,335 @@
+var Gamma_R0: bool;
+var Gamma_R10: bool;
+var Gamma_R8: bool;
+var Gamma_R9: bool;
+var Gamma_mem: [bv64]bool;
+var R0: bv64;
+var R10: bv64;
+var R8: bv64;
+var R9: bv64;
+var mem: [bv64]bv8;
+const $secret_addr: bv64;
+axiom ($secret_addr == 69688bv64);
+const $x_addr: bv64;
+axiom ($x_addr == 69692bv64);
+const $z_addr: bv64;
+axiom ($z_addr == 69684bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $secret_addr) then false else (if (index == $x_addr) then (bvsmod32(memory_load32_le(memory, $z_addr), 2bv32) == 0bv32) else (if (index == $z_addr) then true else false)))
+}
+
+function {:bvbuiltin "bvadd"} bvadd32(bv32, bv32) returns (bv32);
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:bvbuiltin "bvsge"} bvsge32(bv32, bv32) returns (bool);
+function {:bvbuiltin "bvsmod"} bvsmod32(bv32, bv32) returns (bv32);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures (memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr)));
+  ensures (old(gamma_load32(Gamma_mem, $x_addr)) ==> gamma_load32(Gamma_mem, $x_addr));
+  free ensures (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69040bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69041bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69042bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69043bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69044bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69045bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69046bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69047bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 60bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69560bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69561bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69562bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69563bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69564bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69565bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69566bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69567bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures (memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr)));
+  ensures (old(gamma_load32(Gamma_mem, $x_addr)) ==> gamma_load32(Gamma_mem, $x_addr));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr));
+  assert (gamma_load32(Gamma_mem, $x_addr) ==> gamma_load32(Gamma_mem, $x_addr));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert bvsge32(memory_load32_le(mem, $z_addr), memory_load32_le(mem, $z_addr));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R10, Gamma_R8, Gamma_R9, Gamma_mem, R0, R10, R8, R9, mem;
+  requires (gamma_load32(Gamma_mem, $x_addr) == true);
+  requires (gamma_load32(Gamma_mem, $z_addr) == true);
+  requires (gamma_load32(Gamma_mem, $secret_addr) == false);
+  requires (memory_load32_le(mem, $z_addr) == 0bv32);
+  free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69667bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69668bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69669bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69670bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69671bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free requires (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69048bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69040bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 69041bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69042bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69043bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69044bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69045bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69046bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69047bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69568bv64) == 60bv8);
+  free requires (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69560bv64) == 52bv8);
+  free requires (memory_load8_le(mem, 69561bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69562bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69563bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69564bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69565bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69566bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69567bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1968bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1969bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1970bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1971bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
+  free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69584bv64) == 56bv8);
+  free ensures (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69048bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69049bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69050bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69051bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69052bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69053bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69054bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69055bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69040bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 69041bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69042bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69043bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69044bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69045bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69046bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69047bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69568bv64) == 60bv8);
+  free ensures (memory_load8_le(mem, 69569bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69570bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69571bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69572bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69573bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69574bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69575bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69560bv64) == 52bv8);
+  free ensures (memory_load8_le(mem, 69561bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69562bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69563bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69564bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69565bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69566bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69567bv64) == 0bv8);
+{
+  var Gamma_x_old: bool;
+  var z_old: bv32;
+  lmain:
+    R9, Gamma_R9 := 65536bv64, true;
+    R9, Gamma_R9 := memory_load64_le(mem, bvadd64(R9, 4024bv64)), (gamma_load64(Gamma_mem, bvadd64(R9, 4024bv64)) || L(mem, bvadd64(R9, 4024bv64)));
+    R0, Gamma_R0 := 0bv64, true;
+    call rely();
+    assert (L(mem, R9) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, 0bv32), gamma_store32(Gamma_mem, R9, true);
+    assert ((R9 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R8, Gamma_R8 := zero_extend32_32(memory_load32_le(mem, R9)), (gamma_load32(Gamma_mem, R9) || L(mem, R9));
+    R8, Gamma_R8 := zero_extend32_32(bvadd32(R8[32:0], 1bv32)), Gamma_R8;
+    call rely();
+    assert (L(mem, R9) ==> Gamma_R8);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
+    assert ((R9 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R8, Gamma_R8 := 65536bv64, true;
+    R8, Gamma_R8 := memory_load64_le(mem, bvadd64(R8, 4048bv64)), (gamma_load64(Gamma_mem, bvadd64(R8, 4048bv64)) || L(mem, bvadd64(R8, 4048bv64)));
+    R10, Gamma_R10 := zero_extend32_32(memory_load32_le(mem, R8)), (gamma_load32(Gamma_mem, R8) || L(mem, R8));
+    R8, Gamma_R8 := 65536bv64, true;
+    R8, Gamma_R8 := memory_load64_le(mem, bvadd64(R8, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R8, 4032bv64)) || L(mem, bvadd64(R8, 4032bv64)));
+    call rely();
+    assert (L(mem, R8) ==> Gamma_R10);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R8, R10[32:0]), gamma_store32(Gamma_mem, R8, Gamma_R10);
+    assert ((R8 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    call rely();
+    assert (L(mem, R8) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R8, 0bv32), gamma_store32(Gamma_mem, R8, true);
+    assert ((R8 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R8, Gamma_R8 := zero_extend32_32(memory_load32_le(mem, R9)), (gamma_load32(Gamma_mem, R9) || L(mem, R9));
+    R8, Gamma_R8 := zero_extend32_32(bvadd32(R8[32:0], 1bv32)), Gamma_R8;
+    call rely();
+    assert (L(mem, R9) ==> Gamma_R8);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
+    assert ((R9 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    return;
+}
diff --git a/src/test/correct/secret_write/gcc_pic/secret_write.expected b/src/test/correct/secret_write/gcc_pic/secret_write.expected
new file mode 100644
index 000000000..61ac58fb1
--- /dev/null
+++ b/src/test/correct/secret_write/gcc_pic/secret_write.expected
@@ -0,0 +1,341 @@
+var Gamma_R0: bool;
+var Gamma_R1: bool;
+var Gamma_mem: [bv64]bool;
+var R0: bv64;
+var R1: bv64;
+var mem: [bv64]bv8;
+const $secret_addr: bv64;
+axiom ($secret_addr == 69660bv64);
+const $x_addr: bv64;
+axiom ($x_addr == 69656bv64);
+const $z_addr: bv64;
+axiom ($z_addr == 69652bv64);
+function L(memory: [bv64]bv8, index: bv64) returns (bool) {
+  (if (index == $secret_addr) then false else (if (index == $x_addr) then (bvsmod32(memory_load32_le(memory, $z_addr), 2bv32) == 0bv32) else (if (index == $z_addr) then true else false)))
+}
+
+function {:bvbuiltin "bvadd"} bvadd32(bv32, bv32) returns (bv32);
+function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:bvbuiltin "bvsge"} bvsge32(bv32, bv32) returns (bool);
+function {:bvbuiltin "bvsmod"} bvsmod32(bv32, bv32) returns (bv32);
+function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))))))
+}
+
+function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure rely();
+  modifies mem, Gamma_mem;
+  ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
+  ensures (memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr)));
+  ensures (old(gamma_load32(Gamma_mem, $x_addr)) ==> gamma_load32(Gamma_mem, $x_addr));
+  free ensures (memory_load8_le(mem, 2008bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 2009bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 2010bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 2011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69608bv64) == 28bv8);
+  free ensures (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69584bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68992bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 68993bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 68994bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68995bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68996bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68997bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68998bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68999bv64) == 0bv8);
+
+procedure rely_transitive()
+  modifies mem, Gamma_mem;
+  ensures (memory_load32_le(mem, $z_addr) == old(memory_load32_le(mem, $z_addr)));
+  ensures (old(gamma_load32(Gamma_mem, $x_addr)) ==> gamma_load32(Gamma_mem, $x_addr));
+{
+  call rely();
+  call rely();
+}
+
+procedure rely_reflexive()
+{
+  assert (memory_load32_le(mem, $z_addr) == memory_load32_le(mem, $z_addr));
+  assert (gamma_load32(Gamma_mem, $x_addr) ==> gamma_load32(Gamma_mem, $x_addr));
+}
+
+procedure guarantee_reflexive()
+  modifies mem, Gamma_mem;
+{
+  assert bvsge32(memory_load32_le(mem, $z_addr), memory_load32_le(mem, $z_addr));
+}
+
+procedure main()
+  modifies Gamma_R0, Gamma_R1, Gamma_mem, R0, R1, mem;
+  requires (gamma_load32(Gamma_mem, $x_addr) == true);
+  requires (gamma_load32(Gamma_mem, $z_addr) == true);
+  requires (gamma_load32(Gamma_mem, $secret_addr) == false);
+  requires (memory_load32_le(mem, $z_addr) == 0bv32);
+  free requires (memory_load8_le(mem, 69632bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69633bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69634bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69635bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69636bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69637bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69638bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69639bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 2008bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 2009bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 2010bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 2011bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69608bv64) == 28bv8);
+  free requires (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free requires (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free requires (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69584bv64) == 20bv8);
+  free requires (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free requires (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free requires (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69000bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 69007bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 68992bv64) == 80bv8);
+  free requires (memory_load8_le(mem, 68993bv64) == 7bv8);
+  free requires (memory_load8_le(mem, 68994bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 68995bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 68996bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 68997bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 68998bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 68999bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 2008bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 2009bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 2010bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 2011bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69608bv64) == 28bv8);
+  free ensures (memory_load8_le(mem, 69609bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69610bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69611bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69612bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69613bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69614bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69615bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69640bv64) == 8bv8);
+  free ensures (memory_load8_le(mem, 69641bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69642bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69643bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69644bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69645bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69616bv64) == 84bv8);
+  free ensures (memory_load8_le(mem, 69617bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69618bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69619bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69620bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69621bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69622bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69623bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69584bv64) == 20bv8);
+  free ensures (memory_load8_le(mem, 69585bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69586bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69587bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69588bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69589bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69590bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69591bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69592bv64) == 24bv8);
+  free ensures (memory_load8_le(mem, 69593bv64) == 16bv8);
+  free ensures (memory_load8_le(mem, 69594bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69000bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69001bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 69002bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69003bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69004bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69005bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69006bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 69007bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68992bv64) == 80bv8);
+  free ensures (memory_load8_le(mem, 68993bv64) == 7bv8);
+  free ensures (memory_load8_le(mem, 68994bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68995bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68996bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68997bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68998bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 68999bv64) == 0bv8);
+{
+  var Gamma_x_old: bool;
+  var z_old: bv32;
+  lmain:
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4048bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4048bv64)) || L(mem, bvadd64(R0, 4048bv64)));
+    call rely();
+    assert (L(mem, R0) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, 0bv32), gamma_store32(Gamma_mem, R0, true);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4048bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4048bv64)) || L(mem, bvadd64(R0, 4048bv64)));
+    R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    R1, Gamma_R1 := zero_extend32_32(bvadd32(R0[32:0], 1bv32)), Gamma_R0;
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4048bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4048bv64)) || L(mem, bvadd64(R0, 4048bv64)));
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4072bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4072bv64)) || L(mem, bvadd64(R0, 4072bv64)));
+    R1, Gamma_R1 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4056bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4056bv64)) || L(mem, bvadd64(R0, 4056bv64)));
+    call rely();
+    assert (L(mem, R0) ==> true);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, 0bv32), gamma_store32(Gamma_mem, R0, true);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4048bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4048bv64)) || L(mem, bvadd64(R0, 4048bv64)));
+    R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    R1, Gamma_R1 := zero_extend32_32(bvadd32(R0[32:0], 1bv32)), Gamma_R0;
+    R0, Gamma_R0 := 65536bv64, true;
+    R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4048bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4048bv64)) || L(mem, bvadd64(R0, 4048bv64)));
+    call rely();
+    assert (L(mem, R0) ==> Gamma_R1);
+    z_old := memory_load32_le(mem, $z_addr);
+    Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
+    mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
+    assert ((R0 == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    R0, Gamma_R0 := 0bv64, true;
+    return;
+}