Merge pull request #730 from viperproject/meilers_fix_silicon_742

Added missing case (fixes Silicon issue #742)

Author: marcoeilers

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -140,6 +140,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
         case PMapType(_, _) => Seq("Map")
         case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances")
         case PDomainType(d, _) => Seq(d.name)
+        case gt: PGenericType => Seq(gt.genericName)
       }
       !typeNames.exists(tn => wfTypeName.contains(tn))
     }

src/test/resources/all/issues/silicon/0742.vpr

@@ -0,0 +1,28 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/all.vpr>
+
+domain ListWellFoundedOrder[T] {
+
+
+  axiom {
+    forall y : List[T] :: {bounded(y)} bounded(y)
+  }
+
+
+  axiom {
+    forall xs : List[T] , y : T ::
+      decreasing(xs, Cons(y, xs))
+  }
+
+  axiom {
+    forall xs : List[T], ys : List[T], zs : List[T] :: {decreasing(xs, ys), decreasing(ys, zs)}
+      decreasing(xs, ys) && decreasing(ys, zs) ==> decreasing(xs, zs)
+  }
+}
+
+adt List[T] {
+  Nil()
+  Cons(value : T, tail : List[T])
+}