From bcdc238120f2c4a5778b7692d907d9a08f58b8bc Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 8 Apr 2016 14:23:58 +0200
Subject: [PATCH] Terminating test with nested functions

---
 .../scala/leon/termination/StructuralSize.scala |  2 ++
 .../verification/purescala/valid/Nested16.scala | 17 +++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 src/test/resources/regression/verification/purescala/valid/Nested16.scala

diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 610472d92..e4b7d4213 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -78,8 +78,10 @@ trait StructuralSize {
       }).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus)
       case IntegerType =>
         FunctionInvocation(typedAbsBigIntFun, Seq(expr)) 
+/*
       case Int32Type =>
         FunctionInvocation(typedAbsIntFun, Seq(expr))
+*/
       case _ => InfiniteIntegerLiteral(0)
     }
   }
diff --git a/src/test/resources/regression/verification/purescala/valid/Nested16.scala b/src/test/resources/regression/verification/purescala/valid/Nested16.scala
new file mode 100644
index 000000000..411e4a27f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Nested16.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+object Nested16 {
+
+  def foo(i: BigInt): BigInt = {
+    def rec1(j: BigInt): BigInt = {
+      require(j >= 0)
+      def rec2(k: BigInt): BigInt = {
+        require(j > 0 || j == k)
+        if(k == 0) 0 else rec1(j-1)
+      }
+      rec2(j)
+    }
+    rec1(3)
+  } ensuring(0 == _)
+
+}
-- 
GitLab