Commit 4fe1dfde authored by MARCHE Claude's avatar MARCHE Claude

add test for bug #20610

parent 249ec851
module M
use import bool.Bool
use import option.Option
exception A
let rec foo (x: option bool) : unit
diverges
raises { A -> true }
=
match x with
| None -> ()
| Some b ->
if b then
(
let rec aux (x: unit) : unit
diverges
raises { A -> true }
=
foo (Some false)
in
aux ()
)
else
raise A
end
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
</why3session>
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