diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
index 27e641409..eae537bf6 100644
--- 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)}
 
-#####
\ No newline at end of file
+#####
diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
deleted file mode 100644
index 201e5efbb..000000000
--- a/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
+++ /dev/null
@@ -1,9 +0,0 @@
-should insert an item at the beginning of a list
-
-#####
-
-{true; r :-> x ** lseg(x, 0, S)}
-void llist_insert_tail(loc r, int item)
-{S1 == <item>; r:-> z ** lseg(z, y, S) ** lseg(y, 0, S1)}
-
-#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/lseg.def b/src/test/resources/synthesis/sequences/llist/lseg.def
index 24ebdd087..858723c8d 100644
--- 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) }
-}
\ No newline at end of file
+|  not (x == y)  => { s == v::s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
+}
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/FAIL_dll-delete-all.syn
similarity index 93%
rename from src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn
rename to src/test/resources/synthesis/sequences/paper-benchmarks/dll/FAIL_dll-delete-all.syn
index cc83611fa..e578ffdf4 100644
--- a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn
+++ b/src/test/resources/synthesis/sequences/paper-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/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-pop-back.syn
similarity index 100%
rename from src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn
rename to src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-pop-back.syn