Commit eea10a7d authored by David Hauzar's avatar David Hauzar

Not reporting error of missing location of the term that triggers VC if

the counter-example is empty while printing part of the counter-example
related to the term that triggers VC.
parent 9dcb1b22
......@@ -224,13 +224,14 @@ let print_model_vc_term
?(sep = "\n")
fmt
model =
match model.vc_term_loc with
| None -> fprintf fmt "error: cannot get location of the check"
| Some pos ->
let (filename, line_number, _, _) = Loc.get pos in
let model_file = get_model_file model.model_files filename in
let model_elements = get_elements model_file line_number in
print_model_elements ~sep me_name_trans fmt model_elements
if not (is_model_empty model) then
match model.vc_term_loc with
| None -> fprintf fmt "error: cannot get location of the check"
| Some pos ->
let (filename, line_number, _, _) = Loc.get pos in
let model_file = get_model_file model.model_files filename in
let model_elements = get_elements model_file line_number in
print_model_elements ~sep me_name_trans fmt model_elements
let model_vc_term_to_string
?(me_name_trans = why_name_trans)
......
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