Skip to content

Commit

Permalink
Now also reverting the oracle change
Browse files Browse the repository at this point in the history
  • Loading branch information
nadia-polikarpova committed Jul 12, 2018
1 parent 25f7bbb commit 46fcc0a
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 9 deletions.
24 changes: 16 additions & 8 deletions src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

0 comments on commit 46fcc0a

Please sign in to comment.