diff options
| author |  qunyanm <unknown> | 2015-04-24 13:03:39 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-24 13:03:39 -0700 |
| commit | e4f315cdf92340332ffddeb164ccb10eb73c4e85 (patch) | |
| tree | 847d56108a3bfff879eb2dec69344dfa951db615 /Test/dafny4 | |
| parent | 688f9daef70041641ea61f2c34a25878d762b75a (diff) | |
Fix issue #72. Add the constructor questionmark to a function's axiom if the
function has a MemberSelectExpr that accesses a type with only one constructor.
Diffstat (limited to 'Test/dafny4')
| -rw-r--r-- | Test/dafny4/Bug72.dfy | 22 | ||||
| -rw-r--r-- | Test/dafny4/bug72.dfy.expect | 2 |
2 files changed, 24 insertions, 0 deletions
diff --git a/Test/dafny4/Bug72.dfy b/Test/dafny4/Bug72.dfy new file mode 100644 index 00000000..829c82e0 --- /dev/null +++ b/Test/dafny4/Bug72.dfy @@ -0,0 +1,22 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Ballot = Ballot(seqno:int)
+
+predicate BalLt(ba:Ballot, bb:Ballot)
+{
+ ba.seqno < bb.seqno
+}
+
+lemma Cases()
+{
+ var b1:Ballot;
+ var b2:Ballot;
+ if (b1 == b2) {
+ } else if (BalLt(b1,b2)) {
+ } else {
+ //assert b1.seqno == b1.seqno;
+ //assert b2.seqno == b2.seqno;
+ assert BalLt(b2, b1); // Fails without asserts above
+ }
+}
\ No newline at end of file diff --git a/Test/dafny4/bug72.dfy.expect b/Test/dafny4/bug72.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/bug72.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 3 verified, 0 errors
|