Commit 071a1394 authored by Martin Clochard's avatar Martin Clochard

bugfix: simplify_trivial_quantification used equalities under match branches

The following could be proved correct:

type t = A | B
function f (x:'a) : 'a = x
predicate top = A = f A
lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end
lemma fail : false
parent 98a436ee
......@@ -79,13 +79,8 @@ let rec fmla_find_subst boundvars var sign f =
let vs,f' = t_open_bound fb in
let boundvars = Svs.add vs boundvars in
fmla_find_subst boundvars var sign f'
| Tcase (_,fbs) ->
let iter_fb fb =
let patl,f = t_open_branch fb in
let boundvars = patl.pat_vars in
fmla_find_subst boundvars var sign f in
List.iter iter_fb fbs
| Tbinop (_, _, _) | Tif ( _, _, _) | Tapp _ | Tfalse | Ttrue-> ()
| Tbinop (_, _, _) | Tif ( _, _, _) | Tcase (_, _)
| Tapp _ | Tfalse | Ttrue -> ()
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
let rec fmla_quant sign f = function
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment