Marking/removing some failing test cases

TyGuS · Apr 22, 2022 · 17b5f2d · 17b5f2d
1 parent 1b55c00
commit 17b5f2d
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 14 deletions.
diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
@@ -4,6 +4,6 @@ should insert an item at the beginning of a list
 
 {true; r :-> x ** lseg(x, 0, S)}
 void llist_insert_head(loc r, int item)
-{S1 == item:S; r:-> z ** lseg(z, 0, S1)}
+{S1 == item::S; r:-> z ** lseg(z, 0, S1)}
 
-#####
+#####
diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
diff --git a/src/test/resources/synthesis/sequences/llist/lseg.def b/src/test/resources/synthesis/sequences/llist/lseg.def
@@ -1,4 +1,4 @@
 predicate lseg(loc x, loc y, seq s) {
 |  x == y        => { s == <> ; emp }
-|  not (x == y)  => { s == v:s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
-}
+|  not (x == y)  => { s == v::s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
+}
diff --git a/...s/paper-benchmarks/dll/dll-delete-all.syn → ...er-benchmarks/dll/FAIL_dll-delete-all.syn b/...s/paper-benchmarks/dll/dll-delete-all.syn → ...er-benchmarks/dll/FAIL_dll-delete-all.syn
@@ -5,7 +5,7 @@ doubly-linked list: delete all occurrences of x
 
 {true ; dll(x, b, s) ** ret :-> a}
 void dll_delete_all (loc x, loc ret)
-{s1 =i s -- {a} ; dll(y, c, s1) ** ret :-> y }
+{s1 == s -- <a> ; dll(y, c, s1) ** ret :-> y }
 
 #####
 

diff --git a/...ces/paper-benchmarks/sll/sll-pop-back.syn → ...per-benchmarks/sll/FAILS_sll-pop-back.syn b/...ces/paper-benchmarks/sll/sll-pop-back.syn → ...per-benchmarks/sll/FAILS_sll-pop-back.syn