From be71561e2a2b3a66e96c0d382eab0af1ab003d69 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Wed, 3 Jun 2015 13:58:53 +0200
Subject: [PATCH] fix int2Nat function (was non-terminating for negative
arguments)
---
.../regression/verification/purescala/valid/Nat.scala | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/test/resources/regression/verification/purescala/valid/Nat.scala b/src/test/resources/regression/verification/purescala/valid/Nat.scala
index 498373c4a..2c6b8724a 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)))
--
GitLab