From 854acf0f7f5aa105500c6d0ee0fcf0d4c918a81e Mon Sep 17 00:00:00 2001 From: qunyanm Date: Sat, 14 Nov 2015 14:50:26 -0800 Subject: Fix issue 94. Allow tuple-based assignment in statement contexts. --- Test/dafny4/Bug94.dfy | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 Test/dafny4/Bug94.dfy (limited to 'Test/dafny4/Bug94.dfy') diff --git a/Test/dafny4/Bug94.dfy b/Test/dafny4/Bug94.dfy new file mode 100644 index 00000000..2f437785 --- /dev/null +++ b/Test/dafny4/Bug94.dfy @@ -0,0 +1,35 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function foo() : (int, int) +{ + (5, 10) +} + +function bar() : int +{ + var (x, y) := foo(); + x + y +} + +lemma test() +{ + var (x, y) := foo(); +} + +function method foo2() : (int,int) +{ + (5, 10) +} + +method test2() +{ + var (x, y) := foo2(); +} + +method Main() +{ + var (x, y) := foo2(); + assert (x+y == 15); + print(x+y); +} -- cgit v1.2.3