Fixed some omitted cases in Substitute (and added "assume false" to catch any other, later)

1 files changed, 13 insertions, 0 deletions

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index b451cdf1..6b1b366d 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -249,3 +249,16 @@ method notQuiteSwap3(c: CC, d: CC)
   c.x, d.x := 4, c.y;

   c.x, c.y := 3, c.y;

 }

+

+// ---------------------------

+// regression tests of things that were once errors

+

+method InlineMultisetFormingExpr(s: seq<int>)

+  ensures MSFE(s);

+predicate MSFE(s: seq<int>)

+{

+  multiset(s) == multiset(s)

+}

+

+copredicate CoPredTypeCheck(n: int)

+  requires n != 0;