Commit c960373a authored by David Hauzar's avatar David Hauzar

Bugfix: counter-example model is showed in why3ide if it is not empty.

parent 45892471
......@@ -642,7 +642,7 @@ let update_tabs a =
begin
match a.S.proof_state with
| S.Done r ->
if 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
r.Call_provers.pr_model
~filename:!current_file
......
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