fix(translator): Strip type constraints before generating rank axioms (…

…#1876)

* fix(translator): Strip type constraints before generating rank axioms

Fixes #1875

RELEASE_NOTES.md

@@ -10,7 +10,8 @@
 - fix: export-reveals of function-by-method now allows the function body to be ghost (https://github.com/dafny-lang/dafny/pull/1855)
 - fix: Regain C# 7.3 compatibility of the compiled code. (https://github.com/dafny-lang/dafny/pull/1877)
 - fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (https://github.com/dafny-lang/dafny/pull/1862)
-
+- fix: Plug two memory leaks in Dafny's verification server (#1858, #1863)
+- fix: Generate missing termination measures for subset types on sequences (#1875)
 
 # 3.4.2
 

Source/Dafny/Verifier/Translator.DataTypes.cs

@@ -500,7 +500,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor)
         AddOtherDefinition(fn, (new Bpl.Axiom(ctor.tok, q, "Constructor injectivity")));
 
         if (dt is IndDatatypeDecl) {
-          var argType = arg.Type.NormalizeExpandKeepConstraints(); // TODO: keep constraints -- really?  Write a test case
+          var argType = arg.Type.NormalizeExpand();
           if (argType.IsDatatype || argType.IsTypeParameter) {
             // for datatype:             axiom (forall params :: {#dt.ctor(params)} DtRank(params_i) < DtRank(#dt.ctor(params)));
             // for type-parameter type:  axiom (forall params :: {#dt.ctor(params)} BoxRank(params_i) < DtRank(#dt.ctor(params)));

Test/git-issues/git-issue-1875.dfy

@@ -0,0 +1,84 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+/// This file checks whether sufficient axioms are generated to compare
+/// datatypes constructed using subset types over sequences.
+
+module Datatype {
+  datatype Box_<T> = Box(t: T)
+  type Box<T> = b: Box_<T> | true witness *
+
+  datatype List<T> = Nil | Cons(t: T, Box<List<T>>)
+
+  function Length<T>(l: List<T>): int {
+    match l {
+      case Nil => 0
+      case Cons(t, q) => 1 + Length(q.t)
+    }
+  }
+}
+
+module Seq {
+  type Box_<T> = seq<T>
+  type Box<T> = b: Box_<T> | |b| == 1 witness *
+
+  datatype List<T> = Nil | Cons(t: T, Box<List<T>>)
+
+  function Length<T>(l: List<T>): int {
+    match l {
+      case Nil => 0
+      case Cons(t, q) =>
+        assert q[0] in q;
+        var l :| l in q;
+        Length(l)
+    }
+  }
+}
+
+module Set {
+  type Box_<T> = set<T>
+  type Box<T> = b: Box_<T> | |b| == 1 witness *
+
+  datatype List<T(==)> = Nil | Cons(t: T, Box<List<T>>)
+
+  function Length<T>(l: List<T>): int {
+    match l {
+      case Nil => 0
+      case Cons(t, q) =>
+        var l :| l in q;
+        Length(l)
+    }
+  }
+}
+
+module Multiset {
+  type Box_<T> = multiset<T>
+  type Box<T> = b: Box_<T> | |b| == 1 witness *
+
+  datatype List<T(==)> = Nil | Cons(t: T, Box<List<T>>)
+
+  function Length<T>(l: List<T>): int {
+    match l {
+      case Nil => 0
+      case Cons(t, q) =>
+        var l :| l in q;
+        Length(l)
+    }
+  }
+}
+
+module Map {
+  type Box_<T> = map<T, bool>
+  type Box<T> = b: Box_<T> | |b| == 1 witness *
+
+  datatype List<T(==)> = Nil | Cons(t: T, Box<List<T>>)
+
+  function Length<T>(l: List<T>): int {
+    match l {
+      case Nil => 0
+      case Cons(t, q) =>
+        var l :| l in q.Keys;
+        Length(l)
+    }
+  }
+}

Test/git-issues/git-issue-1875.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 5 verified, 0 errors