Levels of the quantifier bounds were effectively ignored. (#189)

Signed-off-by: Karolis Petrauskas <[email protected]>

src/expr/e_levels.ml

@@ -196,7 +196,8 @@ class virtual ['s] level_computation = object (self : 'self)
                         (v, k, No_domain)
                     end
                 in
-                (List.map f bs, !bs_levels, !level_args_sets) in
+                let fbs = List.map f bs in (* has to be executed before reading refs. *)
+                (fbs, !bs_levels, !level_args_sets) in
             let doms_level = List.fold_left max 0 bs_levels in
             let level_args = List.fold_left
                 StringSet.union StringSet.empty level_args_sets in

test/bugs/quant_level_test.tla

@@ -0,0 +1,11 @@
+---- MODULE quant_level_test ----
+(*
+The levels of quantifier bounds were ignored.
+That lead to considering formulas as being constant level
+leading to proofs passing were they must fail.
+*)
+VARIABLE v
+I == \A y \in v: y = y
+LEMMA ASSUME I PROVE I' OBVIOUS
+====
+stderr: status:failed