Commit 316f02ad authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fixed bug #13445

parent 573a4b75
module T
let test () =
let a,b,c,d = (1,2,3,4) in ()
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/tuples"
End:
*)
......@@ -719,11 +719,17 @@ let add_wp_decl ps f uc =
let id = id_fresh ~label ?loc:name.id_loc s in
let pr = create_prsymbol id in
(* prepare the VC formula *)
let km = get_known (pure_uc uc) in
let f = remove_at f in
let f = bool_to_prop uc f in
let f = eval_match ~inline:inline_nonrec_linear km f in
let f = unabsurd f in
(* get a known map with tuples added *)
let km =
let d = create_prop_decl Pgoal pr f in
let uc = add_pure_decl d uc in
get_known (pure_uc uc)
in
(* simplify f *)
let f = eval_match ~inline:inline_nonrec_linear km f in
(* printf "wp: f=%a@." print_term f; *)
let d = create_prop_decl Pgoal pr f in
add_pure_decl d uc
......
(*
module ExcepAndRec
use import int.Int
......@@ -13,6 +15,7 @@ let rec f (x:int) : int =
end
end
*)
(*
module Test
......
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