diff --git a/.vscode/settings.json b/.vscode/settings.json
index 7630411..45ecc55 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,6 +1,8 @@
 {
     "files.associations": {
+        "*.smtlib2": "smt-lib",
         "*.vcy": "c",
-        "random": "c"
+        "random": "c",
+        "fetchandadd": "c"
     }
 }
\ No newline at end of file
diff --git a/README.md b/README.md
index a59e167..cc329e1 100644
--- a/README.md
+++ b/README.md
@@ -26,7 +26,7 @@ opam switch create 4.12.0mc 4.12.0+domains+effects --repositories=multicore=git+
 opam switch 4.12.0mc
 eval $(opam env)
 
-opam install sexplib ppxlib.0.22.0+effect-syntax ppx_deriving_yaml
+opam install sexplib ppxlib.0.22.0+effect-syntax ppx_deriving_yaml ounit2 menhir
 eval $(opam env)
 ```
 
diff --git a/benchmarks/inferred/auction1.vcy b/benchmarks/inferred/auction1.vcy
new file mode 100644
index 0000000..212dd42
--- /dev/null
+++ b/benchmarks/inferred/auction1.vcy
@@ -0,0 +1,97 @@
+
+int main(int argc, string[] argv) {
+
+    int[] bids = new int[100];
+
+    int msg_sender = int_of_string(argv[1]);
+    int highestBindingBid = int_of_string(argv[2]);
+    int highestBidder = int_of_string(argv[3]);
+    int msg_value = int_of_string(argv[4]);
+    int minimumBidValue = int_of_string(argv[5]);
+    int bidIncrement = int_of_string(argv[6]);
+
+    int bidIncrementWei_arg = int_of_string(argv[7]);
+    int minimumBidValue_arg = int_of_string(argv[8]);
+    int startBlock = int_of_string(argv[9]);
+    int endBlock = int_of_string(argv[10]);
+    string ipfsHash = int_of_string(argv[11]);
+    int block_number = int_of_string(argv[12]);
+    int blocksGenerated = int_of_string(argv[13]);
+
+    int auctionState = 0;
+    int state_started = 1;
+    int state_running = 2;
+    int state_ended = 3;
+    int state_canceled = 4;
+
+    int currentBid = 0;
+    int a = 0;
+    int b = 0;
+    int c = 0;
+
+	commute _ {
+        {
+            /* placeBid */
+            assume(auctionState == state_running);
+            assume(msg_value >= minimumBidValue);
+            currentBid = bids[msg_sender] + msg_value;
+            assume(currentBid >= highestBindingBid);
+            bids[msg_sender] = currentBid;
+            b = bids[highestBidder];
+            if(currentBid <= b){
+                a = currentBid + bidIncrement;
+                if(a <= b){
+                    highestBindingBid = a;
+                }
+                else{
+                    highestBindingBid = b;
+                }
+                return 0;
+            }
+            
+            if(currentBid > b){ 
+                c = bids[highestBidder];
+                c = c + bidIncrement;
+                if(currentBid <= c){
+                    highestBindingBid = currentBid;
+                }
+                else{
+                    highestBindingBid = c;
+                }
+                highestBidder = msg_sender;
+            }
+        }
+        {
+            /* placeBid */
+            assume(auctionState == state_running);
+            assume(msg_value >= minimumBidValue);
+            currentBid = bids[msg_sender] + msg_value;
+            assume(currentBid >= highestBindingBid);
+            bids[msg_sender] = currentBid;
+            b = bids[highestBidder];
+            if(currentBid <= b){
+                a = currentBid + bidIncrement;
+                if(a <= b){
+                    highestBindingBid = a;
+                }
+                else{
+                    highestBindingBid = b;
+                }
+                return 0;
+            }
+            
+            if(currentBid > b){ 
+                c = bids[highestBidder];
+                c = c + bidIncrement;
+                if(currentBid <= c){
+                    highestBindingBid = currentBid;
+                }
+                else{
+                    highestBindingBid = c;
+                }
+                highestBidder = msg_sender;
+            }
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/auction2.vcy b/benchmarks/inferred/auction2.vcy
new file mode 100644
index 0000000..96d2864
--- /dev/null
+++ b/benchmarks/inferred/auction2.vcy
@@ -0,0 +1,79 @@
+int min(int a, int b){
+        if(a<=b){
+            return a;
+        }else {
+            return b;
+        }
+    }
+
+int main(int argc, string[] argv) {
+
+    int[] bids = new int[100];
+
+    int msg_sender = int_of_string(argv[1]);
+    int highestBindingBid = int_of_string(argv[2]);
+    int highestBidder = int_of_string(argv[3]);
+    int msg_value = int_of_string(argv[4]);
+    int minimumBidValue = int_of_string(argv[5]);
+    int bidIncrement = int_of_string(argv[6]);
+
+    int bidIncrementWei_arg = int_of_string(argv[7]);
+    int minimumBidValue_arg = int_of_string(argv[8]);
+    int startBlock = int_of_string(argv[9]);
+    int endBlock = int_of_string(argv[10]);
+    string ipfsHash = int_of_string(argv[11]);
+    int block_number = int_of_string(argv[12]);
+    int blocksGenerated = int_of_string(argv[13]);
+
+    int auctionState = 0;
+    int state_started = 1;
+    int state_running = 2;
+    int state_ended = 3;
+    int state_canceled = 4;
+
+    int currentBid = 0;
+    int a = 0;
+    int b = 0;
+    int c = 0;
+
+
+	commute _ {
+        {
+            /* cancelAuction */
+            auctionState = state_canceled;
+            
+        }
+        {
+             /* placeBid */
+            assume(auctionState == state_running);
+            assume(msg_value >= minimumBidValue);
+            currentBid = bids[msg_sender] + msg_value;
+            assume(currentBid >= highestBindingBid);
+            bids[msg_sender] = currentBid;
+            b = bids[highestBidder];
+            if(currentBid <= b){
+                a = currentBid + bidIncrement;
+                if(a <= b){
+                    highestBindingBid = a;
+                }
+                else{
+                    highestBindingBid = b;
+                }
+                return 0;
+            }
+            
+            if(currentBid > b) {
+                c = bids[highestBidder];
+                c = c + bidIncrement;
+                if(currentBid <= c){
+                    highestBindingBid = currentBid;
+                }
+                else{
+                    highestBindingBid = c;
+                }
+                highestBidder = msg_sender;
+            }
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/auction3.vcy b/benchmarks/inferred/auction3.vcy
new file mode 100644
index 0000000..d060f78
--- /dev/null
+++ b/benchmarks/inferred/auction3.vcy
@@ -0,0 +1,63 @@
+
+int main(int argc, string[] argv) {
+
+    int[] bids = new int[100];
+
+    int msg_sender = int_of_string(argv[1]);
+    int highestBindingBid = int_of_string(argv[2]);
+    int highestBidder = int_of_string(argv[3]);
+    int msg_value = int_of_string(argv[4]);
+    int minimumBidValue = int_of_string(argv[5]);
+    int bidIncrement = int_of_string(argv[6]);
+
+    int bidIncrementWei_arg = int_of_string(argv[7]);
+    int minimumBidValue_arg = int_of_string(argv[8]);
+    int startBlock = int_of_string(argv[9]);
+    int endBlock = int_of_string(argv[10]);
+    string ipfsHash = int_of_string(argv[11]);
+    int block_number = int_of_string(argv[12]);
+    int blocksGenerated = int_of_string(argv[13]);
+
+    int auctionState = 0;
+    int state_started = 1;
+    int state_running = 2;
+    int state_ended = 3;
+    int state_canceled = 4;
+
+    int currentBid = 0;
+    int a = 0;
+    int b = 0;
+
+
+	commute _ {
+        {
+            /* startNewBid */
+            assume (auctionState == state_started);
+            startBlock = block_number;
+            endBlock = startBlock + blocksGenerated;
+            auctionState = state_running;
+            ipfsHash = "";
+            bidIncrement = bidIncrementWei_arg;
+            minimumBidValue = minimumBidValue_arg;
+        }
+        {
+            /* placeBid */
+            assume(auctionState == state_running);
+            assume(msg_value >= minimumBidValue);
+            currentBid = bids[msg_sender] + msg_value;
+            assume(currentBid >= highestBindingBid);
+            bids[msg_sender] = currentBid;
+            b = bids[highestBidder];
+            if(currentBid <= b){
+                a = currentBid + bidIncrement;
+                if(a <= b){
+                    highestBindingBid = a;
+                }
+                else{
+                    highestBindingBid = b;
+                }
+            }
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/auction4.vcy b/benchmarks/inferred/auction4.vcy
new file mode 100644
index 0000000..44ce89b
--- /dev/null
+++ b/benchmarks/inferred/auction4.vcy
@@ -0,0 +1,78 @@
+
+int main(int argc, string[] argv) {
+
+    int[] bids = new int[100];
+
+    int msg_sender = int_of_string(argv[1]);
+    int highestBindingBid = int_of_string(argv[2]);
+    int highestBidder = int_of_string(argv[3]);
+    int msg_value = int_of_string(argv[4]);
+    int minimumBidValue = int_of_string(argv[5]);
+    int bidIncrement = int_of_string(argv[6]);
+
+    int bidIncrementWei_arg = int_of_string(argv[7]);
+    int minimumBidValue_arg = int_of_string(argv[8]);
+    int startBlock = int_of_string(argv[9]);
+    int endBlock = int_of_string(argv[10]);
+    string ipfsHash = int_of_string(argv[11]);
+    int block_number = int_of_string(argv[12]);
+    int blocksGenerated = int_of_string(argv[13]);
+
+    int auctionState = 0;
+    int state_started = 1;
+    int state_running = 2;
+    int state_ended = 3;
+    int state_canceled = 4;
+
+    int currentBid = 0;
+    int a = 0;
+    int b = 0;
+    int c = 0;
+
+
+	commute _ {
+        {
+            /* startNewBid */
+            assume (auctionState == state_started);
+            startBlock = block_number;
+            endBlock = startBlock + blocksGenerated;
+            auctionState = state_running;
+            ipfsHash = "";
+            bidIncrement = bidIncrementWei_arg;
+            minimumBidValue = minimumBidValue_arg;
+        }
+        {
+            /* placeBid */
+            assume(auctionState == state_running);
+            assume(msg_value >= minimumBidValue);
+            currentBid = bids[msg_sender] + msg_value;
+            assume(currentBid >= highestBindingBid);
+            bids[msg_sender] = currentBid;
+            b = bids[highestBidder];
+            if(currentBid <= b){
+                a = currentBid + bidIncrement;
+                if(a <= b){
+                    highestBindingBid = a;
+                }
+                else{
+                    highestBindingBid = b;
+                }
+                return 0;
+            }
+            
+            if(currentBid > b){ 
+                c = bids[highestBidder];
+                c = c + bidIncrement;
+                if(currentBid <= c){
+                    highestBindingBid = currentBid;
+                }
+                else{
+                    highestBindingBid = c;
+                }
+                highestBidder = msg_sender;
+            }
+            
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/pullPayment.vcy b/benchmarks/inferred/pullPayment.vcy
new file mode 100644
index 0000000..047b63f
--- /dev/null
+++ b/benchmarks/inferred/pullPayment.vcy
@@ -0,0 +1,37 @@
+
+int main(int argc, string[] argv) {
+
+    int[] payments = new int[10];
+
+    int msg_sender = int_of_string(argv[1]);
+    int dest = int_of_string(argv[2]);
+    int amount = int_of_string(argv[3]);
+    int balance = int_of_string(argv[4]);
+    int flag = 1;
+    int payee = 0;
+    int payment = 0;
+
+	commute _ {
+        {
+            /* asyncSend */
+            payments[dest] = payments[dest] + amount;
+        }
+        {
+            /* withdrawPayments */ 
+            payee = msg_sender;
+            payment = payments[payee];
+
+            if (payment == 0){
+                flag = 0;
+                return 0;
+            }
+            if (balance < payment){
+                flag = 0;
+                return 0;
+            }
+            payments[payee] = 0;
+            /* if(!payee.send(payment)) throw */
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/standardToken1.vcy b/benchmarks/inferred/standardToken1.vcy
new file mode 100644
index 0000000..8db3583
--- /dev/null
+++ b/benchmarks/inferred/standardToken1.vcy
@@ -0,0 +1,25 @@
+
+int main(int argc, string[] argv) {
+
+    int[] allowed = new int[100];
+    int allowed_size = 10;
+
+    int value = int_of_string(argv[3]);
+    int spender = int_of_string(argv[4]);
+    int i = 0;
+    int msg_sender = int_of_string(argv[5]);
+
+	commute _ {
+        {
+            /* approve */ 
+            i = allowed_size * msg_sender + spender;
+            allowed[i] = value;
+        }
+        {
+            /* approve */ 
+            i = allowed_size * msg_sender + spender;
+            allowed[i] = value;
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/standardToken2.vcy b/benchmarks/inferred/standardToken2.vcy
new file mode 100644
index 0000000..6189e4b
--- /dev/null
+++ b/benchmarks/inferred/standardToken2.vcy
@@ -0,0 +1,34 @@
+
+int main(int argc, string[] argv) {
+
+    int[] balances = new int[10];
+    int[] allowed = new int[100];
+    int allowed_size = 10;
+
+    int from = int_of_string(argv[1]);
+    int to = int_of_string(argv[2]);
+    int value = int_of_string(argv[3]);
+    int spender = int_of_string(argv[4]);
+    int i = 0;
+    int msg_sender = int_of_string(argv[5]);
+
+	commute _ {
+        {
+            /* transferFrom */
+            i = allowed_size * from + msg_sender;
+            assume (to != 0);
+            assume (value <= balances[from]);
+            assume (value <= allowed[i]);
+            balances[from] = balances[from] - value;
+            balances[to] = balances[to] + (value);
+            i = allowed_size * from + msg_sender;
+            allowed[i] = allowed[i] - (value);
+        }
+        {
+            /* approve */ 
+            i = allowed_size * msg_sender + spender;
+            allowed[i] = value;
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/standardToken3.vcy b/benchmarks/inferred/standardToken3.vcy
new file mode 100644
index 0000000..8fd0c7f
--- /dev/null
+++ b/benchmarks/inferred/standardToken3.vcy
@@ -0,0 +1,26 @@
+
+int main(int argc, string[] argv) {
+
+    int[] allowed = new int[100];
+    int allowed_size = 10;
+
+    int owner = int_of_string(argv[1]);
+    int spender = int_of_string(argv[2]);
+    int msg_sender = int_of_string(argv[3]);
+    int value = int_of_string(argv[4]);
+    int i = 0;
+
+	commute _ {
+        {
+            /* allowance */ 
+            i = allowed_size * owner + spender;
+            return allowed[i];
+        }
+        {
+            /* approve */ 
+            i = allowed_size * msg_sender + spender;
+            allowed[i] = value;
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/standardToken4.vcy b/benchmarks/inferred/standardToken4.vcy
new file mode 100644
index 0000000..bfe2a2c
--- /dev/null
+++ b/benchmarks/inferred/standardToken4.vcy
@@ -0,0 +1,35 @@
+
+int main(int argc, string[] argv) {
+
+    int[] balances = new int[10];
+    int[] allowed = new int[100];
+    int allowed_size = 10;
+
+    int addedValue = int_of_string(argv[1]);
+    int subtractedValue = int_of_string(argv[2]);
+    int value = int_of_string(argv[3]);
+    int spender = int_of_string(argv[4]);
+    int i = 0;
+    int msg_sender = int_of_string(argv[5]);
+    int oldValue = 0;
+
+	commute _ {
+        {
+            /* increaseApproval */
+            i = allowed_size * msg_sender + spender;
+            allowed[i] = allowed[i] + addedValue;
+        }
+        {
+            /* decreaseApproval */ 
+            i = allowed_size * msg_sender + spender;
+            oldValue = allowed[i];
+            if(subtractedValue > oldValue){
+                allowed[i] = 0;
+            }
+            else{
+                allowed[i] = oldValue - subtractedValue;
+            }
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/inferred/standardToken5.vcy b/benchmarks/inferred/standardToken5.vcy
new file mode 100644
index 0000000..bcf968a
--- /dev/null
+++ b/benchmarks/inferred/standardToken5.vcy
@@ -0,0 +1,43 @@
+
+int main(int argc, string[] argv) {
+
+    int[] balances = new int[10];
+    int[] allowed = new int[100];
+    int allowed_size = 10;
+
+    int from = int_of_string(argv[1]);
+    int to = int_of_string(argv[2]);
+    int value = int_of_string(argv[3]);
+    int spender = int_of_string(argv[4]);
+    int i = 0;
+    int msg_sender = int_of_string(argv[5]);
+    int addedValue = int_of_string(argv[6]);
+    int subtractedValue = int_of_string(argv[7]);
+    int oldValue = 0;
+
+	commute _ {
+        {
+            /* transferFrom */
+            i = allowed_size * from + msg_sender;
+            assume (to != 0);
+            assume (value <= balances[from]);
+            assume (value <= allowed[i]);
+            balances[from] = balances[from] - value;
+            balances[to] = balances[to] + (value);
+            i = allowed_size * from + msg_sender;
+            allowed[i] = allowed[i] - (value);
+        }
+        {
+            /* decreaseApproval */ 
+            i = allowed_size * msg_sender + spender;
+            oldValue = allowed[i];
+            if(subtractedValue > oldValue){
+                allowed[i] = 0;
+            }
+            else{
+                allowed[i] = oldValue - subtractedValue;
+            }
+        }
+    }
+	return 0;
+}
diff --git a/benchmarks/pre_post/hoare-triple.vcy b/benchmarks/pre_post/hoare-triple.vcy
new file mode 100644
index 0000000..ae5d842
--- /dev/null
+++ b/benchmarks/pre_post/hoare-triple.vcy
@@ -0,0 +1,19 @@
+int main(int argc, string[] argv) {
+    int x = int_of_string(argv[1]);
+    int n = int_of_string(argv[2]);
+    int[] arr = new int[n];
+    int j = 0;
+
+    commute (true) {
+        pre: (j >= 0 && arr[j] > 1 && j < n && x >= n)
+        { 
+            
+        }
+        {      
+            arr[j] = arr[j] + 1;
+        }
+        post: (j >= 0 && arr[j] > 1 && j < n && x >= n)
+    }
+
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/pre_post/inductive-loop-array.vcy b/benchmarks/pre_post/inductive-loop-array.vcy
new file mode 100644
index 0000000..695139d
--- /dev/null
+++ b/benchmarks/pre_post/inductive-loop-array.vcy
@@ -0,0 +1,20 @@
+int main(int argc, string[] argv) {
+    int x = int_of_string(argv[1]);
+    int n = int_of_string(argv[2]);
+    int[] arr = new int[n];
+    int j = 0;
+
+    commute _ {
+        { 
+            arr[x] = arr[x] / 2;
+        }
+        {
+            /* for (int j = 0; j < n; j = j + 1;) {
+                 arr[j] = arr[j] + 1;
+            }*/
+            arr[j] = arr[j] + 1;
+        }
+    }
+
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/pre_post/inductive-loop.vcy b/benchmarks/pre_post/inductive-loop.vcy
new file mode 100644
index 0000000..3c9019e
--- /dev/null
+++ b/benchmarks/pre_post/inductive-loop.vcy
@@ -0,0 +1,79 @@
+int main(int argc, string[] argv) {
+    int x = int_of_string(argv[1]);
+    int[] files = new int[10];
+    int c = int_of_string(argv[2]);
+    int n = int_of_string(argv[3]);
+  
+
+    commute (x < n) { /* true */
+        pre: (c > 0)
+        { 
+            /* while(x<n) { c = c + 1; x = x + 1; } */
+
+            assume(x < n);
+
+            c = c + 1;
+            x = x + 1;
+            
+        } 
+        { 
+            if (c > 0){
+                c = c - 1;
+            }
+        }
+        post: (c > 0)
+    }
+
+    commute _ { /* !(1 > c) && !(0 == c) && !(c == 1) || c == 1 */
+        pre: (!(0 == c + 1))
+        { 
+            /* while(x<n) { c = c + 1; x = x + 1; } */
+
+            assume(x < n);
+
+            c = c + 1;
+            x = x + 1;
+            
+        } 
+        { 
+            if (c > 0){
+                c = c - 1;
+            }
+        }
+        post: (!(0 == c) && !(0 == c + 1))
+    }
+
+    commute (!(0 == c + 1)) {
+        pre: (!(0 == c))
+        { 
+            /* while(x<n) { c = c + 1; x = x + 1; } */
+
+            assume(x < n);
+
+            c = c + 1;
+            x = x + 1;
+            
+        } 
+        { 
+            if (c > 0){
+                c = c - 1;
+            }
+        }
+        post: (!(0 == c))
+    }
+
+    commute (true) { 
+        {
+            assume(x >= n);
+            }
+        {
+            if (c > 0){
+                c = c - 1;
+            }
+        }
+    }
+    
+    return 0;
+}
+
+
diff --git a/benchmarks/pre_post/inductive-loop2.vcy b/benchmarks/pre_post/inductive-loop2.vcy
new file mode 100644
index 0000000..0eacb08
--- /dev/null
+++ b/benchmarks/pre_post/inductive-loop2.vcy
@@ -0,0 +1,61 @@
+int main(int argc, string[] argv) {
+    int x = int_of_string(argv[1]);
+    int[] files = new int[10];
+    int c = int_of_string(argv[2]);
+    int n = int_of_string(argv[3]);
+
+    commute (x < n) {
+        pre: (c > 0)
+        { /* while(x<n) { c = c + 1; x = x + 1; } */
+            assume(x < n);
+
+            int old_x = x;
+            c = c + 1;
+            x = x + 1;
+
+            assert(x == old_x + 1);
+            assert(c > 0);
+        }
+        {
+            if (c > 0) {
+                c = c - 1;
+            }
+        }
+        post: (c > 0)
+    }
+
+    commute (!(0 == c + 1)) {
+        pre: (!(0 == c))
+        {
+            assume(x < n);
+
+            int old_x = x;
+            c = c + 1;
+            x = x + 1;
+
+            assert(x == old_x + 1);
+            assert(c >= 0);
+        }
+        {
+            if (c > 0) {
+                c = c - 1;
+            }
+        }
+        post: (!(0 == c))
+    }
+
+    commute (x >= n) {
+        pre: (true)
+        {
+            assume(x >= n);
+
+            assert(x >= n);
+        }
+        {
+            if (c > 0) {
+                c = c - 1;
+            }
+        }
+        post: (true)
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/pre_post/simple.vcy b/benchmarks/pre_post/simple.vcy
new file mode 100644
index 0000000..b625972
--- /dev/null
+++ b/benchmarks/pre_post/simple.vcy
@@ -0,0 +1,19 @@
+int main(int argc, string[] argv) {
+    int c = int_of_string(argv[1]);
+    
+  
+    commute _ { /* (c > 0) */
+        pre: (true)
+        { 
+            c = c * -1;
+        } 
+        { 
+            
+        }
+        post: (c < 0)
+    }
+    
+    return 0;
+}
+
+
diff --git a/reports/inference_gen.py b/reports/inference_gen.py
new file mode 100644
index 0000000..2b6045e
--- /dev/null
+++ b/reports/inference_gen.py
@@ -0,0 +1,227 @@
+#!/usr/bin/env python3
+
+import subprocess
+import sys, os, glob
+import csv
+from pathlib import Path
+from typing import Tuple, List
+from enum import Enum
+
+Benchmark = str
+Data = Tuple[str, float]
+Result = Tuple[Benchmark, Data]
+
+os.chdir(os.path.dirname(sys.argv[0]))
+verbose = '--verbose' in sys.argv
+
+vcy_exe = '../veracity/src/vcy.exe'
+infer_dir = 'benchmarks/inferred/'
+infer_loop_dir = 'benchmarks/inferred_loops/'
+output_dir = 'benchmarks/inference_output/'
+
+class VcyError(Exception):
+    def __init__(self, msg) -> None:
+        super().__init__(msg)
+        self.msg = msg
+
+def filesInDir(d):
+    return [d + f for f in os.listdir("../veracity/" + d) if os.path.isfile(os.path.join("../veracity/" + d, f))]
+
+# Program name, followed by any command line arguments
+benchmarks : List[Benchmark] = \
+    filesInDir('benchmarks/test/')
+    #filesInDir(infer_dir) + filesInDir(infer_loop_dir)
+
+manual_results : List[Result] = [
+    ("matrix", ("y0 = 0", 1.88)),
+    ("nonlinear", ("w * x = 0 && z = 0", 25.59))
+]
+
+class Heuristic(Enum):
+    # SIMPLE = 0
+    POKE = 11
+    POKE2 = 21
+    # POKE2_LATTICE = 22
+    MC_MAX = 31
+    # MC_MAX_EARLY_TERM = 33
+    # MC_MAX_LATTICE = 32
+    # MC_MAX_POKE2 = 34
+    # MC_BISECT = 41
+    # MC_BISECT_LATTICE = 42
+    
+    def __str__(self):
+        return string_of_heuristic[self]
+
+string_of_heuristic = {
+    # Heuristic.SIMPLE: "simple",
+    Heuristic.POKE: "poke",
+    Heuristic.POKE2: "poke2",
+    # Heuristic.POKE2_LATTICE: "\\poketwo{}-lattice",
+    Heuristic.MC_MAX: "mcmax",
+    # Heuristic.MC_MAX_EARLY_TERM: "\\mcmax-earlyterm{}",
+    # Heuristic.MC_MAX_LATTICE: "\\mcmax{}-lattice",
+    # Heuristic.MC_MAX_POKE2: "mcmaxpoke2",
+    # Heuristic.MC_BISECT: "mc-bisect",
+    # Heuristic.MC_BISECT_LATTICE: "mc-bisect-lattice"
+}
+
+command_of_heuristic = {
+    # Heuristic.SIMPLE: [],
+    Heuristic.POKE: "--poke",
+    Heuristic.POKE2: "--poke2",
+    # Heuristic.POKE2_LATTICE: ["--poke2", "--lattice"],
+    Heuristic.MC_MAX: "--mcpeak-max",
+    # Heuristic.MC_MAX_EARLY_TERM: ["--mcpeak-max", "--mc-term", "0.75"],
+    # Heuristic.MC_MAX_LATTICE: ["--mcpeak-max", "--lattice"],
+    # Heuristic.MC_MAX_POKE2: "--mcpeak-max-poke2",
+    # Heuristic.MC_BISECT: ["--mcpeak-bisect"],
+    # Heuristic.MC_BISECT_LATTICE: ["--mcpeak-bisect", "--lattice"]
+}
+
+prover = ['cvc4', 'cvc5', 'z3']
+
+def goodness(n_atoms, answer_incomplete):
+    cmplx = int(n_atoms) >= 10
+    if(answer_incomplete == "false"):
+        if cmplx: return "complex complete"
+        else: return "simple complete"
+    else:
+        if cmplx: return "complex incomplete"
+        else: return "simple incomplete"
+
+def run_benchmark(index : int, b : Benchmark, h, p) -> Result:
+    prog = b
+    if os.path.exists("test.lattice"):
+        os.remove("test.lattice")
+    if os.path.exists("test.equivc"):
+        os.remove("test.equivc")
+    command_infer = [vcy_exe, 'infer', '-q', '../veracity/' + prog, '--time', '-o', '../veracity/' + output_dir + os.path.basename(prog), '--timeout', '120', '--prover', p, command_of_heuristic[h]] # Time out in 2 minutes.
+
+    def f(command : List[str]):
+        popen = subprocess.Popen(
+            command, universal_newlines=True,
+            stdout=subprocess.PIPE, stderr=subprocess.PIPE
+        )
+        out, err = popen.communicate()
+        if 'error' in err or 'exception' in err:
+            raise VcyError(err.split('\n')[1])
+        return out, err
+
+    sys.stdout.write(f'{(index+1):#2d}/{len(benchmarks)} {prog} Finding inference... ')
+    sys.stdout.flush()
+    infer, output = f(command_infer)
+    print(output)
+    output = list(filter(None, output.split('\n')))
+    time = output[len(output)-1]
+    time_synth = float(output[len(output)-2])
+    time_lattice_construct = float(output[len(output)-3])
+    n_atoms = '-'.join(line.split(', ')[0] for line in output[0:len(output)-1])
+    answer_incomplete = '-'.join(line.split(', ')[1] for line in output[0:len(output)-1])
+
+    if verbose:
+        sys.stdout.write(infer)
+
+    sys.stdout.write(f'Done.\n')
+    sys.stdout.flush()
+    return b, (infer, float(time), float(time_synth), float(time_lattice_construct), n_atoms, answer_incomplete)
+
+# https://texblog.net/latex-archive/uncategorized/symbols/
+def latex_escape(s : str):
+    s = s.replace('#', '\\#')
+    s = s.replace('$', '\\$')
+    s = s.replace('%', '\\%')
+    s = s.replace('_', '\\_')
+    s = s.replace('&', '\\&')
+    s = s.replace('{', '\\{')
+    s = s.replace('}', '\\}')
+    s = s.replace('^', '\\^{}')
+    s = s.replace('||', '\\textbar\\textbar\\ ')
+    s = s.replace('>', '\\textgreater\\ ')
+    s = s.replace('<', '\\textless\\ ')
+    return s
+
+def latex_of_result(r : Result) -> str:
+    prog,data = r
+    if data == [] :
+        infer = ''
+        n_atoms = -1
+        good = 'error'
+        time = -1
+        time_synth = -1
+        time_lattice_construct = -1
+        return \
+        f'{Path(prog).stem},' + \
+        f'{time},' + \
+        f'{time_synth},' + \
+        f'{time_lattice_construct},' + \
+        f'{n_atoms},' + \
+        f'{good} '
+    else:
+        (infer,time,time_synth,time_lattice_construct,n_atoms,ans_incomplete) = data
+        infer = infer.replace('\\', '')
+        infer = ' '.join(s for s in infer.splitlines() if s)
+        infer = latex_escape(infer)
+        n_atoms = ' '.join(s for s in n_atoms.split('-') if s)
+        ans_incomplete = ' '.join(s for s in ans_incomplete.split('-') if s)
+        good = []
+        for n in n_atoms.split(' '):
+            i = 0
+            good.append(goodness(n, ans_incomplete.split(' ')[i]))
+            i = i + 1
+        good = ' '.join(good)
+    prog = latex_escape(prog)
+
+    return \
+        f'{Path(prog).stem},' + \
+        f'{time:#.2f},' + \
+        f'{time_synth:#.2f},' + \
+        f'{time_lattice_construct:#.2f},' + \
+        f'{n_atoms},' + \
+        f'{good} '
+
+    # f'\\texttt{{{infer}}} & ' + \
+
+# latex_table_start = \
+# r'''{\renewcommand{\arraystretch}{1.1}
+# \begin{tabularx}{\columnwidth}{|l|c|X|c|c}
+#     \hline
+#     adt and test case,time,natoms,quality
+#     \hline
+# '''
+
+latex_table_start = \
+r'''adt and test case,time,natoms,quality
+'''
+
+# Program & Time (s) & Inference & n_atoms & Quality \\
+
+# latex_table_end = \
+# r'''
+#     \hline
+# \end{tabularx}}'''
+
+latex_table_end = \
+r''' '''
+
+def build_table(rs : List[Result]) -> str:
+    rows = "\n".join(map(latex_of_result, rs))
+    return latex_table_start + rows + latex_table_end
+
+def build_files():
+    for h in string_of_heuristic:
+        for p in prover:
+            rs = []
+            for i, b in enumerate(benchmarks):
+                try:
+                    rs.append(run_benchmark(i, b, h, p))
+                except VcyError as err:
+                    rs.append([b, []])
+                    sys.stdout.write(f'\nFailure: {err.msg}\n')
+            # rs.extend(manual_results)
+            latex = build_table(list(rs))
+            name = 'out-veracity-'+string_of_heuristic[h]+'-NoLatt-'+p+'-NoTermGen.csv'
+            with open(name, 'w') as file:
+                file.write(latex)
+
+if __name__ == '__main__':
+    build_files()
diff --git a/src/analysis/analyze.ml b/src/analysis/analyze.ml
index f25d7ce..1983a22 100644
--- a/src/analysis/analyze.ml
+++ b/src/analysis/analyze.ml
@@ -39,7 +39,7 @@ let rec smt_translation (input: Smt.exp) (embedding: embedding_map) : exp =
     else if String.sub s (len - 5) 5 = "_size"
     then Call(MethodL("ht_size", List.assoc "ht_size" Vcylib.lib_hashtable), [no_loc @@ Id(String.sub s 0 (len - 5))])
     else if String.sub s (len - 5) 5 = "_keys"
-    then raise @@ NotImplemented "_keys translation back from smt"
+    then Id(String.sub s 0 (len - 5))
     else Id s
   | EArg i -> failwith "Not Implemented"
   | EConst c -> 
@@ -92,24 +92,38 @@ let rec smt_translation (input: Smt.exp) (embedding: embedding_map) : exp =
         end
       | _ -> raise @@ NotImplemented "Can't currently handle complicated things; requires recursive expression typechecking"
       end
+    | "insert", [e1; e2] | "set.insert", [e1; e2] -> 
+      let elem = exp_node e1 in 
+        begin match e2 with
+        | EVar (Var id) ->
+          let id, t = assoc_servois_ty id embedding in
+          begin match t with
+          | THashTable _ ->
+            CallRaw ("ht_put", [no_loc @@ Id id; elem])
+          | _ -> raise @@ Failure "Bad variable type for 'insert'"
+          end
+        | _ -> raise @@ NotImplemented "Can't currently handle complicated things; requires recursive expression typechecking"
+        end
     | _ -> failwith @@ "Function "^s^" not recognized or supported or improper arguments applied"
     end
   | EExists(binding, exp) -> raise @@ Failure "Cannot translate existential quantifier back from smt"
 
-let exp_of_phi (phi : Servois2.Phi.t) (embedding: embedding_map) : exp =
+let exp_of_phi (phi : Servois2.Phi.disjunction) (embedding: embedding_map) : exp =
   smt_translation (Servois2.Phi.smt_of_disj phi) embedding
   
-let phi_of_blocks (genv: global_env) (_: commute_variant) (blks: block node list) (vars : ty bindlist) =
+let phi_of_blocks (genv: global_env) (_: commute_variant) (blks: block node list) (vars : ty bindlist) pre post =
   let embedding = generate_embedding_map vars in
-  let [@warning "-8"] spec , [m1;m2] = Spec_generator.compile_blocks_to_spec genv blks embedding
+  let [@warning "-8"] spec , [m1;m2] = Spec_generator.compile_blocks_to_spec genv blks embedding pre post
   in
   Servois2.Choose.choose := Servois2.Choose.poke2;
   let phi, _ = Servois2.Synth.synth ~options:!Util.servois2_synth_option spec m1 m2 in
-  exp_of_phi phi embedding
+    (* Printf.eprintf "%f, %f, %f, %d, %b\n" (!Servois2.Synth.last_benchmarks.time) (!Servois2.Synth.last_benchmarks.synth_time) (!Servois2.Synth.last_benchmarks.lattice_construct_time) (!Servois2.Synth.last_benchmarks.n_atoms) (!Servois2.Synth.last_benchmarks.answer_incomplete); *)
+    exp_of_phi phi embedding
+  (* Servois2.Choose.choose := Servois2.Choose.poke2; *)
 
-let verify_of_block e genv _ blks vars : bool option * bool option =
+let verify_of_block e genv _ blks vars pre post : bool option * bool option =
   let embedding = generate_embedding_map vars in
-  let [@warning "-8"] spec , [m1;m2] = Spec_generator.compile_blocks_to_spec genv blks embedding in
+  let [@warning "-8"] spec , [m1;m2] = Spec_generator.compile_blocks_to_spec genv blks embedding pre post in
   let cond = (fst @@ Spec_generator.exp_to_smt_exp e 1 Spec_generator.variable_ctr_list) in
   Servois2.Verify.verify spec m1 m2 cond,
   Servois2.Verify.verify ~options:{Servois2.Verify.default_verify_options with ncom = true} spec m1 m2 (EUop(Not, cond))
diff --git a/src/analysis/spec_generator.ml b/src/analysis/spec_generator.ml
index 4c5e654..bf73a2b 100644
--- a/src/analysis/spec_generator.ml
+++ b/src/analysis/spec_generator.ml
@@ -15,6 +15,8 @@ let gstates = ref []
 let terms_list = ref []
 let variable_ctr_list = (Hashtbl.create 50)
 
+let pre = ref (EConst (CBool true))
+
 let sexp_of_sexp_list = function
   | [e] -> e
   | es -> ELop(And, es)
@@ -36,7 +38,6 @@ let generate_spec_statesEqual (em_vars : (ty binding * ety) list) : sexp =
    in
    sexp_of_sexp_list exp_list
 
-
 let generate_spec_state (embedding_vars: (ty binding * ety) list) : sty Smt.bindlist = 
     List.concat_map (fun ((id,ty),ety) -> let list_of_sty = compile_ety_to_sty id ety in
                         List.map (fun (id, sty) -> (Smt.Var id, sty)) list_of_sty
@@ -163,24 +164,26 @@ let set_counter (s: string) (vctrs : (string, int ref) Hashtbl.t) =
     (* if (is_global s) then *)
       Hashtbl.add vctrs s (ref 0)
 
-let set_variable_id (var: string) (side: int) (vctrs : (string, int ref) Hashtbl.t) : string =
-  if not (Hashtbl.mem vctrs var) && (side == 0) then
-    set_counter var vctrs;
-
-  if (Hashtbl.mem vctrs var) then begin
-    let current_id = Hashtbl.find vctrs var in
-    let update_id = if side == 0 
-                    then begin
-                      incr_uid (current_id) 
-                    end
-                    else begin
-                        !current_id 
-                    end in
-    let new_id = if update_id == 0 then var else var ^ "_" ^ (Int.to_string update_id) in
-    new_id
+let set_variable_id (var: string) (side: int) (vctrs : (string, int ref) Hashtbl.t) (indexed : bool) : string =
+  if indexed = false then var else begin
+    if not (Hashtbl.mem vctrs var) && (side == 0) then
+      set_counter var vctrs;
+
+    if (Hashtbl.mem vctrs var) then begin
+      let current_id = Hashtbl.find vctrs var in
+      let update_id = if side == 0 
+                      then begin
+                        incr_uid (current_id) 
+                      end
+                      else begin
+                          !current_id 
+                      end in
+      let new_id = if update_id == 0 then var else var ^ "_" ^ (Int.to_string update_id) in
+      new_id
+    end
+    else
+      var
   end
-  else
-    var
 
 let get_postconditions () : sexp =
   let exp_list = ref [] in
@@ -214,19 +217,19 @@ let make_temp_value_of_htbl (htbl : (string, int ref) Hashtbl.t) : (string * int
   Hashtbl.iter (fun id -> fun index -> temp := !temp @ [(id, !index)] ) htbl;
   ! temp
  
-let rec exp_to_smt_exp (e: exp node) (side: int) (vctrs : (string, int ref) Hashtbl.t) : sexp * sexp Smt.bindlist = 
+let rec exp_to_smt_exp (e: exp node) (side: int) ?(indexed = true) (vctrs : (string, int ref) Hashtbl.t) : sexp * sexp Smt.bindlist = 
     match e.elt with
     | CBool b -> Smt.EConst (CBool b), []
     | CInt i -> Smt.EConst (CInt (Int64.to_int i)), []
     | CStr str -> Smt.EConst (CString str), []
-    | Id id -> EVar (Var (set_variable_id id side vctrs)), []
+    | Id id -> EVar (Var (set_variable_id id side vctrs indexed)), []
     | Index (e1,e2) when side == 1 -> 
-        let rtn1, binds1 = exp_to_smt_exp e1 side vctrs in
-        let rtn2, binds2 = exp_to_smt_exp e2 side vctrs in
+        let rtn1, binds1 = exp_to_smt_exp e1 side ~indexed vctrs in
+        let rtn2, binds2 = exp_to_smt_exp e2 side ~indexed vctrs in
         EFunc ("select", [rtn1; rtn2]), binds1 @ binds2
     | Bop (op, e1, e2) ->
-        let rtn1, binds1 = exp_to_smt_exp e1 side vctrs in
-        let rtn2, binds2 = exp_to_smt_exp e2 side vctrs in
+        let rtn1, binds1 = exp_to_smt_exp e1 side ~indexed vctrs in
+        let rtn2, binds2 = exp_to_smt_exp e2 side ~indexed vctrs in
 
         begin match op with
         | Sub | Mul | Mod | Div | Eq | Lt | Gt | Lte | Gte -> 
@@ -238,12 +241,12 @@ let rec exp_to_smt_exp (e: exp node) (side: int) (vctrs : (string, int ref) Hash
         | _ -> failwith @@ sp "undefined op: %s" @@ AstML.string_of_binop op
         end
     | Uop (op, e) -> 
-        let rtn, binds = exp_to_smt_exp e side vctrs in
+        let rtn, binds = exp_to_smt_exp e side ~indexed vctrs in
 
         EUop (uop_to_servoisUop op, rtn), binds
 
     | Call (MethodL (id, {pc=Some pc;_}), el) -> 
-      let args_rtn, args_binds = List.split @@ List.map (fun exp -> exp_to_smt_exp exp right vctrs) el in
+      let args_rtn, args_binds = List.split @@ List.map (fun exp -> exp_to_smt_exp exp right ~indexed vctrs) el in
 
       let id_value = match (List.hd args_rtn) with | Smt.EVar (Var v) -> v | _ -> failwith "non string var" in     
       let dst_id = remove_index (id_value) in
@@ -260,7 +263,7 @@ let rec exp_to_smt_exp (e: exp node) (side: int) (vctrs : (string, int ref) Hash
 
        rtn, List.concat args_binds @ binds
     | Ternary(i, t, e) ->
-        let f x = exp_to_smt_exp x side vctrs in
+        let f x = exp_to_smt_exp x side ~indexed vctrs in
         let i', i_binds = f i in
         let t', t_binds = f t in
         let e', e_binds = f e in
@@ -348,7 +351,7 @@ let compile_block_to_smt_exp (genv: global_env) (b : block) =
 
           bind binds @@ compile_block_to_smt tl vctrs
 
-        | Commute (_, _, blks) -> 
+        | Commute (_, _, blks, _, _) -> 
           (* List.map (fun {elt=bl; _} -> compile_block_to_smt bl ) blks *)
           let comm_blk = List.map (fun {elt=bl; _} -> bl ) blks in
           compile_block_to_smt (List.concat comm_blk) vctrs; 
@@ -364,6 +367,11 @@ let compile_block_to_smt_exp (genv: global_env) (b : block) =
 
           EExists([(Var havoc_id, TInt (* TODO: make type dynamic *))], ELet([new_id, exp_smt], compile_block_to_smt tl vctrs))
 
+        | Require(e) ->
+          let exp_smt,_ = exp_to_smt_exp e right ~indexed:false vctrs in
+          pre := exp_smt;
+          compile_block_to_smt tl vctrs;
+
         | _ -> compile_block_to_smt tl vctrs
         end
   in
@@ -387,6 +395,15 @@ let compile_block_to_smt_exp (genv: global_env) (b : block) =
   else
   ELet (!ety_init_list, res), local_variable_ctr_list
 
+let generate_spec_pre_post_condition pre post =
+  let vctrs = variable_ctr_list in
+  match pre, post with 
+  | Some pre, Some post -> (fst @@ exp_to_smt_exp pre right vctrs),(fst @@ exp_to_smt_exp post right vctrs)
+  | None, None -> (Smt.EConst (CBool true)),(Smt.EConst (CBool true))
+  | None, Some post -> (Smt.EConst (CBool true)),(fst @@ exp_to_smt_exp post right vctrs)
+  | Some pre, None -> (fst @@ exp_to_smt_exp pre right vctrs),(Smt.EConst (CBool true))
+  
+
 let generate_method_spec_postcondition (genv: global_env) (b : block) : sexp =
     let block_to_exp, local_variable_ctr_list = (compile_block_to_smt_exp genv b) in
 
@@ -409,7 +426,9 @@ let compile_method_to_methodSpec (genv: global_env) (m:mdecl) : method_spec =
     let ret = [(Smt.Var "result", updated_return_type)] in 
     let post = generate_method_spec_postcondition genv m.body.elt in
     let terms = compile_block_to_term_list m.body.elt in 
-    let method_spec = { name = m.mname; args = args; ret = ret; pre = EConst (CBool true);
+    let method_spec = { name = m.mname; args = args; ret = ret; 
+                        pre = !pre;
+                        (* pre = EConst (CBool true); *)
                         post = post; terms = terms} in
 
     terms_list := [];
@@ -422,7 +441,8 @@ let compile_method_to_methodSpec (genv: global_env) (m:mdecl) : method_spec =
 
     method_spec
 
-let compile_blocks_to_spec (genv: global_env) (blks: block node list) (embedding_vars : (ty binding * ety) list) =
+let compile_blocks_to_spec (genv: global_env) (blks: block node list) (embedding_vars : (ty binding * ety) list) pre post =
+  let embedding_vars = List.filter (fun ((id, _),_) -> not (String.equal id "argv") ) embedding_vars in
   gstates := embedding_vars;
 
   let predicates = generate_spec_predicates embedding_vars in
@@ -432,12 +452,14 @@ let compile_blocks_to_spec (genv: global_env) (blks: block node list) (embedding
   let mdecls = List.map create_dummy_method blks in
   let methods = List.map (compile_method_to_methodSpec genv) mdecls in
   
+  let pre, post = generate_spec_pre_post_condition pre post in
+
   let preamble = None in 
 
   let spec = { name = "test"; preamble = preamble; preds = predicates; state_eq = state_equal;
-              precond = Smt.EConst (CBool true); state = state; methods= methods} in
+              precond = pre; postcond = post; state = state; methods= methods; smt_fns = []} in
   let mnames = List.map (fun ({mname = name; _}) -> name) mdecls 
   in
 
-  (* Printf.printf "%s\n" (Spec.Spec_ToMLString.spec spec); *)
-  spec, mnames
+  (* Printf.printf "%s\n" (Servois2.Spec.Spec_ToMLString.spec spec); *)
+  spec, mnames
\ No newline at end of file
diff --git a/src/servois2 b/src/servois2
index 53ef3ec..048bd25 160000
--- a/src/servois2
+++ b/src/servois2
@@ -1 +1 @@
-Subproject commit 53ef3ecd8bc5534e7e6d5961bdce79b2d3f7a25b
+Subproject commit 048bd2578427b1ddeadbfe98929b23efef2fb7e0
diff --git a/src/vcy/ast.ml b/src/vcy/ast.ml
index 4f874ed..683bdbb 100644
--- a/src/vcy/ast.ml
+++ b/src/vcy/ast.ml
@@ -134,10 +134,15 @@ and stmt =
 | For of vdecl list * exp node option * stmt node option * block node
 | While of exp node * block node
 | Raise of exp node
-| Commute of commute_variant * commute_condition * block node list
+| Commute of commute_variant * commute_condition * block node list * commute_pre_cond option * commute_post_cond option
 | Assert of exp node
 | Assume of exp node
 | Havoc of id
+| Require of exp node
+
+and commute_pre_cond = exp node 
+
+and commute_post_cond = exp node
 
 and tyval = ty * (value ref)
 
diff --git a/src/vcy/ast_print.ml b/src/vcy/ast_print.ml
index 49e8b6c..01541b9 100644
--- a/src/vcy/ast_print.ml
+++ b/src/vcy/ast_print.ml
@@ -251,7 +251,7 @@ module AstPP = struct
         end; pp_close_box fmt ();
         pps ") "; print_block_aux fmt body
 
-      | Commute(variant, phi, bodies) ->
+      | Commute(variant, phi, bodies, pre, post) ->
           pps "commute_";
           begin match variant with
             | CommuteVarSeq -> pps "seq"
@@ -502,7 +502,9 @@ module AstML = struct
                           (string_of_option string_of_exp e)
                           (string_of_option string_of_stmt s) (string_of_block b)
     | While (e,b) -> sp "While (%s, %s)" (string_of_exp e) (string_of_block b)
-    | Commute (var,phi,bl) -> 
+    | Commute (var,phi,bl,pre,post) -> 
+      begin match pre, post with 
+      | None, None -> 
       sp "Commute (%s, %s, %s)"
         begin match var with
         | CommuteVarSeq -> "CommuteVarSeq"
@@ -513,6 +515,45 @@ module AstML = struct
         | PhiExp e -> sp "PhiExp (%s)" (string_of_exp e)
         end
         (string_of_list string_of_block bl)
+      | Some pr, None ->
+      sp "Commute (%s, %s, %s, %s)"
+        begin match var with
+        | CommuteVarSeq -> "CommuteVarSeq"
+        | CommuteVarPar -> "CommuteVarPar"
+        end
+        begin match phi with 
+        | PhiInf   -> "PhiInf" 
+        | PhiExp e -> sp "PhiExp (%s)" (string_of_exp e)
+        end
+        (string_of_exp pr)
+        (string_of_list string_of_block bl)
+      | None, Some po ->
+      sp "Commute (%s, %s, %s, %s)"
+        begin match var with
+        | CommuteVarSeq -> "CommuteVarSeq"
+        | CommuteVarPar -> "CommuteVarPar"
+        end
+        begin match phi with 
+        | PhiInf   -> "PhiInf" 
+        | PhiExp e -> sp "PhiExp (%s)" (string_of_exp e)
+        end
+        (string_of_list string_of_block bl)
+        (string_of_exp po)
+      | Some pr, Some po ->
+      sp "Commute (%s, %s, %s, %s, %s)"
+        begin match var with
+        | CommuteVarSeq -> "CommuteVarSeq"
+        | CommuteVarPar -> "CommuteVarPar"
+        end
+        begin match phi with 
+        | PhiInf   -> "PhiInf" 
+        | PhiExp e -> sp "PhiExp (%s)" (string_of_exp e)
+        end
+        (string_of_exp pr)
+        (string_of_list string_of_block bl)
+        (string_of_exp po)
+      end
+      
     | Raise e ->
       sp "Raise (%s)" (string_of_exp e)
     | Assert e ->
diff --git a/src/vcy/ast_to_c.ml b/src/vcy/ast_to_c.ml
index 6f941c2..1876824 100644
--- a/src/vcy/ast_to_c.ml
+++ b/src/vcy/ast_to_c.ml
@@ -58,7 +58,7 @@ and c_of_stmt = function
     | For(inits, guard, update, body) -> sp "for(%s; %s; %s) %s" (String.concat ", " @@ List.map (fun (id, (ty, rhs)) -> sp "%s %s = %s" (c_of_ty ty) (!mangle id) (c_of_expnode rhs)) inits) (guard |> Option.map c_of_expnode |> Option.value ~default:"") (update |> Option.map c_of_stmtnode |> Option.value ~default:"") (c_of_blocknode body)
     | While(guard, body) -> sp "while(%s) %s" (c_of_expnode guard) (c_of_blocknode body)
     | Raise(e) -> raise @@ NotImplemented "c_of_stmt Raise"
-    | Commute(var, phi, bodies) -> !handle_comm phi bodies
+    | Commute(var, phi, bodies, _, _) -> !handle_comm phi bodies
     | Havoc(id) -> sp "/* %s = __VERIFIER_nondet_int() */" (!mangle id)
     | Assume(e) -> sp "/* assume%s */" (c_of_expnode e)
 and c_of_stmtnode x = c_of_stmt x.elt
diff --git a/src/vcy/interp.ml b/src/vcy/interp.ml
index ad6b8d2..30b6a87 100644
--- a/src/vcy/interp.ml
+++ b/src/vcy/interp.ml
@@ -588,7 +588,7 @@ and interp_stmt (env : env) (stmt : stmt node) : env * value option =
     pop_block_from_callstack env, v
   | While (cnd, body) ->
     interp_stmt_while env stmt.loc cnd body
-  | Commute (variant, phi, blocks) ->
+  | Commute (variant, phi, blocks, _, _) ->
     let cnd =
       match phi with
       | PhiExp p -> interp_phi env p
@@ -624,6 +624,26 @@ and interp_stmt (env : env) (stmt : stmt node) : env * value option =
     end
   | Assume _ | Havoc _ ->
     env, None (* We simply ignore 'assume's and 'havoc's at runtime *)
+  (* | GCommute (variant, phi, pre, blocks, post) ->
+    let cnd =
+      match phi with
+      | PhiExp p -> interp_phi env p
+      | PhiInf ->
+        debug_print @@ lazy (Printf.sprintf 
+          "Inferred commute condition at %s is missing; defaulting to 'false'.\n"
+          (Range.string_of_range stmt.loc));
+        false
+    in let commute = cnd && not !force_sequential in
+    begin match variant with
+    | CommuteVarPar ->
+      if commute
+      then interp_commute_async env blocks, None
+      else interp_commute_blocks env blocks, None
+    | CommuteVarSeq ->
+      if commute
+      then interp_commute_blocks env (shuffle blocks), None
+      else interp_commute_blocks env blocks, None
+    end *)
   
 
 and interp_block (env : env) (block : block node) : env * value option =
@@ -654,8 +674,8 @@ and interp_block (env : env) (block : block node) : env * value option =
 (*** COMMUTATIVITY INFERENCE ***)
 
 (* Globals are relative to the blocks *)
-let infer_phi (g : global_env) (var : commute_variant) (bl : block node list) (globals : ty bindlist) : exp node =
-  let e = Analyze.phi_of_blocks g var bl globals in
+let infer_phi (g : global_env) (var : commute_variant) (bl : block node list) (globals : ty bindlist) pre post : exp node =
+  let e = Analyze.phi_of_blocks g var bl globals pre post in
   no_loc e
 
 let rec infer_phis_of_block (g : global_env) (defs : ty bindlist) (body : block node) : block node =
@@ -663,7 +683,7 @@ let rec infer_phis_of_block (g : global_env) (defs : ty bindlist) (body : block
   let h,t = List.hd body.elt, node_app List.tl body in
   match h.elt with
   | Assn _ | Ret _ | SCall _ | SCallRaw _
-  | Raise _ | Assert _ | Assume _  | Havoc _ -> 
+  | Raise _ | Assert _ | Assume _  | Havoc _ | Require _ -> 
     node_app
     (List.cons h)
     (infer_phis_of_block g defs t)
@@ -691,10 +711,10 @@ let rec infer_phis_of_block (g : global_env) (defs : ty bindlist) (body : block
     node_app
       (List.cons (node_up h s))
       (infer_phis_of_block g defs t)
-  | Commute (var,phi,bl) ->
+  | Commute (var,phi,bl, pre, post) ->
     let bl = List.map (infer_phis_of_block g defs) bl in
     let phi' =
-      let infer () = let phi' = infer_phi g var bl defs in
+      let infer () = let phi' = infer_phi g var bl defs pre post in
         if !emit_inferred_phis then
           begin if !emit_quiet
           then Printf.printf "%s\n"
@@ -707,7 +727,7 @@ let rec infer_phis_of_block (g : global_env) (defs : ty bindlist) (body : block
       in match phi with
     | PhiExp e -> if !force_infer then infer () else e
     | PhiInf -> infer ()
-    in let s = Commute (var, PhiExp phi', bl) in
+    in let s = Commute (var, PhiExp phi', bl, pre, post) in
     node_app
       (List.cons (node_up h s))
       (infer_phis_of_block g defs t)
@@ -756,14 +776,14 @@ let rec verify_phis_of_block (g : global_env) (defs : ty bindlist) (body : block
     node_app
       (List.cons (node_up h s))
       (verify_phis_of_block g defs t)
-  | Commute (var,phi,bl) ->
+  | Commute (var,phi,bl,pre,post) ->
     let bl = List.map (verify_phis_of_block g defs) bl in
     begin match phi with
       | PhiExp e ->
         if !print_cond then 
           Printf.printf "%s\n" (AstPP.string_of_exp e);
 
-        begin match Analyze.verify_of_block e g var bl defs with
+        begin match Analyze.verify_of_block e g var bl defs pre post with
         | Some b, compl -> 
           let compl_str = 
             match compl with 
@@ -792,7 +812,7 @@ let rec verify_phis_of_block (g : global_env) (defs : ty bindlist) (body : block
           else print_string "failure\n"
         end
       | PhiInf -> () end;
-    let s = Commute (var, phi, bl) in
+    let s = Commute (var, phi, bl, pre, post) in
     node_app
       (List.cons (node_up h s))
       (verify_phis_of_block g defs t)
@@ -907,19 +927,28 @@ let cook_calls (g : global_env) : global_env =
       While (cook_calls_of_exp e, cook_calls_of_block b)
     | Raise e ->
       Raise (cook_calls_of_exp e)
-    | Commute (v, c, bl) ->
+    | Commute (v, c, bl, pre, post) ->
       let c =
         match c with
         | PhiExp e -> PhiExp (cook_calls_of_exp e)
         | PhiInf -> PhiInf
       in
-      Commute (v, c, List.map cook_calls_of_block bl)
+      let pre_exp, post_exp = begin match pre, post with 
+      | None, None -> pre, post
+      | Some pr, None -> Some (cook_calls_of_exp pr), post
+      | None, Some po -> pre, Some (cook_calls_of_exp po)
+      | Some pr, Some po -> Some (cook_calls_of_exp pr), Some (cook_calls_of_exp po)
+      end
+      in
+      Commute (v, c, List.map cook_calls_of_block bl, pre_exp, post_exp)
     | Assert e ->
       Assert (cook_calls_of_exp e)
     | Assume e ->
       Assume (cook_calls_of_exp e)
     | Havoc id ->
       Havoc id
+    | Require e ->
+      Require (cook_calls_of_exp e)
     in
     node_up s s'
 
diff --git a/src/vcy/run.ml b/src/vcy/run.ml
index 864f999..02b6f17 100644
--- a/src/vcy/run.ml
+++ b/src/vcy/run.ml
@@ -418,6 +418,10 @@ module RunInfer : Runner = struct
   let prover_name = ref ""
   let output_file = ref ""
   let timeout = ref None
+  let lattice = ref false
+  let lattice_timeout = ref (Some 30.)
+  let stronger_pred_first = ref false
+  let no_cache = ref true
 
   let speclist =
     [ "-d",      Arg.Set debug, " Display verbose debugging info during interpretation"
@@ -426,6 +430,18 @@ module RunInfer : Runner = struct
     ; "-q", Arg.Set quiet, " Quiet - just display conditions"
     (* ; "--poke", Arg.Unit (fun () -> Choose.choose := Choose.poke), " Use servois poke heuristic (default: simple)"
     ; "--poke2", Arg.Unit (fun () -> Choose.choose := Choose.poke2), " Use improved poke heuristic (default: simple)" *)
+    ;"--poke", Arg.Unit (fun () -> Servois2.Choose.choose := Servois2.Choose.poke), " Use servois poke heuristic (default: simple)"
+    ; "--poke2", Arg.Unit (fun () -> Servois2.Choose.choose := Servois2.Choose.poke2), " Use improved poke heuristic (default: simple)"
+    ; "--mcpeak-bisect", Arg.Unit (fun () -> Servois2.Choose.choose := Servois2.Choose.mc_bisect), " Use model counting based synthesis with strategy: bisection"    
+    ; "--mcpeak-max", Arg.Unit (fun () -> Servois2.Choose.choose := Servois2.Choose.mc_max), " Use model counting based synthesis with strategy: maximum-coverage"
+    ; "--mcpeak-max-poke2", Arg.Unit (fun () -> Servois2.Choose.choose := Servois2.Choose.mc_max_poke), " Use model counting based synthesis with strategy: maximum-coverage, then poke2"
+    ; "--lattice-timeout", Arg.Float (fun f -> lattice_timeout := Some f), " Set the time limit for lattice construction"
+    ; "--stronger-pred-first", Arg.Unit (fun () -> stronger_pred_first := true), " Choose stronger predicates first"
+    ; "--lattice", Arg.Unit (fun () -> lattice := true), " Create and use lattice of predicate implication"
+    ; "--timeout", Arg.Float (fun f -> timeout := Some f), " Set time limit for execution"
+    ; "--auto-terms", Arg.Unit (fun () -> Servois2.Predicate.autogen_terms := true), " Automatically generate terms from method specifications"
+    ; "--cache", Arg.Unit (fun () -> no_cache := false), " Use cached implication lattice" 
+    
     ; "--verbose", Arg.Set Servois2.Util.verbosity, " Servois2 verbose output"
     ; "--very-verbose", Arg.Set Servois2.Util.very_verbose, " Very verbose output and print smt query files"
     ; "--prover", Arg.Set_string prover_name, "<name> Use a particular prover (default: CVC4)"
@@ -472,7 +488,11 @@ module RunInfer : Runner = struct
     Arg.parse speclist anon_fun (usage_msg Sys.argv.(0));
     let anons = List.rev (!anons) in
     let synth_options = {
-      Servois2.Synth.default_synth_options with prover = get_prover (); timeout = !timeout
+      Servois2.Synth.default_synth_options with prover = get_prover (); timeout = !timeout; 
+                                        lattice = !lattice;
+                                        lattice_timeout = !lattice_timeout;
+                                         no_cache = !no_cache;
+                                         stronger_predicates_first = !stronger_pred_first;
     } in
     Util.servois2_synth_option := synth_options;
     match anons with
diff --git a/src/vcy/vcy_lexer.mll b/src/vcy/vcy_lexer.mll
index 82c0f08..7ebf6ad 100644
--- a/src/vcy/vcy_lexer.mll
+++ b/src/vcy/vcy_lexer.mll
@@ -43,6 +43,8 @@
   ("hashtable", HASHTABLE);
   ("hashtable_seq", HASHTABLE_SEQ);
   ("hashtable_naive", HASHTABLE_NAIVE);
+  ("pre", PRE);
+  ("post", POST);
 
   (* Symbols *)
   ( ";", SEMI);
diff --git a/src/vcy/vcy_parser.mly b/src/vcy/vcy_parser.mly
index f6d0233..86442a5 100644
--- a/src/vcy/vcy_parser.mly
+++ b/src/vcy/vcy_parser.mly
@@ -78,6 +78,7 @@ let loc (startpos:Lexing.position) (endpos:Lexing.position) (elt:'a) : 'a node =
 %token PURE
 
 %token ASSERT ASSUME HAVOC
+%token PRE POST
 
 %token UNDERSCORE
 
@@ -248,8 +249,8 @@ stmt:
   | FOR LPAREN vdecls=separated_list(COMMA, vdecl) SEMI e=option(exp) SEMI s=option(stmt) RPAREN b=block
       {loc $startpos $endpos @@ For(vdecls, e, s, b)}
   | variant=commute_variant phi=commute_condition
-    LBRACE blocks=nonempty_list(block) RBRACE
-    { loc $startpos $endpos @@ Commute(variant,phi,blocks) }
+    LBRACE option(PRE) option(COLON) pre=option(exp) blocks=nonempty_list(block) option(POST) option(COLON) post=option(exp) RBRACE
+    { loc $startpos $endpos @@ Commute(variant,phi,blocks,pre,post) }
   | RAISE e=exp SEMI { loc $startpos $endpos @@ Raise e }
   | ASSERT e=exp SEMI { loc $startpos $endpos @@ Assert e }
   | ASSUME e=exp SEMI { loc $startpos $endpos @@ Assume e }
@@ -274,4 +275,4 @@ if_stmt:
 else_stmt:
   | (* empty *)       { loc $startpos $endpos @@ [] }
   | ELSE b=block      { b }
-  | ELSE ifs=if_stmt  { loc $startpos $endpos @@ [ ifs ] }
+  | ELSE ifs=if_stmt  { loc $startpos $endpos @@ [ ifs ] }
\ No newline at end of file