From d7f6b848d4290d5d2ca7fa247bfbe13696cbb581 Mon Sep 17 00:00:00 2001
From: Jean-Christophe <Jean-Christophe.Filliatre@lri.fr>
Date: Sat, 21 Jul 2012 01:00:36 +0200
Subject: [PATCH] no need for these ghost
---
examples/programs/distance.mlw | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/examples/programs/distance.mlw b/examples/programs/distance.mlw
index ba840f36b5..5bce4ae665 100644
--- a/examples/programs/distance.mlw
+++ b/examples/programs/distance.mlw
@@ -64,10 +64,10 @@ module Distance
f i <= !j < i /\ !count + d[!j] <= i-1 /\
(forall k: int. !j < k < i -> d[!j] < d[k]) }
variant { !j }
- ghost incr count;
+ incr count;
j := g[!j]
done;
- ghost d[i] <- 1 + d[!j];
+ d[i] <- 1 + d[!j];
g[i] <- !j
done;
assert { !count < n }; (* O(n) is thus ensured *)
--
GitLab