Skip to content
Snippets Groups Projects
Unverified Commit 92654857 authored by Thibaut Benjamin's avatar Thibaut Benjamin
Browse files

[e-acsl] bugfix: unguarded quantifications

parent 8330d9d6
No related branches found
No related tags found
No related merge requests found
......@@ -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 =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment