Add test for issue #2726

dafny-lang · Nov 1, 2022 · cc2fb2e · cc2fb2e
1 parent f4bac32
commit cc2fb2e
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/Test/git-issues/git-issue-2726.dfy b/Test/git-issues/git-issue-2726.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny_0 /compile:1 /compileTarget:cs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Formula =
+  | And(left: Formula, right: Formula)
+  | Not(underlying: Formula)
+  | True
+{
+  function method size(): nat {
+    match this
+    case And(l, r) => l.size() + r.size()
+    case Not(u) => u.size() + 1
+    case True => 1
+  }
+}
diff --git a/Test/git-issues/git-issue-2726.dfy.expect b/Test/git-issues/git-issue-2726.dfy.expect