spare __init__ from the precondition

dfinity · Oct 15, 2022 · ed66529 · ed66529
1 parent 8bb8858
commit ed66529
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -39,7 +39,10 @@ let rec extract_invariants : item list -> (par -> invariants -> invariants) = fu
 let rec adorn_invariants (is : par -> invariants -> invariants) = function
   | [] -> []
   | { it = MethodI (d, (self :: _ as i), o, r, e, b); _ } as m :: p ->
-    let m = { m with it = MethodI (d, i, o, is self r, is self e, b) } in
+    let pre_is = function
+      | "__init__" -> fun _ l -> l
+      | _ -> is in
+    let m = { m with it = MethodI (d, i, o, pre_is d.it self r, is self e, b) } in
     m :: adorn_invariants is p
   | i :: p -> i :: adorn_invariants is p