diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml index f6fa2398373722c71c9d19af4976ec3348bebe63..447a396a39957c009b90080dca5222f5c92117a4 100644 --- a/src/plugins/e-acsl/src/analyses/bound_variables.ml +++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml @@ -684,8 +684,14 @@ end compute_guards loc ~is_forall:true p bound_vars goal | Pexists(bound_vars, ({ pred_content = Pand(_, _) } as goal)) -> compute_guards loc ~is_forall:false p bound_vars goal - | Pforall _ -> Error.not_yet "unguarded \\forall quantification" - | Pexists _ -> Error.not_yet "unguarded \\exists quantification" + | Pforall _ -> + Quantifier.add + p + (Err (Error.Not_yet "unguarded \\forall quantification")) + | Pexists _ -> + Quantifier.add + p + (Err (Error.Not_yet "unguarded \\exists quantification")) | _ -> () let gannot a =