From f1fecf942143d3f96e3768830926a88e07e9fd42 Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Wed, 1 Jul 2015 18:38:16 +0200 Subject: [PATCH] Blah --- src/main/scala/leon/synthesis/rules/IntInduction.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala index 8f619667a..c9c61ffd7 100644 --- a/src/main/scala/leon/synthesis/rules/IntInduction.scala +++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala @@ -55,8 +55,8 @@ case object IntInduction extends Rule("Int Induction") { IfExpr(Equals(Variable(inductOn), InfiniteIntegerLiteral(0)), base.toExpr, IfExpr(GreaterThan(Variable(inductOn), InfiniteIntegerLiteral(0)), - letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Minus(Variable(inductOn), InfiniteIntegerLiteral(1)))), gt.toExpr) - , letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Plus(Variable(inductOn), InfiniteIntegerLiteral(1)))), lt.toExpr))) + letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Minus(Variable(inductOn), InfiniteIntegerLiteral(1)))), gt.toExpr), + letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Plus(Variable(inductOn), InfiniteIntegerLiteral(1)))), lt.toExpr))) ) -- GitLab