diff --git a/defs.h b/defs.h
index 9762473..0675af1 100644
--- a/defs.h
+++ b/defs.h
@@ -298,6 +298,13 @@ predicate void ByteV (pointer virt, u8 the_value)
   return;
 }
 
+// predicate (u8) NewByteV (pointer virt)
+// {
+//   take B = Owned<char>(virt);
+//   // assert (B == the_value);
+//   return B;
+// }
+
 predicate void Page (pointer vbase, boolean guard, u8 order)
 {
   if (!guard) {
@@ -308,7 +315,7 @@ predicate void Page (pointer vbase, boolean guard, u8 order)
     let vbaseI = (u64) vbase;
     // FULM_OPT
     take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length)))
-         {Byte(array_shift<char>(NULL, i))};
+         {Block(array_shift<char>(NULL, i))};
     return;
   }
 }
@@ -323,7 +330,9 @@ predicate void ZeroPage (pointer vbase, boolean guard, u8 order)
     let vbaseI = ((u64) vbase);
     // FULM_OPT
     take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length)))
-         {ByteV(array_shift<char>(NULL, i), 0u8)};
+         {RW(array_shift<char>(NULL, i))};
+    assert (each (u64 i; (vbaseI <= i) && (i < (vbaseI + length)))
+         {Bytes[i] == 0u8});
     return;
   }
 }
@@ -335,7 +344,9 @@ predicate void AllocatorPageZeroPart (pointer zero_start, u8 order)
   let length = region_length - sizeof<struct list_head>;
   // FULM_OPT
   take Bytes = each (u64 i; (start <= i) && (i < (start + length)))
-       {ByteV(array_shift<char>(NULL, i), 0u8)};
+       {RW(array_shift<char>(NULL, i))};
+  assert (each (u64 i; (start <= i) && (i < (start + length)))
+      {Bytes[i] == 0u8});
   return;
 }
 
diff --git a/run.sh b/run.sh
index 4b122e1..dbc3efd 100755
--- a/run.sh
+++ b/run.sh
@@ -10,5 +10,8 @@ $CC -g -c -O0 -std=gnu11 -I$OPAM_SWITCH_PREFIX/lib/cn/runtime/include build/driv
 echo "Linking..."
 $CC driver.pp.exec.o $OPAM_SWITCH_PREFIX/lib/cn/runtime/libcn_exec.a -L $OPAM_SWITCH_PREFIX/lib/cn/runtime -lcn_exec -o driver.exe
 echo "Running..."
-./driver.exe
+for i in $(seq 1 10);
+do
+    gtime -f ~%e~%M ./driver.exe
+done
 echo "Done!"