diff --git a/Gillian-C/lib/gilgen.ml b/Gillian-C/lib/gilgen.ml
index a2a5ac0ff..3473298d1 100644
--- a/Gillian-C/lib/gilgen.ml
+++ b/Gillian-C/lib/gilgen.ml
@@ -888,7 +888,8 @@ let is_builtin_func func_name =
   List.mem func_name builtins
 
 let is_gil_func func_name exec_mode =
-  Exec_mode.is_symbolic_exec exec_mode
+  (Exec_mode.is_symbolic_exec exec_mode
+  || Exec_mode.is_verification_exec exec_mode)
   && (String.equal func_name Builtin_Functions.assume_f
      || String.equal func_name Builtin_Functions.assert_f)
 
diff --git a/Gillian-C/scripts/testSymb.sh b/Gillian-C/scripts/testSymb.sh
index a6d5ad277..489b89425 100755
--- a/Gillian-C/scripts/testSymb.sh
+++ b/Gillian-C/scripts/testSymb.sh
@@ -34,3 +34,22 @@ printf "\n\n"
 echo "--- testing BST ---"
 $WPST symbolic/bst.c -l disabled
 printf "\n\n"
+
+echo "--- testing globalvar ---"
+$WPST symbolic/globalvar.c -l disabled
+printf "\n\n"
+
+echo "--- testing unstructured ---"
+$WPST symbolic/unstructured.c -l disabled
+printf "\n\n"
+
+# Expected-failure test: array_oob.c contains an out-of-bounds bug that
+# symbolic testing must catch, so a zero exit code here is itself a failure.
+echo "--- testing array_oob (expect failure: out-of-bounds bug) ---"
+if $WPST symbolic/bug_examples/array_oob.c -l disabled; then
+  echo "ERROR: expected array_oob.c to fail, but it succeeded"
+  exit 1
+else
+  echo "(failed as expected)"
+fi
+printf "\n\n"
diff --git a/Gillian-C/scripts/testVerif.sh b/Gillian-C/scripts/testVerif.sh
index 885668eae..63c9069d0 100755
--- a/Gillian-C/scripts/testVerif.sh
+++ b/Gillian-C/scripts/testVerif.sh
@@ -23,3 +23,15 @@ printf "\n\n"
 echo "--- verifying sort ---"
 $VERIFY verification/sort.c -l disabled
 printf "\n\n"
+
+echo "--- verifying vector ---"
+$VERIFY verification/vector.c -l disabled
+printf "\n\n"
+
+echo "--- verifying array ---"
+$VERIFY verification/array.c -l disabled
+printf "\n\n"
+
+echo "--- verifying batch ---"
+$VERIFY verification/batch.c -l disabled
+printf "\n\n"
diff --git a/Gillian-JS/scripts/testJaVerT.sh b/Gillian-JS/scripts/testJaVerT.sh
index 6148cf9b3..b63025036 100755
--- a/Gillian-JS/scripts/testJaVerT.sh
+++ b/Gillian-JS/scripts/testJaVerT.sh
@@ -4,13 +4,39 @@ set -e
 
 if [[ "${GITHUB_ACTIONS}" ]]; then
 	VERIFY="gillian-js verify"
+	WPST="gillian-js wpst"
 else
   VERIFY="dune exec -- gillian-js verify"
+  WPST="dune exec -- gillian-js wpst"
 fi
 
 # Bash array format: ("one" "two" "three")
-# JS Files to test
-declare -a jsfiles=("BST" "PriQ" "SLL" "DLL" "Sort")
+# JaVerT verification examples to test
+declare -a jsfiles=("BST" "PriQ" "SLL" "DLL" "Sort" "ExprEval" "IDGen" "KVMap" "annotated/SLL")
+
+# Cosette symbolic-testing (wpst) case studies, relative to Examples/
+declare -a wpstfiles=(
+	"Cosette/CaseStudies/BST/bst_find_1"
+	"Cosette/CaseStudies/BST/bst_find_min_1"
+	"Cosette/CaseStudies/BST/bst_insert_1"
+	"Cosette/CaseStudies/BST/bst_remove_1"
+	"Cosette/CaseStudies/DLL/dll"
+	"Cosette/CaseStudies/ExprEval/exprEval_3"
+	"Cosette/CaseStudies/ExprEval/exprEval_4"
+	"Cosette/CaseStudies/ExprEval/exprEval_5"
+	"Cosette/CaseStudies/ExprEval/exprEval_6"
+	"Cosette/CaseStudies/ExprEval/exprEval_7"
+	"Cosette/CaseStudies/IDGen/IdGen"
+	"Cosette/CaseStudies/KVMap/kv_map_1"
+	"Cosette/CaseStudies/KVMap/kv_map_2"
+	"Cosette/CaseStudies/PriQ/pri_q_1"
+	"Cosette/CaseStudies/PriQ/pri_q_2"
+	"Cosette/CaseStudies/SLL/sll"
+	"Cosette/CaseStudies/Sort/sort_1"
+	"Cosette/CaseStudies/Sort/sort_2"
+	"Cosette/simple_example"
+	"Cosette/check_div_by_zero"
+)
 
 FINAL_RETURN=0
 
@@ -36,4 +62,21 @@ do
 	if [[ $rc != 0 ]]; then FINAL_RETURN=1; fi
 	echo "----------------"
 done
+
+echo "Symbolic-testing (wpst) Cosette case studies"
+echo "--------------------------------------------"
+for f in "${wpstfiles[@]}"
+do
+  sleep 1
+	echo "Testing: $f.js"
+	if [[ $1 == "count" ]]; then
+		$WPST Examples/$f.js -l disabled --stats
+		rc=$?
+	else
+		$WPST Examples/$f.js -l disabled
+		rc=$?
+	fi
+	if [[ $rc != 0 ]]; then FINAL_RETURN=1; fi
+	echo "----------------"
+done
 exit $FINAL_RETURN
diff --git a/GillianCore/smt/smt.ml b/GillianCore/smt/smt.ml
index c5b567b84..0fa32946b 100644
--- a/GillianCore/smt/smt.ml
+++ b/GillianCore/smt/smt.ml
@@ -607,7 +607,9 @@ let encode_binop (op : BinOp.t) (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t
   | FPlus -> num_add (get_num p1) (get_num p2) >- NumberType
   | FMinus -> num_sub (get_num p1) (get_num p2) >- NumberType
   | FTimes -> num_mul (get_num p1) (get_num p2) >- NumberType
-  | FDiv -> num_div (get_num p1) (get_num p2) >- NumberType
+  (* Numbers are encoded as reals, so float division must use SMT-LIB real
+     division ["/" *)
+  | FDiv -> app_ "/" [ get_num p1; get_num p2 ] >- NumberType
   | FLessThan -> num_lt (get_num p1) (get_num p2) >- BooleanType
   | FLessThanEqual -> num_leq (get_num p1) (get_num p2) >- BooleanType
   | Equal -> encode_equality p1 p2
diff --git a/wisl/examples/Array.wisl b/wisl/examples/Array.wisl
deleted file mode 100644
index cd325f14b..000000000
--- a/wisl/examples/Array.wisl
+++ /dev/null
@@ -1,11 +0,0 @@
-predicate array(+x, alpha : List) {
-    (x == null) * (alpha == nil);
-    (x -> #s, #c, #b) * (#s <= #c) * (#c == len(#b)) * (#s == len(alpha)) * (#b == (alpha @ #beta))
-}
-
-{ (#x == x) * list(#x, #alpha) }
-function llen(x) {
-  n := [x+1];
-  return n
-}
-{ list(#x, #alpha) * (ret == len(#alpha)) }
diff --git a/wisl/examples/SLL_ex_complete.wisl b/wisl/examples/SLL_ex_complete.wisl
index 930f2bbde..e66c6a397 100644
--- a/wisl/examples/SLL_ex_complete.wisl
+++ b/wisl/examples/SLL_ex_complete.wisl
@@ -52,7 +52,7 @@ lemma list_member_concat {
 }
 
 // 00. Allocating an SLL node with the given value
-{ v == #v }
+{ (v == #v) }
 function SLL_allocate_node(v){
   t := new(2);
   [t] := v;
@@ -146,7 +146,7 @@ function SLL_length(x) {
   };
   return n
 }
-{ ret == len(#vs) }
+{ (ret == len(#vs)) }
 
 // 07. Reversing a given SLL
 { (x == #x) *  SLL(#x, #vs) }
@@ -296,7 +296,7 @@ function SLL_append_iter(x, k){
           SLLseg(head, prev, #vs1) * (prev -b> #v, next) * SLL(next,  #vs2) *
            (#vx == #vs1 @ (#v :: #vs2)) ]];
     while(next != null){
-      [[ assert {bind: #prev} prev == #prev ]];
+      [[ assert {bind: #prev} (prev == #prev) ]];
       prev := next;
       next := [next + 1];
       [[ apply SLLseg_append(head,  #vs1, #v, prev) ]]
@@ -324,7 +324,7 @@ function SLL_append_node_iter(x, y){
           SLLseg(head, prev, #vs1) * (prev -b> #v, next) * SLL(next,  #vs2) *
            (#vx == #vs1 @ (#v :: #vs2)) ]];
     while(next != null){
-      [[ assert {bind: #prev} prev == #prev ]];
+      [[ assert {bind: #prev} (prev == #prev) ]];
       prev := next;
       next := [next + 1];
       [[ apply SLLseg_append(head,  #vs1, #v, prev) ]]
@@ -352,7 +352,7 @@ function SLL_concat_iter(x, y){
           SLLseg(head, prev, #vs1) * (prev -b> #v, next) * SLL(next,  #vs2) *
            (#vx == #vs1 @ (#v :: #vs2)) ]];
     while (next != null) {
-        [[ assert {bind: #prev} prev == #prev ]];
+        [[ assert {bind: #prev} (prev == #prev) ]];
         prev := next;
         next := [next + 1];
         [[ apply SLLseg_append(head,  #vs1, #v, prev) ]]
@@ -413,7 +413,7 @@ function SLL_length_iter(x) {
       SLLseg(x, y,  #nvx) * SLL(y, #nvy) *
          (#vx == (#nvx@#nvy)) * (n == len #nvx) ]];
   while (y != null) {
-    [[ assert {bind: #y} y == #y ]];
+    [[ assert {bind: #y} (y == #y) ]];
     [[ assert {bind: #v, #z} #y -b> #v, #z ]];
     y := [y+1];
     n := n+1;
@@ -451,8 +451,8 @@ function SLL_member_iter(x, k) {
          (#alpha == (#beta @ #gamma)) * (#r == (found || #rg)) *
            list_member(#beta, k, found) * list_member(#gamma, k, #rg) ]];
   while ((found == false) && (next != null)){
-    [[ assert found == false ]];
-    [[ assert {bind: #next} next == #next ]];
+    [[ assert (found == false) ]];
+    [[ assert {bind: #next} (next == #next) ]];
     [[ assert {bind: #v, #z} #next -b> #v, #z ]];
     v := [next];
     found := (v == k);
diff --git a/wisl/examples/SLL_ex_ongoing.wisl b/wisl/examples/SLL_ex_ongoing.wisl
index 9eecc39b8..c930be1ed 100644
--- a/wisl/examples/SLL_ex_ongoing.wisl
+++ b/wisl/examples/SLL_ex_ongoing.wisl
@@ -57,7 +57,7 @@ predicate SLL_len(+x, n : Int) {
 // With length
 predicate SLLseg_len(+x, y, n : Int) {
   (x == y) * (n == 0);
-  (x -b> #v, #z) * SLLseg_len(#z, y, n - 1) * (0 <# n)
+  (x -b> #v, #z) * SLLseg_len(#z, y, n - 1) * (0 < n)
 }
 
 // With values
@@ -146,7 +146,7 @@ lemma SLLseg_vals_to_SLL_vals {
 lemma SLLseg_len_append_lr {
   statement:
     forall x.
-      SLLseg_len(#x, #y, #n) * (#y -b> #v, #z) |- SLLseg_len(#x, #z, #n + 1) * (0 <=# #n)
+      SLLseg_len(#x, #y, #n) * (#y -b> #v, #z) |- SLLseg_len(#x, #z, #n + 1) * (0 <= #n)
 
   variant: #n
 
@@ -163,7 +163,7 @@ lemma SLLseg_len_append_lr {
 lemma SLLseg_len_append_rl {
   statement:
     forall x.
-      SLLseg_len(#x, #z, #n + 1) * (0 <=# #n) |- SLLseg_len(#x, #y, #n) * (#y -b> #v, #z)
+      SLLseg_len(#x, #z, #n + 1) * (0 <= #n) |- SLLseg_len(#x, #y, #n) * (#y -b> #v, #z)
 
   variant: #n
 
@@ -461,7 +461,7 @@ function SLL_member_iter(x, k) {
            list_member(#beta, k, found) * list_member(#gamma, k, #rg)
      with variant: (len #gamma) ]] ;
   while ((found == false) && (next != null)) {
-    [[ assert found == false ]];
+    [[ assert (found == false) ]];
     [[ assert {bind: #v} next -> #v ]];
     v := [ next ];
     found := (v == k);
diff --git a/wisl/examples/loop.wisl b/wisl/examples/loop.wisl
index d9600708a..d5bd3010f 100644
--- a/wisl/examples/loop.wisl
+++ b/wisl/examples/loop.wisl
@@ -9,35 +9,33 @@ predicate lseg(+x, +y, alpha) {
   (x -> #a, #z) * (alpha == #a :: #beta) * lseg(#z, y, #beta)
 }
 
-lemma lseg_to_list(x, alpha) {
+lemma lseg_to_list {
+  statement:
+    forall x, alpha.
+      (x == #x) * (alpha == #alpha) * lseg(#x, null, #alpha) |- list(#x, #alpha)
   variant: len alpha
-  hypothesis: (x == #x) * (alpha == #alpha) * lseg(#x, null, #alpha)
-  conclusion: list(#x, #alpha)
   proof: unfold lseg(#x, null, #alpha);
          if (#x == null) {
            fold list(#x, #alpha)
          } else {
-           assert {exists: #next, #beta} (#x + 1 -> #next) * lseg(#next, null, #beta);
+           assert {bind: #next, #beta} (#x + 1 -> #next) * lseg(#next, null, #beta);
            apply lseg_to_list(#next, #beta);
            fold list(#x, #alpha)
          }
 }
 
-lemma lseg_append(x, y, alpha, a, z) {
+lemma lseg_append {
+  statement:
+    forall x, y, alpha, a, z.
+      (x == #x) * (y == #y) * (alpha == #alpha) * (a == #a) * (z == #z) *
+      lseg(#x, #y, #alpha) *
+      (#y -> #a, #z) |- lseg(#x, #z, #alpha @ [ #a ])
   variant: len alpha
-  
-  hypothesis: (x == #x) * (y == #y) * (alpha == #alpha) * (a == #a) * (z == #z) *
-              lseg(#x, #y, #alpha) * 
-              (#y -> #a, #z) 
-
-  conclusion: lseg(#x, #z, #alpha @ [ #a ])
-  
-
   proof: unfold lseg(#x, #y, #alpha);
          if (#alpha == []) {
            fold lseg(#x, #z, #alpha @ [#a])
          } else {
-           assert {exists: #next, #beta} (#x + 1 -> #next) * lseg(#next, #y, #beta);
+           assert {bind: #next, #beta} (#x + 1 -> #next) * lseg(#next, #y, #beta);
            apply lseg_append(#next, #y, #beta, #a, #z); 
            fold lseg(#x, #z, #alpha @ [#a])
          } 
@@ -47,16 +45,17 @@ lemma lseg_append(x, y, alpha, a, z) {
 function llen(x) {
   y := x;
   n := 0;
-  [[ fold lseg(#x, y, []) ]];
-  [[ invariant {exists: #a1, #a2} lseg(#x, y, #a1) * list(y, #a2) * (#alpha == #a1 @ #a2) * (n == len #a1) ]];
+  [[ fold lseg(x, y, []) ]];
+  [[ invariant {bind: y, n, #a1, #a2} lseg(x, y, #a1) * list(y, #a2) * (#alpha == #a1 @ #a2) * (n == len #a1) ]];
   while (y != null) {
     [[ unfold list(y, #a2) ]];
-    [[ assert {exists: #y, #b, #t} (y == #y) * (#y -> #b, #t) ]];
+    [[ assert {bind: #y, #b, #t} (y == #y) * (#y -> #b, #t) ]];
     y := [y+1];
     n := n+1;
-    [[ apply lseg_append(#x, #y, #a1, #b, #t) ]]
+    [[ apply lseg_append(x, #y, #a1, #b, #t) ]]
   };
-  [[ apply lseg_to_list(#x, #alpha) ]];
+  [[ unfold list(y, #a2) ]];
+  [[ apply lseg_to_list(x, #alpha) ]];
   return n
 }
 { list(#x, alpha) * (ret == len(#alpha)) }
diff --git a/wisl/examples/sll_cc.wisl b/wisl/examples/sll_cc.wisl
deleted file mode 100644
index 9a246195b..000000000
--- a/wisl/examples/sll_cc.wisl
+++ /dev/null
@@ -1,212 +0,0 @@
-predicate sll(+x, alpha) {
-    // empty
-    (x == null) * (alpha == nil);
-    // non-empty
-    (x -b> #v, #z) * sll(#z, #beta) * (alpha == #v::#beta)
-}
-predicate lseg(+x, +y, alpha) {
-  (x == y) * (alpha == nil);
-  (x -b> #v, #z) * lseg(#z, y, #beta) * (alpha == #v::#beta)
-}
-
-predicate cc_sll_ht(+x, +h, +t, alpha) {
-  // Full cc_slist_s object: length, head, tail
-  (x -b> 0, h, t) *
-  (alpha == []) *
-  (h == null) * (t == null);
-
-  (x -b> l, h, t) *
-  (h == #h) * (t == #t) *
-  lseg(#h, #t, #beta) *
-  sll(#t, [ #last ]) *
-  (alpha == #beta @ [ #last ]) *
-  (l == (len #beta) + 1)
-}
-
-predicate cc_sll(+x, alpha) {
-  cc_sll_ht(x, #h, #t, alpha)
-}
-
-lemma lseg_to_sll {
-  statement:
-    forall x, alpha.
-      lseg(x, null, alpha) |- sll(x, alpha)
-
-  proof:
-    unfold lseg(x, null, alpha);
-    if (x != null) {
-      assert {bind:  #next, #beta} (x + 1 -> #next) * lseg(#next, null, #beta) ;
-      apply lseg_to_sll(#next, #beta);
-      fold sll(x, #alpha)
-    } else {
-      fold sll(x, #alpha)
-    }
-}
-
-
-lemma concat_lseg_sll {
-  statement:
-    forall x, y, alpha, beta.
-      lseg(x, y, alpha) * sll(y, beta) |- sll(x, alpha @ beta)
-
-  proof:
-    unfold sll(y, beta);
-    if (y == null) {
-      apply lseg_to_sll(x, alpha)
-    } else {
-      assert (y != null);
-      unfold sll(y, beta);
-      assert {bind: #z, #t, #rest} (y -> #z, #t) * sll(#t, #rest) * (beta == #z::#rest);
-      apply lseg_append(x, y, alpha, #z, #t);
-      apply concat_lseg_sll(x, #t, alpha @ [ #z ], #rest)
-    }
-}
-
-lemma lseg_append {
-  statement:
-    forall x, y, alpha, yval, ynext.
-      lseg(x, y, alpha) * (y -b> yval, ynext) |- lseg(x, ynext, alpha @ [ yval ])
-
-  proof:
-    unfold lseg(x, y, alpha);
-    if (alpha != []) {
-      assert {bind: #next, #beta} (x + 1 -> #next) * lseg(#next, y, #beta) ;
-      apply lseg_append(#next, y, #beta, yval, ynext);
-      fold lseg(x, ynext, alpha @ [yval])
-    } else {
-      fold lseg(x, ynext, alpha @ [yval])
-    }
-}
-
-
-{ true }
-function cc_slist_new() {
-  l := new(3);
-  [l] := 0;
-  return l
-}
-{ cc_sll(ret, []) }
-
-{ (v == #v) * (x == #x) * cc_sll(#v, #vs) }
-function cc_slist_add_first(v, x) {
-  node := new(2);
-  [node] := x;
-  size := [v];
-  if (size == 0) {
-    [v + 1] := node;
-    [v + 2] := node;
-    [[ fold lseg(node, node, []) ]];
-    [[ fold sll(node, [ #x ]) ]];
-    [[ fold cc_sll(v, [ #x ]) ]]
-  } else {
-    [[ assert {bind: #l, #h, #t, #beta} (#v -b> #l, #h, #t) * lseg(#h, #t, #beta) ]];
-    head := [v + 1];
-    [node + 1] := head;
-    [v + 1] := node;
-    [[ fold lseg(node, #t, #x :: #beta) ]]
-  };
-  [v] := size + 1;
-  return v
-}
-{ cc_sll(ret, #x::#vs) }
-
-{ (v == #v) * cc_sll(#v, #vs) * (x == #x) }
-function cc_slist_add_last(v, x)
-{
-  node := new(2);
-  [node] := x;
-  size := [v];
-  if (size == 0) {
-    [v + 1] := node;
-    [v + 2] := node
-  } else {
-    [[ assert {bind: #l, #h, #t, #beta, #last}
-      (#v -b> #l, #h, #t) * lseg(#h, #t, #beta) * sll(#t, [ #last ]) ]];
-    [[ unfold sll(#t, [ #last ]) ]];
-    tail := [v + 2];
-    [tail + 1] := node;
-    [[ apply lseg_append(#h, #t, #beta, #last, node) ]];
-    [[ fold sll(node, [ #x ]) ]];
-    [v + 2] := node
-  };
-  [v] := size + 1;
-  return v
-}
-{ cc_sll(ret, #vs @ [ #x ]) }
-
-{ (v == #v) * (i == #i) * cc_sll(#v, #vs) * (0 <= #i) * (#i < (len #vs)) * (#vs != nil) }
-function get_node_at(v, i) {
-    size := [v];
-    if (i >= size) {
-        r := null
-    } else {
-      node := [v + 1];
-      prev := null;
-      j := 0;
-      [[ assert {bind: #beta, #last } (#h == n) * lseg(#h, #t, #beta) * sll(#t, #end) ]];
-      [[ apply concat_lseg_sll(#h, #t, #beta, #end) ]];
-      [[ invariant {bind: node, j, #end, #next}
-        (node -b> #vs lnth j, #next) * sll(node, #end) ]];
-      while (j < i) {
-          prev := node;
-          node := [node + 1];
-          j := j + 1
-      };
-      r := new(2);
-      [r] := node;
-      [r + 1] := prev
-    };
-    return r
-}
-{ (ret -b> #val, #prev) * cc_sll(#v, #vs) * (#val == #vs lnth #i) }
-
-
-{ cc_sll(v, #vs) }
-function cc_slist_destroy(v) {
-    x := cc_slist_remove_all(v);
-    free(v);
-    return null
-}
-{ (ret == null) }
-
-
-{ cc_sll(v, #vs) * (v == #v) }
-function cc_slist_remove_all(v) {
-  x := unlinkn_all(v);
-  if (x == true) {
-    [v + 1] := null;
-    [v + 2] := null
-  } else { skip };
-  return v
-}
-{ (ret == #v) * cc_sll(#v, []) }
-
-
-{ cc_sll_ht(v, #h, #t, #vs) * (v == #v) }
-function unlinkn_all(v) {
-  size := [v];
-  if (size == 0) {
-    non_emp := false
-  } else {
-    n := [v + 1];
-    [[ assert {bind: #beta, #last } (#h == n) * lseg(#h, #t, #beta) * sll(#t, [ #last ]) ]];
-    [[ apply concat_lseg_sll(#h, #t, #beta, [ #last ]) ]];
-    [[ invariant {bind: n, size, #w}
-      sll(n, #w) *
-      (size == len #w) *
-      v -b> size, #h, #t ]];
-    while (n != null) {
-      [[ assert {bind: #fst, #rest} (#w == #fst::#rest) ]];
-      tmp := [n + 1];
-      free(n);
-      n := tmp;
-      size := size - 1;
-      [v] := size;
-      [[ fold sll(n, #rest) ]]
-    };
-    [[ assert sll(n, nil) ]];
-    non_emp := true
-  };
-  return non_emp
-}
-{ (ret == (#vs != [])) * (#v -b> 0, #h, #t) }
diff --git a/wisl/examples/tree.wisl b/wisl/examples/tree.wisl
index 15d79de7f..11e4fceb0 100644
--- a/wisl/examples/tree.wisl
+++ b/wisl/examples/tree.wisl
@@ -1,6 +1,6 @@
 predicate tree(+t) {
     (t == null);
-    (t -b-> #v, #left, #right) * tree(#left) * tree(#right)
+    (t -b> #v, #left, #right) * tree(#left) * tree(#right)
 }
 
 { (x == #x) * tree(#x) }
@@ -10,7 +10,7 @@ function tree_dispose(x) {
     z := [x+2];
     u := tree_dispose(y);
     u := tree_dispose(z);
-    delete(x)
+    free(x)
   } else {
     skip
   };
diff --git a/wisl/examples/wand.wisl b/wisl/examples/wand.wisl
index b2f641a04..93a2687e4 100644
--- a/wisl/examples/wand.wisl
+++ b/wisl/examples/wand.wisl
@@ -31,27 +31,27 @@ predicate xpt(+x) {
 
 
 predicate leq_five(+x) {
-  x <=# 5
+  (x <= 5)
 }
 
 predicate eq_five(+x) {
-  x == 5
+  (x == 5)
 }
 
 predicate leq_six(+x) {
-  x <=# 6
+  (x <= 6)
 }
 
 lemma pure_wand {
   statement:
-    forall x. (5 <=# x) |- (leq_five(x) -* eq_five(x))
+    forall x. (5 <= x) |- (leq_five(x) -* eq_five(x))
   proof:
     package (leq_five(x) -* eq_five(x))
 }
 
 lemma pure_wand_fail {
   statement:
-    forall x. (5 <=# x) |- (leq_six(x) -* eq_five(x))
+    forall x. (5 <= x) |- (leq_six(x) -* eq_five(x))
   proof:
     package (leq_six(x) -* eq_five(x))
 }
diff --git a/wisl/scripts/quicktests.sh b/wisl/scripts/quicktests.sh
index 1852eeebb..c808d02f2 100755
--- a/wisl/scripts/quicktests.sh
+++ b/wisl/scripts/quicktests.sh
@@ -5,12 +5,48 @@ verify () {
   wisl verify $1 -l disabled
 }
 
+verify_frac () {
+  echo "\nVerifying (frac): $1\n"
+  wislf verify $1 -l disabled
+}
+
+# Runs an analysis that is EXPECTED to fail (the file contains deliberately
+# failing specs/lemmas, or demonstrates a bug) and errors out if it
+# unexpectedly succeeds. $1: file, $2: command (e.g. "wisl verify").
+expect_fail () {
+  echo "\nExpecting failure of: $2 $1\n"
+  if $2 $1 -l disabled; then
+    echo "ERROR: expected $1 to fail, but it succeeded"
+    exit 1
+  else
+    echo "(failed as expected)"
+  fi
+}
+
 echo "--- WISL: OX VERIFICATION ---"
 verify wisl/examples/SLL_recursive.wisl
 verify wisl/examples/SLL_iterative.wisl
 verify wisl/examples/DLL_recursive.wisl
+verify wisl/examples/loop.wisl
+verify wisl/examples/tree.wisl
+verify wisl/examples/SLL_ex_complete.wisl
+verify wisl/examples/SLL_ex_ongoing.wisl
+
+echo "\n\n--- WISL: FRACTIONAL-PERMISSION VERIFICATION ---"
+verify_frac wisl/examples/frac/concurrent_binary_tree.wisl
+verify_frac wisl/examples/frac/floating_point.wisl
+verify_frac wisl/examples/frac/concrete_test.wisl
+verify_frac wisl/examples/frac/lambda_terms.wisl
+
+echo "\n\n--- WISL: EXPECTED-FAILURE TESTS (deliberately failing specs / bugs) ---"
+# wand.wisl contains 'should_fail' / 'pure_wand_fail' lemmas.
+expect_fail wisl/examples/wand.wisl "wisl verify"
+# simple_concurrency.wisl contains 'SHOULD_FAIL_*' procedures.
+expect_fail wisl/examples/frac/simple_concurrency.wisl "wislf verify"
+# llen_wpst.wisl asserts a property that is violated for some inputs.
+expect_fail wisl/examples/wpst/llen_wpst.wisl "wisl wpst"
 
 # echo "\n\n--- WISL: EXACT VERIFICATION ---"
 # verify_exv wisl/examples/SLL_ex_ongoing.wisl
 
-exit $FINAL_RETURN
\ No newline at end of file
+exit $FINAL_RETURN