From 46fcc0ae7b68e7750081742e8e470688ad784e7b Mon Sep 17 00:00:00 2001
From: Nadia Polikarpova <nadia.polikarpova@gmail.com>
Date: Thu, 12 Jul 2018 04:45:16 -0700
Subject: [PATCH] Now also reverting the oracle change

---
 .../paper-benchmarks/srtl/srtl-insert.syn     | 24 ++++++++++++-------
 .../paper-benchmarks/srtl/srtl-prepend.syn    |  2 +-
 2 files changed, 17 insertions(+), 9 deletions(-)

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 5d15740f1..93ed09f11 100644
--- a/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn
+++ b/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn
@@ -14,15 +14,23 @@ 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 lo2 = *x;
-    let nxt2 = *(x + 1);
-    srtl_insert(nxt2, r);
-    let y12 = *r;
-    *x = k2 <= lo2 ? k2 : lo2;
-    *(x + 1) = y12;
-    *r = x;
+    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;
+    }
   }
 }
\ 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 8afea493b..78243df44 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 = k;
   *(y2 + 1) = x;
+  *y2 = k;
 }
\ No newline at end of file