From 660c22dc282ee371fdbd4c97e9289ee016a4aca8 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 6 Nov 2009 22:00:56 +0000
Subject: Redesigned the encoding of Dafny generics, including the built-in
 types set and seq.

Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).

Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.

Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.

Added a space in the pretty printing of Boogie coercion expressions.
---
 Source/Core/AbsyExpr.ssc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/Core/AbsyExpr.ssc')

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index 78a796c2..c07db23b 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -1527,7 +1527,7 @@ namespace Microsoft.Boogie
         stream.Write("(");
 
       ((!)args[0]).Emit(stream, opBindingStrength, false);
-      stream.Write(FunctionName);
+      stream.Write("{0} ", FunctionName);
       Type.Emit(stream, 0);
 
       if (parensNeeded) 
-- 
cgit v1.2.3