diff --git a/test/viper/ok/todo_tuple.vpr.ok b/test/viper/ok/todo_tuple.vpr.ok
new file mode 100644
index 00000000000..78cc6c12f1f
--- /dev/null
+++ b/test/viper/ok/todo_tuple.vpr.ok
@@ -0,0 +1,370 @@
+/* BEGIN PRELUDE */
+/* Array encoding */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $loc_inv1(r: Ref): Array
+  function $loc_inv2(r: Ref): Int
+  axiom $all_diff_array { forall a: Array, i: Int :: {$loc(a, i)} $loc_inv1($loc(a, i)) == a && $loc_inv2($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+/* Tuple encoding */
+adt Tuple$3 [T0, T1, T2] { Tup$3(tup$3$0 : T0, tup$3$1 : T1, tup$3$2 : T2) }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
+/* Typed references */
+field $tuple3$int$int$c_State: Tuple$3[Int, Int, State]
+/* END PRELUDE */
+
+define $Perm($Self) ((((true && (acc(($Self).todos,write) && $array_acc(
+                                                             ($Self).todos,
+                                                             $tuple3$int$int$c_State,
+                                                             write))) && 
+  acc(($Self).num,write)) && acc(($Self).nextId,write)))
+define $Inv($Self) (invariant_14($Self))
+method __init__($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var $t_todos: Array
+      inhale $array_acc($t_todos, $tuple3$int$int$c_State, write);
+      inhale ($size($t_todos) == 0);
+      ($Self).todos := $t_todos;
+      ($Self).num := 0;
+      ($Self).nextId := 1; 
+    }
+adt State  { DONE()
+             TODO() }
+field todos: Array
+field num: Int
+field nextId: Int
+define invariant_14($Self) (((0 <= ($Self).num) && (($Self).num <= $size(
+                                                                   ($Self).todos))))
+method resize($Self: Ref, n: Int)
+    
+    requires $Perm($Self)
+    requires ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+    ensures $Perm($Self)
+    ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+    ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+      old(($Self).nextId)))
+    ensures ($size(($Self).todos) >= n)
+    ensures (old($size(($Self).todos)) <= $size(($Self).todos))
+    ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> (
+            ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old((
+                                                                    $loc(
+                                                                    ($Self).todos,
+                                                                    i)).$tuple3$int$int$c_State))))
+    { var new_array: Array
+      var i: Int
+      if ((n <= $size(($Self).todos)))
+         { 
+           goto $Ret; 
+         };
+      assert (n >= 0);
+      inhale $array_acc(new_array, $tuple3$int$int$c_State, write);
+      inhale ($size(new_array) == n);
+      inhale $array_init(new_array, $tuple3$int$int$c_State,
+              Tup$3(0, 0, TODO()));
+      i := 0;
+      while ((i < $size(($Self).todos)))
+         invariant $Perm($Self)
+         invariant $array_acc(new_array, $tuple3$int$int$c_State, write)
+         invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+         invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+         old(($Self).nextId)))
+         invariant ((0 <= i) && (i <= $size(($Self).todos)))
+         invariant ($size(($Self).todos) < $size(new_array))
+         invariant ($size(($Self).todos) == old($size(($Self).todos)))
+         invariant (forall ii : Int :: (((0 <= ii) && (ii < old($size(
+                                                                 ($Self).todos)))) ==> (
+                    ($loc(($Self).todos, ii)).$tuple3$int$int$c_State == 
+                    old(($loc(($Self).todos, ii)).$tuple3$int$int$c_State))))
+         invariant (forall ii : Int :: (((0 <= ii) && (ii < i)) ==> (
+                    ($loc(($Self).todos, ii)).$tuple3$int$int$c_State == 
+                    ($loc(new_array, ii)).$tuple3$int$int$c_State)))
+         { 
+           ($loc(new_array, i)).$tuple3$int$int$c_State := ($loc(($Self).todos,
+                                                             i)).$tuple3$int$int$c_State;
+           i := (i + 1); 
+         };
+      ($Self).todos := new_array;
+      label $Ret; 
+    }
+method getTodos($Self: Ref)
+     returns ($Res: Array)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $array_acc($Res, $tuple3$int$int$c_State, wildcard)
+    ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+      old(($Self).nextId)))
+    ensures ($size(($Self).todos) == old($size(($Self).todos)))
+    ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> (
+            ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old((
+                                                                    $loc(
+                                                                    ($Self).todos,
+                                                                    i)).$tuple3$int$int$c_State))))
+    ensures $Inv($Self)
+    { var new_array: Array
+      inhale $array_acc(new_array, $tuple3$int$int$c_State, write);
+      inhale ($size(new_array) == 1);
+      ($loc(new_array, 0)).$tuple3$int$int$c_State := Tup$3(0, 0, TODO());
+      exhale $array_acc(new_array, $tuple3$int$int$c_State, wildcard);
+      inhale $array_acc(new_array, $tuple3$int$int$c_State, wildcard);
+      $Res := new_array;
+      goto $Ret;
+      label $Ret; 
+    }
+method getTodo($Self: Ref, id: Int)
+     returns ($Res: Option[Tuple$3[Int, Int, State]])
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+      old(($Self).nextId)))
+    ensures ($size(($Self).todos) == old($size(($Self).todos)))
+    ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> (
+            ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old((
+                                                                    $loc(
+                                                                    ($Self).todos,
+                                                                    i)).$tuple3$int$int$c_State))))
+    ensures ((exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (
+             (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id))) ==> true)
+    ensures $Inv($Self)
+    { var i: Int
+      var res: Option[Tuple$3[Int, Int, State]]
+      i := 0;
+      res := None();
+      while ((i < ($Self).num))
+         invariant $Perm($Self)
+         invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+         invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+         old(($Self).nextId)))
+         invariant ($size(($Self).todos) == old($size(($Self).todos)))
+         invariant (forall ii : Int :: (((0 <= ii) && (ii < old($size(
+                                                                 ($Self).todos)))) ==> (
+                    ($loc(($Self).todos, ii)).$tuple3$int$int$c_State == 
+                    old(($loc(($Self).todos, ii)).$tuple3$int$int$c_State))))
+         invariant ((0 <= i) && (i <= ($Self).num))
+         { 
+           label $lbl$continue$l;
+           if (((($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id))
+              { 
+                res := Some(($loc(($Self).todos, i)).$tuple3$int$int$c_State);
+                goto $lbl$l; 
+              }; 
+         };
+      label $lbl$l;
+      $Res := res;
+      goto $Ret;
+      label $Ret; 
+    }
+method addTodo($Self: Ref, description: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+    ensures (($Self).num == (old(($Self).num) + 1))
+    ensures (($Self).nextId == (old(($Self).nextId) + 1))
+    ensures ($Res == old(($Self).nextId))
+    ensures (($loc(($Self).todos, (($Self).num - 1))).$tuple3$int$int$c_State == 
+      Tup$3($Res, description, TODO()))
+    ensures (forall i : Int :: (((0 <= i) && ((i + 1) < ($Self).num)) ==> (
+            ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old((
+                                                                    $loc(
+                                                                    ($Self).todos,
+                                                                    i)).$tuple3$int$int$c_State))))
+    ensures $Inv($Self)
+    { var id: Int
+      id := ($Self).nextId;
+      if ((($Self).num >= $size(($Self).todos)))
+         { 
+           resize($Self, ((($Self).num * 2) + 1)); 
+         };
+      ($loc(($Self).todos, ($Self).num)).$tuple3$int$int$c_State := 
+         Tup$3(id, description, TODO());
+      ($Self).num := (($Self).num + 1);
+      ($Self).nextId := (($Self).nextId + 1);
+      $Res := id;
+      goto $Ret;
+      label $Ret; 
+    }
+method completeTodo($Self: Ref, id: Int)
+    
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+      old(($Self).nextId)))
+    ensures ($size(($Self).todos) == old($size(($Self).todos)))
+    ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && (
+            (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 != id)) ==> (
+            ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old((
+                                                                    $loc(
+                                                                    ($Self).todos,
+                                                                    i)).$tuple3$int$int$c_State))))
+    ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && (
+            (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id)) ==> (
+            (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2 == 
+            DONE())))
+    ensures $Inv($Self)
+    { var i: Int
+      i := 0;
+      while ((i < ($Self).num))
+         invariant $Perm($Self)
+         invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+         invariant ((0 <= i) && (i <= $size(($Self).todos)))
+         invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+         old(($Self).nextId)))
+         invariant ($size(($Self).todos) == old($size(($Self).todos)))
+         invariant (forall ii : Int :: (((i <= ii) && (ii < $size(($Self).todos))) ==> (
+                    ($loc(($Self).todos, ii)).$tuple3$int$int$c_State == 
+                    old(($loc(($Self).todos, ii)).$tuple3$int$int$c_State))))
+         invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
+                    (($loc(($Self).todos, ii)).$tuple3$int$int$c_State).tup$3$0 != id)) ==> (
+                    ($loc(($Self).todos, ii)).$tuple3$int$int$c_State == 
+                    old(($loc(($Self).todos, ii)).$tuple3$int$int$c_State))))
+         invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
+                    (($loc(($Self).todos, ii)).$tuple3$int$int$c_State).tup$3$0 == id)) ==> (
+                    (($loc(($Self).todos, ii)).$tuple3$int$int$c_State).tup$3$2 == 
+                    DONE())))
+         { 
+           if (true)
+              { var taskId: Int
+                var taskDesc: Int
+                var _completed: State
+                taskId := (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0;
+                taskDesc := (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$1;
+                _completed := (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2;
+                if ((taskId == id))
+                   { 
+                     ($loc(($Self).todos, i)).$tuple3$int$int$c_State := 
+                        Tup$3(taskId, taskDesc, DONE()); 
+                   };
+                i := (i + 1); 
+              }; 
+         };
+      label $Ret; 
+    }
+method showTodos($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+      old(($Self).nextId)))
+    ensures ($size(($Self).todos) == old($size(($Self).todos)))
+    ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
+            ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old((
+                                                                    $loc(
+                                                                    ($Self).todos,
+                                                                    i)).$tuple3$int$int$c_State))))
+    ensures $Inv($Self)
+    { var output: Int
+      var i: Int
+      output := 1;
+      i := 0;
+      while ((i < ($Self).num))
+         invariant $Perm($Self)
+         invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+         invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+         old(($Self).nextId)))
+         invariant ($size(($Self).todos) == old($size(($Self).todos)))
+         invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
+                    ($loc(($Self).todos, ii)).$tuple3$int$int$c_State == 
+                    old(($loc(($Self).todos, ii)).$tuple3$int$int$c_State))))
+         { var todo: Tuple$3[Int, Int, State]
+           todo := ($loc(($Self).todos, i)).$tuple3$int$int$c_State;
+           output := $concat($concat(output, 2), (todo).tup$3$1);
+           if (((todo).tup$3$2).isDONE)
+              { 
+                output := $concat(output, 3); 
+              }else
+              { 
+                if (((todo).tup$3$2).isTODO)
+                   { 
+                     output := $concat(output, 4); 
+                   }; 
+              }; 
+         };
+      $Res := $concat(output, 2);
+      goto $Ret;
+      label $Ret; 
+    }
+method clearCompleted($Self: Ref)
+    
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures (($Self).num <= old(($Self).num))
+    ensures (($Self).nextId == old(($Self).nextId))
+    ensures ($size(($Self).todos) == old($size(($Self).todos)))
+    ensures (forall i : Int :: ((((0 <= i) && (i < old(($Self).num))) && (
+            old((($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2) == 
+            TODO())) ==> (exists k : Int :: (((0 <= k) && (k < $size(
+                                                               ($Self).todos))) && (
+                         ($loc(($Self).todos, k)).$tuple3$int$int$c_State == 
+                         old(($loc(($Self).todos, i)).$tuple3$int$int$c_State))))))
+    ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
+            (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2 == 
+            TODO())))
+    ensures $Inv($Self)
+    { var new_array: Array
+      var i: Int
+      var j: Int
+      assert ($size(($Self).todos) >= 0);
+      inhale $array_acc(new_array, $tuple3$int$int$c_State, write);
+      inhale ($size(new_array) == $size(($Self).todos));
+      inhale $array_init(new_array, $tuple3$int$int$c_State,
+              Tup$3(0, 0, TODO()));
+      i := 0;
+      j := 0;
+      while ((i < ($Self).num))
+         invariant $Perm($Self)
+         invariant $array_acc(new_array, $tuple3$int$int$c_State, write)
+         invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
+         invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == 
+         old(($Self).nextId)))
+         invariant ($size(($Self).todos) == old($size(($Self).todos)))
+         invariant (forall ii : Int :: (((0 <= ii) && (ii < old($size(
+                                                                 ($Self).todos)))) ==> (
+                    ($loc(($Self).todos, ii)).$tuple3$int$int$c_State == 
+                    old(($loc(($Self).todos, ii)).$tuple3$int$int$c_State))))
+         invariant (($Self).num <= $size(new_array))
+         invariant ((0 <= i) && (i <= ($Self).num))
+         invariant (j <= i)
+         invariant ((0 <= j) && (j <= ($Self).num))
+         invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
+                    (($loc(($Self).todos, ii)).$tuple3$int$int$c_State).tup$3$2 == 
+                    TODO())) ==> (exists k : Int :: (((0 <= k) && (k < j)) && (
+                                 ($loc(new_array, k)).$tuple3$int$int$c_State == 
+                                 ($loc(($Self).todos, ii)).$tuple3$int$int$c_State)))))
+         invariant (forall ii : Int :: (((0 <= ii) && (ii < j)) ==> (
+                    (($loc(new_array, ii)).$tuple3$int$int$c_State).tup$3$2 == 
+                    TODO())))
+         { 
+           if (((($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2 == 
+              TODO()))
+              { 
+                ($loc(new_array, j)).$tuple3$int$int$c_State := ($loc(
+                                                                  ($Self).todos,
+                                                                  i)).$tuple3$int$int$c_State;
+                j := (j + 1); 
+              };
+           i := (i + 1); 
+         };
+      ($Self).todos := new_array;
+      ($Self).num := j;
+      label $Ret; 
+    }
diff --git a/test/viper/todo_tuple.mo b/test/viper/todo_tuple.mo
index 6e0776af6fa..805aba95757 100644
--- a/test/viper/todo_tuple.mo
+++ b/test/viper/todo_tuple.mo
@@ -1,10 +1,13 @@
+// @verify
+
 import Prim "mo:⛔";
 import Array "mo:base/Array";
 
 actor Assistant {
-  // type ToDo = (Nat, Text, Bool); // (id, desc, completed)
+  // type ToDo = (Nat, Text, State); // (id, desc, completed)
+  public type State = { #TODO; #DONE };
   
-  var todos : [var (Nat, Text, Bool)] = [var ];
+  var todos : [var (Nat, Text, State)] = [var ];
   var num : Nat = 0;
   var nextId : Nat = 1;
 
@@ -23,7 +26,7 @@ actor Assistant {
       (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
     if (n <= todos.size())
       return;
-    let new_array = Array.init<(Nat, Text, Bool)>(n, (0, "", false));
+    let new_array = Array.init<(Nat, Text, State)>(n, (0, "", #TODO));
     var i: Nat = 0;
     while (i < todos.size()) {
       // actor invariant:
@@ -44,21 +47,21 @@ actor Assistant {
     todos := new_array;
   };
 
-  public query func getTodos() : async [(Nat, Text, Bool)] {
+  public query func getTodos() : async [(Nat, Text, State)] {
     assert:return num == (old(num)) and nextId == (old(nextId));
     assert:return todos.size() == (old(todos.size()));
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
-    // BUG: var:return here have type Bool
+    // BUG: var:return here have type State
     // assert:return Prim.forall<Nat>(func i {
     //   0 <= i and i < (old(todos.size())) implies todos[i] == (var:return)[i])});
     // TODO: is not supported yet, do it manually (as in reverse.mo)
-    // let new_array = Array.tabulate<(Nat, Text, Bool)>(num, func i = todos[i]);
-    let new_array = [(0, "", false)];
+    // let new_array = Array.tabulate<(Nat, Text, State)>(num, func i = todos[i]);
+    let new_array : [(Nat, Text, State)] = [(0, "", #TODO)];
     return new_array;
   };
 
-  public query func getTodo(id : Nat): async (Nat, Text, Bool) {
+  public query func getTodo(id : Nat): async ?(Nat, Text, State) {
     assert:return num == (old(num)) and nextId == (old(nextId));
     assert:return todos.size() == (old(todos.size()));
     assert:return Prim.forall<Nat>(func i =
@@ -68,8 +71,8 @@ actor Assistant {
                    // BUG: problem with type of the (var:return)
                    true); // Prim.exists<Nat>(func i = (0 <= i and i < num and todos[i] == (var:return))));
     var i : Nat = 0;
-    // TODO: try to use contine & break
-    while (i < num) {
+    var res : ?(Nat, Text, State) = null;
+    label l while (i < num) {
       // actor invariant:
       assert:loop:invariant 0 <= num and num <= todos.size();
       // fields unchanged:
@@ -80,11 +83,11 @@ actor Assistant {
         (0 <= ii and ii < (old(todos.size())) implies todos[ii] == (old(todos[ii]))));
       assert:loop:invariant 0 <= i and i <= num;
       if (todos[i].0 == id) {
-        return todos[i];
-      }
+        res := ?todos[i];
+        break l;
+      };
     };
-    // TODO: return option
-    return (0, "", false);
+    return res;
   };
 
   // Returns the ID that was given to the ToDo item
@@ -93,14 +96,14 @@ actor Assistant {
     assert:return num == (old(num)) + 1;
     assert:return nextId == (old(nextId)) + 1;
     assert:return (var:return) == (old(nextId));
-    assert:return todos[num-1] == (var:return, description, false);
+    assert:return todos[num-1] == (var:return, description, #TODO);
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i+1 < num implies todos[i] == (old(todos[i]))));
     let id = nextId;
     if (num >= todos.size()) {
       resize(num * 2+1);
     };
-    todos[num] := (id, description, false);
+    todos[num] := (id, description, #TODO);
     num += 1;
     nextId += 1;
     return id;
@@ -112,7 +115,7 @@ actor Assistant {
     assert:return Prim.forall<Nat>(func i =
       ((0 <= i and i < num and todos[i].0 != id) implies todos[i] == (old(todos[i])) ));
     assert:return Prim.forall<Nat>(func i =
-      ((0 <= i and i < num and todos[i].0 == id) implies todos[i].2 == true ));
+      ((0 <= i and i < num and todos[i].0 == id) implies todos[i].2 == #DONE ));
     var i : Nat = 0;
     while (i < num) {
       // actor invariant
@@ -127,12 +130,12 @@ actor Assistant {
       assert:loop:invariant Prim.forall<Nat>(func ii =
         (0 <= ii and ii < i and todos[ii].0 != id implies todos[ii] == (old(todos[ii]))));
       assert:loop:invariant Prim.forall<Nat>(func ii =
-        (0 <= ii and ii < i and todos[ii].0 == id implies todos[ii].2 == true));
+        (0 <= ii and ii < i and todos[ii].0 == id implies todos[ii].2 == #DONE));
       // let (taskId, taskDesc, _) = todos[i]; // TODO: requires recursive patterns
       switch (todos[i]) {
-        case(taskId, taskDesc, /* _ */_completed) {
+        case(taskId, taskDesc, /* _ */_completed: State) {
           if (taskId == id) {
-            todos[i] := (taskId, taskDesc, true);
+            todos[i] := (taskId, taskDesc, #DONE);
           };
           i += 1;
         };
@@ -156,9 +159,12 @@ actor Assistant {
       // NOTE: translation is not handling shadowing here, so `func i` causes an error here
       assert:loop:invariant Prim.forall<Nat>(func ii =
         ((0 <= ii and ii < num) implies todos[ii] == (old(todos[ii])) ));
-      let todo: (Nat, Text, Bool) = todos[i];
+      let todo: (Nat, Text, State) = todos[i];
       output := output # "\n" # todo.1;
-      if (todo.2) { output := output # " ✔"; };
+      switch (todo.2) {
+       case (#DONE) { output := output # " ✔"; };
+       case (#TODO) { output := output # " ❌"; };
+      }
     };
     return output # "\n";
   };
@@ -168,12 +174,12 @@ actor Assistant {
     assert:return nextId == (old(nextId));
     assert:return todos.size() == (old(todos.size()));
     assert:return Prim.forall<Nat>(func i =
-      (0 <= i and i < (old(num)) and (old(todos[i].2)) == false
+      (0 <= i and i < (old(num)) and (old(todos[i].2)) == #TODO
       implies Prim.exists<Nat> (func k =
             ( 0 <= k and k < todos.size() and todos[k] == (old(todos[i])) )) ));
     assert:return Prim.forall<Nat>(func i =
-      (0 <= i and i < num implies todos[i].2 == false));
-    let new_array = Array.init<(Nat, Text, Bool)>(todos.size(), (0, "", false));
+      (0 <= i and i < num implies todos[i].2 == #TODO));
+    let new_array = Array.init<(Nat, Text, State)>(todos.size(), (0, "", #TODO));
     var i: Nat = 0;
     var j: Nat = 0;
     while (i < num) {
@@ -190,12 +196,12 @@ actor Assistant {
       assert:loop:invariant j <= i;
       assert:loop:invariant 0 <= j and j <= num;
       assert:loop:invariant Prim.forall<Nat>(func ii =
-        (0 <= ii and ii < i and todos[ii].2 == false
+        (0 <= ii and ii < i and todos[ii].2 == #TODO
          implies Prim.exists<Nat>(func k =
                   (0 <= k and k < j and new_array[k] == todos[ii] ))));
       assert:loop:invariant Prim.forall<Nat>(func ii =
-        (0 <= ii and ii < j implies new_array[ii].2 == false ));
-      if (todos[i].2 == false) {
+        (0 <= ii and ii < j implies new_array[ii].2 == #TODO ));
+      if (todos[i].2 == #TODO) {
         new_array[j] := todos[i];
         j += 1;
       };