Fix silent extraction issue with Dotty

epfl-lara · Jul 2, 2019 · b5a1aeb · b5a1aeb
1 parent d603698
commit b5a1aeb
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/frontends/benchmarks/verification/invalid/PreInPre.scala b/frontends/benchmarks/verification/invalid/PreInPre.scala
@@ -2,8 +2,11 @@ import stainless.annotation._
 import stainless.collection._
 
 object PreInPre {
+
   @induct
-  def f(t: List[BigInt], st: BigInt) {
+  def f(t: List[BigInt], st: BigInt): Unit = {
     require(t.head == st)
+    ()
   }
+
 }