Merge branch 'master' into meilers_term_plugin_deactive_flag

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/0740.vpr

@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Bool
+
+method fails(a: Bool)
+{
+    var curr: Ref := null
+
+    while (curr != null)
+        invariant curr != null ==> acc(curr.f)
+    {
+        refute false
+        curr := null
+    }
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}

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])
+}