Dafny: make sure assume->assert transformation gives rise to a check

2 files changed, 41 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8cb67403..d0dfc9be 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1359,8 +1359,24 @@ Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this retur
 Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

+Refinement.dfy(179,5): Error BP5003: A postcondition might not hold on this return path.

+Refinement.dfy(112,15): Related location: This is the postcondition that might not hold.

+Refinement.dfy(176,9): Related location: Related location

+Execution trace:

+    (0,0): anon0

+Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path.

+Refinement.dfy(120,15): Related location: This is the postcondition that might not hold.

+Refinement.dfy(176,9): Related location: Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon3

+Refinement.dfy(189,7): Error: assertion violation

+Refinement.dfy[IncorrectConcrete](128,24): Related location: Related location

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 44 verified, 6 errors

+Dafny program verifier finished with 48 verified, 9 errors

 

 -------------------- RefinementErrors.dfy --------------------

 RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index c24ed555..da7f0ac2 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -166,3 +166,27 @@ module Client imports Concrete {
     }
   }
 }
+
+module IncorrectConcrete refines Abstract {
+  class MyNumber {
+    var a: int;
+    var b: int;
+    predicate Valid
+    {
+      N == 2*a - b
+    }
+    constructor Init()
+    {  // error: postcondition violation
+      a := b;
+    }
+    method Inc()
+    {  // error: postcondition violation
+      if (*) { a := a + 1; } else { b := b - 1; }
+    }
+    method Get() returns (n: int)
+    {
+      var k := a - b;
+      assert ...;  // error: assertion violation
+    }
+  }
+}