added failing test to show issue with printing ghost expressions in

methods
dafny-lang · Jul 12, 2016 · 021226d · 021226d
1 parent 016dd09
commit 021226d
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/Test/dafny0/GhostPrint.dfy b/Test/dafny0/GhostPrint.dfy
@@ -0,0 +1,13 @@
+//XFAIL: *
+//RUN: %dafny /dafnyVerify:0 /compile:0 /env:0 /dprint:"%t.dfy" "%s"
+//RUN: %dafny /dafnyVerify:0 /compile:0 /env:0 "%t.dfy" > "%t.output"
+//RUN: %diff "%s.expect" "%t.output"
+
+method M() {
+  ghost var h := var ta := F(); 5;
+  var j := ghost var tb := F(); 5;
+  assert h == j;
+}
+
+function F(): int { 5 }
+
diff --git a/Test/dafny0/GhostPrint.dfy.expect b/Test/dafny0/GhostPrint.dfy.expect