diff --git a/README.md b/README.md
index 29c21f825..1a62bb4d0 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Synthetic Separation Logic
 
-[![Build Status](https://travis-ci.org/TyGuS/synsl.svg?branch=master)](https://travis-ci.org/TyGuS/synsl)
+[![Build Status](https://travis-ci.org/TyGuS/suslik.svg?branch=master)](https://travis-ci.org/TyGuS/suslik)
 [![License](https://img.shields.io/badge/License-BSD%202--Clause-orange.svg)](https://raw.githubusercontent.com/TyGuS/suslik/master/LICENSE)
 
 Synthesis of Heap-Manipulating Programs from Separation Logic Specifications
diff --git a/src/test/resources/synthesis/abduct/list-copy-len-ptr.syn b/src/test/resources/synthesis/abduct/list-copy-len-ptr.syn
index 6925ba9f2..a323ed76d 100644
--- a/src/test/resources/synthesis/abduct/list-copy-len-ptr.syn
+++ b/src/test/resources/synthesis/abduct/list-copy-len-ptr.syn
@@ -17,8 +17,8 @@ void list_copy (loc r) {
     list_copy(r);
     let y12 = *r;
     let y2 = malloc(2);
-    *(y2 + 1) = nxt2;
-    *r = y2;
     *(x2 + 1) = y12;
+    *r = y2;
+    *(y2 + 1) = nxt2;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/account/alloc-struct.syn b/src/test/resources/synthesis/account/alloc-struct.syn
index 9f02c9a0a..08777936d 100644
--- a/src/test/resources/synthesis/account/alloc-struct.syn
+++ b/src/test/resources/synthesis/account/alloc-struct.syn
@@ -6,7 +6,7 @@ should be able to allocate structures
 ###
 void createAccount (loc x, int bal, int lim) {
   let y2 = malloc(2);
-  *(y2 + 1) = bal;
-  *y2 = lim;
   *x = y2;
+  *y2 = lim;
+  *(y2 + 1) = bal;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy-len/c6-alloc-head.syn b/src/test/resources/synthesis/copy-len/c6-alloc-head.syn
index 29b40996d..6f551fe62 100644
--- a/src/test/resources/synthesis/copy-len/c6-alloc-head.syn
+++ b/src/test/resources/synthesis/copy-len/c6-alloc-head.syn
@@ -13,6 +13,6 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy-len/c7-frame-alloc-head.syn b/src/test/resources/synthesis/copy-len/c7-frame-alloc-head.syn
index dcf2e2159..28acb3aeb 100644
--- a/src/test/resources/synthesis/copy-len/c7-frame-alloc-head.syn
+++ b/src/test/resources/synthesis/copy-len/c7-frame-alloc-head.syn
@@ -17,6 +17,6 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy-len/c8-alloc-close.syn b/src/test/resources/synthesis/copy-len/c8-alloc-close.syn
index dd226b9c4..2b0e8ba39 100644
--- a/src/test/resources/synthesis/copy-len/c8-alloc-close.syn
+++ b/src/test/resources/synthesis/copy-len/c8-alloc-close.syn
@@ -17,6 +17,6 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy-len/list-copy-len.syn b/src/test/resources/synthesis/copy-len/list-copy-len.syn
index e15ce4ab9..19cef28a6 100644
--- a/src/test/resources/synthesis/copy-len/list-copy-len.syn
+++ b/src/test/resources/synthesis/copy-len/list-copy-len.syn
@@ -16,7 +16,7 @@ void list_copy (loc r, loc x) {
     list_copy(r, nxt2);
     let y12 = *r;
     let y2 = malloc(2);
-    *(y2 + 1) = y12;
     *r = y2;
+    *(y2 + 1) = y12;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy/c5-alloc_value.syn b/src/test/resources/synthesis/copy/c5-alloc_value.syn
index da9af580d..214fc1042 100644
--- a/src/test/resources/synthesis/copy/c5-alloc_value.syn
+++ b/src/test/resources/synthesis/copy/c5-alloc_value.syn
@@ -13,6 +13,6 @@ void foo(loc r, int v)
 
 void foo (loc r, int v) {
   let Y2 = malloc(2);
-  *Y2 = v;
   *r = Y2;
+  *Y2 = v;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy/c6-alloc_head.syn b/src/test/resources/synthesis/copy/c6-alloc_head.syn
index 253ba0665..21613c085 100644
--- a/src/test/resources/synthesis/copy/c6-alloc_head.syn
+++ b/src/test/resources/synthesis/copy/c6-alloc_head.syn
@@ -16,7 +16,7 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let y2 = malloc(2);
-  *y2 = v;
-  *(y2 + 1) = t3;
   *r = y2;
+  *(y2 + 1) = t3;
+  *y2 = v;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy/c7-frame-alloc-head.syn b/src/test/resources/synthesis/copy/c7-frame-alloc-head.syn
index 43e985755..e16c29b0f 100644
--- a/src/test/resources/synthesis/copy/c7-frame-alloc-head.syn
+++ b/src/test/resources/synthesis/copy/c7-frame-alloc-head.syn
@@ -19,7 +19,7 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *Y2 = v;
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
+  *Y2 = v;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy/c8-alloc-close.syn b/src/test/resources/synthesis/copy/c8-alloc-close.syn
index c60b7c7e6..b822ac192 100644
--- a/src/test/resources/synthesis/copy/c8-alloc-close.syn
+++ b/src/test/resources/synthesis/copy/c8-alloc-close.syn
@@ -19,7 +19,7 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *Y2 = v;
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
+  *Y2 = v;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy/list_copy.syn b/src/test/resources/synthesis/copy/list_copy.syn
index 073c7d057..cf11f782b 100644
--- a/src/test/resources/synthesis/copy/list_copy.syn
+++ b/src/test/resources/synthesis/copy/list_copy.syn
@@ -17,8 +17,8 @@ void list_copy (loc r, loc x) {
     list_copy(r, nxt2);
     let y12 = *r;
     let y2 = malloc(2);
-    *y2 = v2;
-    *(y2 + 1) = y12;
     *r = y2;
+    *(y2 + 1) = y12;
+    *y2 = v2;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/copy/list_copy_hard.syn b/src/test/resources/synthesis/copy/list_copy_hard.syn
index 9af0a8d4a..b122223f8 100644
--- a/src/test/resources/synthesis/copy/list_copy_hard.syn
+++ b/src/test/resources/synthesis/copy/list_copy_hard.syn
@@ -18,9 +18,9 @@ void listcopy (loc r) {
     listcopy(r);
     let y12 = *r;
     let y2 = malloc(2);
-    *y2 = v2;
-    *(y2 + 1) = nxt2;
-    *r = y2;
     *(x2 + 1) = y12;
+    *r = y2;
+    *(y2 + 1) = nxt2;
+    *y2 = v2;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/dllist/dllist-to-llist.syn b/src/test/resources/synthesis/dllist/dllist-to-llist.syn
index b01bd4b9e..71dda2ea8 100644
--- a/src/test/resources/synthesis/dllist/dllist-to-llist.syn
+++ b/src/test/resources/synthesis/dllist/dllist-to-llist.syn
@@ -18,9 +18,9 @@ void dll_to_sll (loc f) {
     dll_to_sll(f);
     let i12 = *f;
     let i2 = malloc(2);
+    *f = i2;
+    *(i2 + 1) = i12;
     free(x2);
     *i2 = v2;
-    *(i2 + 1) = i12;
-    *f = i2;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/entail/duplicator.syn b/src/test/resources/synthesis/entail/duplicator.syn
index 469f10511..0a5b8f93c 100644
--- a/src/test/resources/synthesis/entail/duplicator.syn
+++ b/src/test/resources/synthesis/entail/duplicator.syn
@@ -11,8 +11,8 @@ void duplicate(loc x, loc r)
 void duplicate (loc x, loc r) {
   let a2 = *x;
   let z2 = malloc(2);
-  free(x);
-  *(z2 + 1) = a2;
-  *z2 = a2;
   *r = z2;
+  *z2 = a2;
+  *(z2 + 1) = a2;
+  free(x);
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/flatten/tree-flatten-acc.syn b/src/test/resources/synthesis/flatten/tree-flatten-acc.syn
index d8daaeca8..769b7b840 100644
--- a/src/test/resources/synthesis/flatten/tree-flatten-acc.syn
+++ b/src/test/resources/synthesis/flatten/tree-flatten-acc.syn
@@ -18,9 +18,9 @@ void tree_flatten (loc x, loc z) {
     tree_flatten(r2, z);
     let t22 = *z;
     let t3 = malloc(2);
+    *z = t3;
+    *(t3 + 1) = t22;
     free(x);
     *t3 = v2;
-    *(t3 + 1) = t22;
-    *z = t3;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/flatten/tree-flatten.syn b/src/test/resources/synthesis/flatten/tree-flatten.syn
index c2576e3c8..0e3c23120 100644
--- a/src/test/resources/synthesis/flatten/tree-flatten.syn
+++ b/src/test/resources/synthesis/flatten/tree-flatten.syn
@@ -23,9 +23,9 @@ void tree_flatten (loc z) {
     list_append(z, y22);
     let z12 = *z;
     let y3 = malloc(2);
+    *z = y3;
+    *(y3 + 1) = z12;
     free(x2);
     *y3 = v2;
-    *(y3 + 1) = z12;
-    *z = y3;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/llist/llist-nil.syn b/src/test/resources/synthesis/llist/llist-nil.syn
index d04bb2e96..3b0e48d14 100644
--- a/src/test/resources/synthesis/llist/llist-nil.syn
+++ b/src/test/resources/synthesis/llist/llist-nil.syn
@@ -9,6 +9,6 @@ should be able to allocate a linked list
 
 void create_llist (loc z, loc r) {
   let x2 = malloc(1);
-  *x2 = 0;
   *r = x2;
+  *x2 = 0;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn b/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn
index 93ed09f11..5d15740f1 100644
--- a/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn
+++ b/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn
@@ -14,23 +14,15 @@ void srtl_insert (loc x, loc r) {
   if (x == 0) {
     let y2 = malloc(2);
     *r = y2;
+    *y2 = k2 <= 7 ? k2 : 7;
     *(y2 + 1) = 0;
-    *y2 = k2;
   } else {
-    let v2 = *x;
-    if (v2 <= k2) {
-      let nxt2 = *(x + 1);
-      srtl_insert(nxt2, r);
-      let y12 = *r;
-      *(x + 1) = y12;
-      *r = x;
-    } else {
-      let nxt2 = *(x + 1);
-      srtl_insert(nxt2, x);
-      let y12 = *x;
-      *r = x;
-      *(x + 1) = y12;
-      *x = k2;
-    }
+    let lo2 = *x;
+    let nxt2 = *(x + 1);
+    srtl_insert(nxt2, r);
+    let y12 = *r;
+    *x = k2 <= lo2 ? k2 : lo2;
+    *(x + 1) = y12;
+    *r = x;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-prepend.syn b/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-prepend.syn
index 78243df44..8afea493b 100644
--- a/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-prepend.syn
+++ b/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-prepend.syn
@@ -11,6 +11,6 @@ void srtl_prepend (loc x, int k, loc r)
 void srtl_prepend (loc x, int k, loc r) {
   let y2 = malloc(2);
   *r = y2;
-  *(y2 + 1) = x;
   *y2 = k;
+  *(y2 + 1) = x;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/simple/alloc.syn b/src/test/resources/synthesis/simple/alloc.syn
index f24e9fb5d..86e506161 100644
--- a/src/test/resources/synthesis/simple/alloc.syn
+++ b/src/test/resources/synthesis/simple/alloc.syn
@@ -9,6 +9,6 @@ void create(loc x)
 
 void create (loc x) {
   let y2 = malloc(1);
-  *y2 = 42;
   *x = y2;
+  *y2 = 42;
 }
diff --git a/src/test/resources/synthesis/simple/blocks.syn b/src/test/resources/synthesis/simple/blocks.syn
index 1cf47aa54..9372c1521 100644
--- a/src/test/resources/synthesis/simple/blocks.syn
+++ b/src/test/resources/synthesis/simple/blocks.syn
@@ -10,8 +10,8 @@ void create(loc x)
 
 void create (loc x) {
   let y2 = malloc(3);
-  *(y2 + 2) = x;
-  *(y2 + 1) = 2;
-  *y2 = 1;
   *x = y2;
+  *y2 = 1;
+  *(y2 + 1) = 2;
+  *(y2 + 2) = x;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/simple/kareem.syn b/src/test/resources/synthesis/simple/kareem.syn
index f524c5b53..aa11175eb 100644
--- a/src/test/resources/synthesis/simple/kareem.syn
+++ b/src/test/resources/synthesis/simple/kareem.syn
@@ -6,8 +6,8 @@ void kareem1(loc x, loc y, loc z)
 ###
 void kareem1 (loc x, loc y, loc z) {
   let v2 = *x;
-  *v2 = x;
+  *x = y;
   *z = x;
   *y = z;
-  *x = y;
+  *v2 = x;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/simple/kareem2.syn b/src/test/resources/synthesis/simple/kareem2.syn
index 835191f66..cdb135a8a 100644
--- a/src/test/resources/synthesis/simple/kareem2.syn
+++ b/src/test/resources/synthesis/simple/kareem2.syn
@@ -12,8 +12,8 @@ void kareem3 (loc x) {
   let a2 = *x;
   let b2 = *a2;
   let c2 = *b2;
-  *c2 = b2;
+  *x = 42;
   *a2 = c2;
+  *c2 = b2;
   *b2 = a2;
-  *x = 42;
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/tree/tree-copy-len-ptr.syn b/src/test/resources/synthesis/tree/tree-copy-len-ptr.syn
index ced84017b..8cb99dcb3 100644
--- a/src/test/resources/synthesis/tree/tree-copy-len-ptr.syn
+++ b/src/test/resources/synthesis/tree/tree-copy-len-ptr.syn
@@ -21,10 +21,10 @@ void tree_copy (loc r) {
     tree_copy(x2);
     let y22 = *x2;
     let y3 = malloc(3);
-    *(y3 + 2) = r12;
-    *(y3 + 1) = l2;
-    *r = y3;
-    *(x2 + 2) = y22;
     *(x2 + 1) = y12;
+    *(x2 + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = l2;
+    *(y3 + 2) = r12;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/tree/tree-copy-len.syn b/src/test/resources/synthesis/tree/tree-copy-len.syn
index 5d12f41d0..255c40c0b 100644
--- a/src/test/resources/synthesis/tree/tree-copy-len.syn
+++ b/src/test/resources/synthesis/tree/tree-copy-len.syn
@@ -19,9 +19,9 @@ void tree_copy (loc x, loc r) {
     tree_copy(r12, x);
     let y22 = *x;
     let y3 = malloc(3);
-    *(y3 + 2) = r12;
-    *(y3 + 1) = y12;
-    *r = y3;
     *(x + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = y12;
+    *(y3 + 2) = r12;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/tree/tree-copy-ptr.syn b/src/test/resources/synthesis/tree/tree-copy-ptr.syn
index 7c7bb265d..0e1589ed3 100644
--- a/src/test/resources/synthesis/tree/tree-copy-ptr.syn
+++ b/src/test/resources/synthesis/tree/tree-copy-ptr.syn
@@ -22,12 +22,12 @@ void tree_copy (loc r) {
     tree_copy(x2);
     let y22 = *x2;
     let y3 = malloc(3);
-    *x2 = v2;
-    *y3 = v2;
-    *(y3 + 2) = r12;
-    *(y3 + 1) = l2;
-    *r = y3;
-    *(x2 + 2) = y22;
     *(x2 + 1) = y12;
+    *(x2 + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = l2;
+    *(y3 + 2) = r12;
+    *y3 = v2;
+    *x2 = v2;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/tree/tree-copy.syn b/src/test/resources/synthesis/tree/tree-copy.syn
index 9597399d3..d9fbe3eb0 100644
--- a/src/test/resources/synthesis/tree/tree-copy.syn
+++ b/src/test/resources/synthesis/tree/tree-copy.syn
@@ -20,11 +20,11 @@ void tree_copy (loc x, loc r) {
     tree_copy(r12, x);
     let y22 = *x;
     let y3 = malloc(3);
-    *y3 = v2;
-    *x = v2;
-    *(y3 + 2) = r12;
-    *(y3 + 1) = y12;
-    *r = y3;
     *(x + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = y12;
+    *(y3 + 2) = r12;
+    *x = v2;
+    *y3 = v2;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/tree/tree-morph.syn b/src/test/resources/synthesis/tree/tree-morph.syn
index f1de2d746..f72c2056f 100644
--- a/src/test/resources/synthesis/tree/tree-morph.syn
+++ b/src/test/resources/synthesis/tree/tree-morph.syn
@@ -14,8 +14,8 @@ void morhp_tree (loc x, int i) {
     let r2 = *(x + 2);
     morhp_tree(l2, i);
     morhp_tree(r2, i);
+    *x = i;
     *(x + 1) = r2;
     *(x + 2) = l2;
-    *x = i;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/tree/tree-size-ptr.syn b/src/test/resources/synthesis/tree/tree-size-ptr.syn
index d0982af41..8df397080 100644
--- a/src/test/resources/synthesis/tree/tree-size-ptr.syn
+++ b/src/test/resources/synthesis/tree/tree-size-ptr.syn
@@ -21,8 +21,8 @@ void tree_size (loc r) {
     *x2 = r12;
     tree_size(x2);
     let n22 = *x2;
-    *r = 1 + n12 + n22;
     *(x2 + 1) = r12;
     *(x2 + 2) = l2;
+    *r = 1 + n12 + n22;
   }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/tree/tree-size.syn b/src/test/resources/synthesis/tree/tree-size.syn
index 3e8b31318..9899c037d 100644
--- a/src/test/resources/synthesis/tree/tree-size.syn
+++ b/src/test/resources/synthesis/tree/tree-size.syn
@@ -19,8 +19,8 @@ void tree_size (loc x, loc r) {
     *x = 0;
     tree_size(r12, x);
     let n22 = *x;
-    *r = 1 + n12 + n22;
     *(x + 1) = r12;
     *(x + 2) = l2;
+    *r = 1 + n12 + n22;
   }
 }
\ No newline at end of file