diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala index 610472d92bcd8c43e80235c51b0fb89e9a5354bd..e4b7d42139f5a921c23012c202c7d877422b1803 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 0000000000000000000000000000000000000000..411e4a27f0fb918eba1cd5b8d31131f734d0142b --- /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 == _) + +}