From 80fbe74f7cc472c733a85a90f774182d0d0a8964 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 26 Jan 2012 13:05:50 -0800 Subject: Dafny: fixed bug in compilation of let expressions. --- Test/dafny1/Rippling.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test') diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 677e6e70..8bed7545 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -303,7 +303,7 @@ ghost method P1() } ghost method P2() - ensures forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys))); + ensures forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, concat(xs, ys)); { } -- cgit v1.2.3