fix int2Nat function (was non-terminating for negative arguments)

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)))