Commit bbda54f1 authored by Sylvain Dailler's avatar Sylvain Dailler

Avoid some generation of *_vc_constant

parent 01980e91
......@@ -88,6 +88,13 @@ module Hprid = Exthtbl.Make (struct
let hash p = Exthtbl.hash p
end)
let same_line_loc loc1 loc2 =
match loc1, loc2 with
| Some loc1, Some loc2 ->
let (f1, l1, _, _) = Loc.get loc1 in
let (f2, l2, _, _) = Loc.get loc2 in
f1 = f2 && l1 = l2
| _ -> false
(* Used to generate duplicate vc_constant and axioms for counterex generation.
This function is always called when the term is in negative position or
......@@ -117,7 +124,9 @@ let rec do_intro info vc_loc vc_map vc_var t =
should be in counterexample, introduce new constant in location
loc with all labels necessary for collecting it for counterexample
and make it equal to the variable *)
if Ident.has_a_model_label ls then
if Ident.has_a_model_label ls &&
not (same_line_loc info.vc_loc ls.id_loc)
then
let const_label = if info.vc_pre_or_post then
model_trace_for_postcondition ~labels:ls.id_label
else
......
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