Now also reverting the oracle change

TyGuS · Jul 12, 2018 · 46fcc0a · 46fcc0a
1 parent 25f7bbb
commit 46fcc0a
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 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
@@ -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;
+    }
   }
 }
diff --git 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;
 }