From c960373ae75a66b8f1c1e081eeec3bbbe1375b0c Mon Sep 17 00:00:00 2001
From: David Hauzar <david.hauzar@inria.fr>
Date: Sun, 26 Jul 2015 15:38:53 +0200
Subject: [PATCH] Bugfix: counter-example model is showed in why3ide if it is
not empty.
---
src/ide/gmain.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml
index 8a593e6efa..c8e2fc7b49 100644
--- a/src/ide/gmain.ml
+++ b/src/ide/gmain.ml
@@ -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
--
GitLab