diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
index 47a6bed091305e1f9ef1f9a93c2c6154874d9599..95b3310d42b8b4cbe5983104f286d409a06d2eb8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -27,16 +27,16 @@ trait SMTLIBQuantifiedSolver extends SMTLIBSolver {
     val inductiveHyps = for {
       fi@FunctionInvocation(tfd, args) <- functionCallsOf(cond).toSeq
     } yield {
-        val formalToRealArgs = tfd.params.map{ _.id}.zip(args).toMap
-        val post = tfd.postcondition map { post =>
-          application(
-            replaceFromIDs(formalToRealArgs, post),
-            Seq(fi)
-          )
-        } getOrElse BooleanLiteral(true)
-        val pre = tfd.precondition getOrElse BooleanLiteral(true)
-        and(pre, post)
-      }
+      val formalToRealArgs = tfd.params.map{ _.id}.zip(args).toMap
+      val post = tfd.postcondition map { post =>
+        application(
+          replaceFromIDs(formalToRealArgs, post),
+          Seq(fi)
+        )
+      } getOrElse BooleanLiteral(true)
+      val pre = tfd.precondition getOrElse BooleanLiteral(true)
+      and(pre, post)
+    }
 
     // We want to check if the negation of the vc is sat under inductive hyp.
     // So we need to see if (indHyp /\ !vc) is satisfiable