Fix epfl-lara#1401

frontends/benchmarks/verification/valid/i1401.scala

@@ -0,0 +1,18 @@
+import stainless.lang._
+import stainless.annotation._
+import scala.collection.immutable.{Set => ScalaSet}
+
+object i1401 {
+  case class Set[T](@extern @pure s: ScalaSet[T]) {
+    @extern
+    def apply(t: T): Boolean = s(t)
+
+    @extern
+    def subsetOf(that: Set[T]): Boolean = s.subsetOf(that.s)
+
+    @extern
+    def ++(that: Set[T]): Set[T] = {
+      Set(s ++ that.s)
+    }.ensuring(res => this.subsetOf(res) && that.subsetOf(res))
+  }
+}

frontends/scalac/src/main/scala/stainless/frontends/scalac/FragmentChecker.scala

@@ -263,7 +263,8 @@ trait FragmentChecker extends SubComponent { self: StainlessExtraction =>
 
         // ignore param accessors because they are duplicates of constructor parameters.
         // We catch them when we check constructors
-        if ((sym.tpe ne null) && !sym.isParamAccessor) {
+        // Also ignore *here* class constructors because they contain param accessors.
+        if ((sym.tpe ne null) && !sym.isParamAccessor && !sym.isClassConstructor) {
           checkType(tree.pos, sym.tpe)
         }
       } else {