diff --git a/src/expr/e_levels.ml b/src/expr/e_levels.ml
index bb9e3db8..97dd69ae 100644
--- a/src/expr/e_levels.ml
+++ b/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
diff --git a/test/bugs/quant_level_test.tla b/test/bugs/quant_level_test.tla
new file mode 100644
index 00000000..f94f7053
--- /dev/null
+++ b/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