diff --git a/src/test/resources/regression/verification/purescala/valid/Nat.scala b/src/test/resources/regression/verification/purescala/valid/Nat.scala
index 498373c4ac3cb0c95948ac6d0b6e0831f74352f0..2c6b8724aa090bb3420d8714153e59000a7b83d5 100644
--- a/src/test/resources/regression/verification/purescala/valid/Nat.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Nat.scala
@@ -18,7 +18,10 @@ object Nat {
     case Succ(n1) => 1 + nat2Int(n1)
   }
 
-  def int2Nat(n: Int): Nat = if (n == 0) Zero() else Succ(int2Nat(n-1))
+  def int2Nat(n: Int): Nat = {
+    require(n >= 0)
+    if (n == 0) Zero() else Succ(int2Nat(n-1))
+  }
 
   def sum_lemma(): Boolean = {
     3 == nat2Int(plus(int2Nat(1), int2Nat(2)))