1 files changed, 12 insertions, 0 deletions
diff --git a/Test/dafny0/Include.dfy b/Test/dafny0/Include.dfy
new file mode 100644
index 00000000..a228194f
--- /dev/null
+++ b/Test/dafny0/Include.dfy
@@ -0,0 +1,12 @@
+
+include "Includee.dfy"
+
+method test_include(z:int)
+{
+  // Make sure we can still see function bodies
+  assert forall y :: f(y) == 2*y;
+
+  // Use an unverified method
+  var w := m_unproven(z);
+  assert w == 2*z;
+}