diff --git a/examples/acasxu/property_5_aimos.why b/examples/acasxu/property_5_aimos.why
index e653e16cd1245844e081e185679e6371d8987beb..d0ca6f9a0f7594c5132630e96c65d5a3c5945439 100644
--- a/examples/acasxu/property_5_aimos.why
+++ b/examples/acasxu/property_5_aimos.why
@@ -3,6 +3,7 @@ theory ACASXU_P5
   use ieee_float.Float64
   use caisar.DatasetClassification
   use caisar.DatasetClassificationProps
+  use option.Option
 
-  goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
+  goal G: meta_robust model dataset (1.0:t) "reluplex_rotation" "config/custom_transformations.py" "classif_min" None
 end