From eb451d8e263bf2dc90d10ac4f24b2f4be9657540 Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Thu, 2 Jul 2015 13:49:11 +0200 Subject: [PATCH] Indentation --- .../smtlib/SMTLIBQuantifiedSolver.scala | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala index 47a6bed09..95b3310d4 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 -- GitLab