diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok index 4c2cc845438..85045179432 100644 --- 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