diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala index c20a80028aca7f6509b7f889c5e6be8bc115592c..eec8591db992ac76957ea60cc729f66da0233599 100644 --- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala +++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala @@ -434,4 +434,39 @@ class EvaluatorsTests extends LeonTestSuite { checkEvaluatorError(e, mkCall("c", IL(42))) } } + + test("Infinite Recursion") { + import codegen._ + + val p = """|object Program { + | import leon.Utils._ + | + | def c(i : Int) : Int = c(i-1) + |} + |""".stripMargin + + implicit val prog = parseString(p) + + val e = new CodeGenEvaluator(leonContext, prog, CodeGenParams(maxFunctionInvocations = 32)) + checkEvaluatorError(e, mkCall("c", IL(42))) + } + + test("Wrong Contracts") { + import codegen._ + + val p = """|object Program { + | import leon.Utils._ + | + | def c(i : Int) : Int = { + | require(i > 0); + | c(i-1) + | } + |} + |""".stripMargin + + implicit val prog = parseString(p) + + val e = new CodeGenEvaluator(leonContext, prog, CodeGenParams(checkContracts = true)) + checkError(e, mkCall("c", IL(-42))) + } }