Commit e4340f82 authored by David Hauzar's avatar David Hauzar
Browse files

Displaying a counterexample in IDE before interleaving it with code.

parent 8a46fa14
...@@ -643,10 +643,13 @@ let update_tabs a = ...@@ -643,10 +643,13 @@ let update_tabs a =
match a.S.proof_state with match a.S.proof_state with
| S.Done r -> | S.Done r ->
if not (Model_parser.is_model_empty r.Call_provers.pr_model) then begin if not (Model_parser.is_model_empty r.Call_provers.pr_model) then begin
Model_parser.interleave_with_source "Counterexample:\n" ^
r.Call_provers.pr_model (Model_parser.model_to_string r.Call_provers.pr_model) ^
~filename:!current_file "\n\nSource code interleaved with counterexample:" ^
~source_code:(Sysutil.file_contents !current_file) (Model_parser.interleave_with_source
r.Call_provers.pr_model
~filename:!current_file
~source_code:(Sysutil.file_contents !current_file))
end else end 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