diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml
index 158a71fb7f6..99f038b56a9 100644
--- a/src/viper/prelude.ml
+++ b/src/viper/prelude.ml
@@ -17,10 +17,19 @@ 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 */|prelude}
diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok
index 729e8d3f00d..dc4206b8f7d 100644
--- a/test/viper/ok/array.silicon.ok
+++ b/test/viper/ok/array.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@46.1)
diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
index 910777ccb86..896ea80fbb2 100644
--- a/test/viper/ok/array.vpr.ok
+++ b/test/viper/ok/array.vpr.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 */
 
 define $Perm($Self) (((((true && (acc(($Self).immut_arr,write) && ($array_acc(
diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok
index 4fc0e3b8c7b..1c0878ce6a6 100644
--- a/test/viper/ok/assertions.silicon.ok
+++ b/test/viper/ok/assertions.silicon.ok
@@ -1,2 +1,2 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@37.13--37.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@55.15--55.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@46.13--46.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@64.15--64.44)
diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok
index 63cc15e2232..6a7b6e32dd7 100644
--- a/test/viper/ok/assertions.vpr.ok
+++ b/test/viper/ok/assertions.vpr.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
diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok
index 421761c48d4..71cd3dc5691 100644
--- a/test/viper/ok/async.silicon.ok
+++ b/test/viper/ok/async.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@60.15--60.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@69.15--69.42)
diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok
index 1754bb9244b..d37cd8572fe 100644
--- a/test/viper/ok/async.vpr.ok
+++ b/test/viper/ok/async.vpr.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_4: Int
diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok
index efee6cfcdb5..63db8799253 100644
--- a/test/viper/ok/claim-broken.silicon.ok
+++ b/test/viper/ok/claim-broken.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@58.20--58.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@67.20--67.47)
diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok
index aa58fedc049..b0d7564b48d 100644
--- a/test/viper/ok/claim-broken.vpr.ok
+++ b/test/viper/ok/claim-broken.vpr.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
diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok
index 707a17b923d..af0d648480e 100644
--- a/test/viper/ok/claim-reward-naive.vpr.ok
+++ b/test/viper/ok/claim-reward-naive.vpr.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 */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok
index 3faf76cbba3..de2d22407eb 100644
--- a/test/viper/ok/claim-simple.silicon.ok
+++ b/test/viper/ok/claim-simple.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@38.1)
diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok
index c55c22dc519..808b33b356e 100644
--- a/test/viper/ok/claim-simple.vpr.ok
+++ b/test/viper/ok/claim-simple.vpr.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 */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok
index 9d57c8f8505..f8679a31150 100644
--- a/test/viper/ok/claim.vpr.ok
+++ b/test/viper/ok/claim.vpr.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
diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok
index 82c5fbf11d0..bd240ee0e3d 100644
--- a/test/viper/ok/counter.silicon.ok
+++ b/test/viper/ok/counter.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@38.1)
diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok
index 48ae7c4a0dd..4a7b83bf366 100644
--- a/test/viper/ok/counter.vpr.ok
+++ b/test/viper/ok/counter.vpr.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 */
 
 define $Perm($Self) ((true && acc(($Self).count,write)))
diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok
index a69c5f71f1a..7638af33db4 100644
--- a/test/viper/ok/invariant.silicon.ok
+++ b/test/viper/ok/invariant.silicon.ok
@@ -1 +1 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@34.13--34.24)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@43.13--43.24)
diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
index e4c323fdde0..1a5769b06a0 100644
--- a/test/viper/ok/invariant.vpr.ok
+++ b/test/viper/ok/invariant.vpr.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 */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok
index 441ccbbcb46..3dba2b49c20 100644
--- a/test/viper/ok/loop-invariant.silicon.ok
+++ b/test/viper/ok/loop-invariant.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@28.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@29.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@38.1)
diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
index 22ac3a0c146..2cd1e593141 100644
--- a/test/viper/ok/loop-invariant.vpr.ok
+++ b/test/viper/ok/loop-invariant.vpr.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 */
 
 define $Perm($Self) (true)
diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok
index 075d66b154a..7d42acbf433 100644
--- a/test/viper/ok/method-call.silicon.ok
+++ b/test/viper/ok/method-call.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@38.1)
diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok
index a53076986f4..a321d1a1a45 100644
--- a/test/viper/ok/method-call.vpr.ok
+++ b/test/viper/ok/method-call.vpr.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 */
 
 define $Perm($Self) ((true && acc(($Self).boolFld,write)))
diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok
index 910430540d9..ab81ca6c18c 100644
--- a/test/viper/ok/nats.silicon.ok
+++ b/test/viper/ok/nats.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@38.1)
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
index b23ce4f2b4d..42ad155e097 100644
--- a/test/viper/ok/nats.vpr.ok
+++ b/test/viper/ok/nats.vpr.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 */
 
 define $Perm($Self) ((true && acc(($Self).x,write)))
diff --git a/test/viper/ok/polymono.silicon.ok b/test/viper/ok/polymono.silicon.ok
index fe4dbcfdf0e..824ad659969 100644
--- a/test/viper/ok/polymono.silicon.ok
+++ b/test/viper/ok/polymono.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@28.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@29.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@38.1)
diff --git a/test/viper/ok/polymono.vpr.ok b/test/viper/ok/polymono.vpr.ok
index aa51e879610..f8f7c025cda 100644
--- a/test/viper/ok/polymono.vpr.ok
+++ b/test/viper/ok/polymono.vpr.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 */
 
 define $Perm($Self) (true)
diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok
index cea5c33665c..76a62e08c36 100644
--- a/test/viper/ok/private.vpr.ok
+++ b/test/viper/ok/private.vpr.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 */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
diff --git a/test/viper/ok/reverse.silicon.ok b/test/viper/ok/reverse.silicon.ok
index b1031edd0c9..df06cca5ed2 100644
--- a/test/viper/ok/reverse.silicon.ok
+++ b/test/viper/ok/reverse.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@32.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@41.1)
diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok
index cad19d63a02..155ddca2b60 100644
--- a/test/viper/ok/reverse.vpr.ok
+++ b/test/viper/ok/reverse.vpr.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 */
 
 define $Perm($Self) ((true && (acc(($Self).xarray,write) && ($array_acc(
diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok
index 6535224ff32..3b186feb918 100644
--- a/test/viper/ok/simple-funs.silicon.ok
+++ b/test/viper/ok/simple-funs.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@28.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@29.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@38.1)
diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok
index 8ed1c3df6fc..2cfd17e7002 100644
--- a/test/viper/ok/simple-funs.vpr.ok
+++ b/test/viper/ok/simple-funs.vpr.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 */
 
 define $Perm($Self) (true)
diff --git a/test/viper/ok/tuple.silicon.ok b/test/viper/ok/tuple.silicon.ok
index d337fec8563..cf1fccc4738 100644
--- a/test/viper/ok/tuple.silicon.ok
+++ b/test/viper/ok/tuple.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (tuple.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (tuple.vpr@42.1)
diff --git a/test/viper/ok/tuple.vpr.ok b/test/viper/ok/tuple.vpr.ok
index 175ed493e3e..d857252c085 100644
--- a/test/viper/ok/tuple.vpr.ok
+++ b/test/viper/ok/tuple.vpr.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 */
 
 define $Perm($Self) (((true && (acc(($Self).fld1,write) && (acc(($prj(
diff --git a/test/viper/ok/variants.silicon.ok b/test/viper/ok/variants.silicon.ok
index 59551735932..d2588c5c13f 100644
--- a/test/viper/ok/variants.silicon.ok
+++ b/test/viper/ok/variants.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (variants.vpr@28.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (variants.vpr@29.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (variants.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (variants.vpr@38.1)
diff --git a/test/viper/ok/variants.vpr.ok b/test/viper/ok/variants.vpr.ok
index 9d99ec20647..2effe918be4 100644
--- a/test/viper/ok/variants.vpr.ok
+++ b/test/viper/ok/variants.vpr.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 */
 
 define $Perm($Self) (true)