diff --git a/src/test/scala/leon/integration/purescala/InliningSuite.scala b/src/test/scala/leon/integration/purescala/InliningSuite.scala index fbbc8765a1c3b627dccd0cf783f03d69eba8b126..069a0e5badea7be393be043fba0793844aa3d3d8 100644 --- a/src/test/scala/leon/integration/purescala/InliningSuite.scala +++ b/src/test/scala/leon/integration/purescala/InliningSuite.scala @@ -20,7 +20,7 @@ class InliningSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL | |} """.stripMargin, - """ |import leon.lang._ + """|import leon.lang._ |import leon.annotation._ | |object InlineBad { @@ -30,6 +30,21 @@ class InliningSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL | | def bar(a: BigInt) = foo(a) | + |}""".stripMargin, + + """|import leon.lang._ + |import leon.annotation._ + | + |object InlineGood2 { + | + | @inline + | def foo(a: BigInt) = true + | + | @inline + | def bar(a: BigInt) = foo(a) + | + | def baz(a: BigInt) = bar(a) + | |}""".stripMargin ) @@ -45,4 +60,9 @@ class InliningSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL fail(s"Resultig body should be a call to 'foo', got '$b'") } } + + test("Double Inlining") { implicit fix => + assert(funDef("InlineGood2.baz").fullBody == BooleanLiteral(true), "Inlined function invocation not inlined in turn?") + } + }