motoko-san: propagate viper tests

serokell · May 21, 2024 · 09f926d · 09f926d
1 parent 65439db
commit 09f926d
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 field $message_async: Int