diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 6fde42aecd40673887f723438b9ab2acbdbb3ef6..ca3fdd6761bc35099df89ec194127e6a9be1dd2c 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -9,7 +9,7 @@ import java.io.File
import scala.reflect.ClassTag
/** Everything that is part of a compilation unit, except the actual program tree.
- * Contexts are immutable, and so should all there fields (with the possible
+ * Contexts are immutable, and so should all their fields (with the possible
* exception of the reporter).
*/
case class LeonContext(
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index 18a9159c3cb0e29f47e0757314f935865f6b10cf..985b2988504757a05ec2b881880f5609898e5833 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -6,6 +6,6 @@ package evaluators
import purescala.Definitions.Program
class DefaultEvaluator(ctx: LeonContext, prog: Program)
- extends RecursiveEvaluator(ctx, prog, 5000)
+ extends RecursiveEvaluator(ctx, prog, 50000)
with HasDefaultGlobalContext
with HasDefaultRecContext
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 689980682c86d03bb715b50e0dd2ff6ce530c331..b101f9de4e1fb6abb3d981830a2e551981803f3e 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -29,7 +29,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
lazy val scalaEv = new ScalacEvaluator(this, ctx, prog)
- protected var clpCache = Map[(Choose, Seq[Expr]), Expr]()
+ protected val clpCache = MutableMap[(Choose, Seq[Expr]), Expr]()
protected var frlCache = Map[(Forall, Seq[Expr]), Expr]()
private var evaluationFailsOnChoose = false
diff --git a/src/main/scala/leon/grammars/Grammars.scala b/src/main/scala/leon/grammars/Grammars.scala
index 06aba3d5f5343cc7e2807854f0b4665bfa1a602c..388a610d2010c4dac270bd12115511f0872792d8 100644
--- a/src/main/scala/leon/grammars/Grammars.scala
+++ b/src/main/scala/leon/grammars/Grammars.scala
@@ -18,8 +18,8 @@ object Grammars {
EqualityGrammar(Set(IntegerType, Int32Type, BooleanType) ++ inputs.map { _.getType }) ||
OneOf(inputs) ||
Constants(currentFunction.fullBody) ||
- FunctionCalls(prog, currentFunction, inputs.map(_.getType), exclude) ||
- SafeRecursiveCalls(prog, ws, pc)
+ // SafeRecursiveCalls(prog, ws, pc) ||
+ FunctionCalls(prog, currentFunction, inputs.map(_.getType), exclude)
}
def default(sctx: SynthesisContext, p: Problem): ExpressionGrammar[TypeTree] = {
diff --git a/src/main/scala/leon/grammars/SafeRecursiveCalls.scala b/src/main/scala/leon/grammars/SafeRecursiveCalls.scala
index f3234176a8c17378a7a5f027f38cbd42069ae7d6..938f88597221e5b8d29aac0c17e5bc6e7417a879 100644
--- a/src/main/scala/leon/grammars/SafeRecursiveCalls.scala
+++ b/src/main/scala/leon/grammars/SafeRecursiveCalls.scala
@@ -16,18 +16,17 @@ import synthesis.utils.Helpers._
*/
case class SafeRecursiveCalls(prog: Program, ws: Expr, pc: Expr) extends ExpressionGrammar[TypeTree] {
def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Prod] = {
- val calls = terminatingCalls(prog, t, ws, pc)
+ val calls = terminatingCalls(prog,ws, pc, Some(t), true)
- calls.map {
- case (fi, free) =>
+ calls.map { c => (c: @unchecked) match {
+ case (fi, Some(free)) =>
val freeSeq = free.toSeq
nonTerminal(
- freeSeq.map(_.getType),
- { sub => replaceFromIDs(freeSeq.zip(sub).toMap, fi) },
+ freeSeq.map(_.getType), { sub => replaceFromIDs(freeSeq.zip(sub).toMap, fi) },
Tags.tagOf(fi.tfd.fd, isSafe = true),
2
)
- }
+ }}
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 3a86ca64a79238aec4e59b197e001fd4c24660b4..1ed75343c0ba8c4953c3d2df9ac74cd057fe7ba0 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -7,7 +7,7 @@ import purescala.Common._
import purescala.Expressions._
import purescala.Types._
import purescala.ExprOps._
-import purescala.Constructors.and
+import purescala.Constructors._
import rules._
/** A Rule can be applied on a synthesis problem */
@@ -56,6 +56,7 @@ object Rules {
OptimisticGround,
EqualitySplit,
InequalitySplit,
+ IntroduceRecCall,
if(naiveGrammar) NaiveCEGIS else CEGIS,
//TEGIS,
//BottomUpTEGIS,
@@ -213,4 +214,20 @@ trait RuleDSL {
case _ => None
}
+
+ /** Straightforward combination of solutions, where expression is reconstructed according to a combiner.
+ * If combiner fails, no solution will be returned.
+ *
+ * @param combiner The combiner of synthesized subterms which reconstructs the term of the solution from the subterms.
+ */
+ def simpleCombine(combiner: PartialFunction[List[Expr], Expr]): List[Solution] => Option[Solution] = { ls =>
+ combiner.lift(ls map (_.term)).map{ combined =>
+ Solution(
+ orJoin(ls map (_.pre)),
+ ls.flatMap (_.defs).toSet,
+ combined,
+ ls.forall(_.isTrusted)
+ )
+ }
+ }
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index b01077ce751f6b53e397b15eb3d5126e560d1b56..5b2a9a9f16e414f37e3d257b2ee775ad675c89ed 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -4,7 +4,6 @@ package leon
package synthesis
import solvers._
-import solvers.combinators._
import purescala.Definitions.{Program, FunDef}
import evaluators._
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 7461f4d58c1a9213dd68168e4f7e4551eeee1711..9787811b7383112961443f0b13db0f0fbe1ef25c 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -114,7 +114,6 @@ case object ADTInduction extends Rule("ADT Induction") {
val funPre = substAll(substMap, and(p.pc, orJoin(globalPre)))
val funPost = substAll(substMap, p.phi)
val idPost = FreshIdentifier("res", resType)
- val outerPre = orJoin(globalPre)
newFun.precondition = Some(funPre)
newFun.postcondition = Some(Lambda(Seq(ValDef(idPost)), letTuple(p.xs.toSeq, Variable(idPost), funPost)))
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 29f27a93128bc58acf97961d0314a8472391df2b..543d6d75339400d6f6e5714b38703b38b39f0889 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -25,7 +25,7 @@ case object CaseSplit extends Rule("Case-Split") {
val pre = orJoin(sols.map(_.pre))
val defs = sols.map(_.defs).reduceLeft(_ ++ _)
- val (prefix, last) = (sols.dropRight(1), sols.last)
+ val (prefix, last) = (sols.init, sols.last)
val term = prefix.foldRight(last.term) { (s, t) => IfExpr(s.pre, s.term, t) }
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 79595656c4c53cca6e47747ac34a52f436697b31..50a38abc6fe5dbe434b799caaeb67ee48274cbf8 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -55,12 +55,7 @@ case object EqualitySplit extends Rule("Eq. Split") {
eb = p.qeb.filterIns( (m: Map[Identifier, Expr]) => m(a1) != m(a2))
)
- val onSuccess: List[Solution] => Option[Solution] = {
- case List(s1, s2) =>
- Some(Solution(or(s1.pre, s2.pre), s1.defs ++ s2.defs, IfExpr(Equals(Variable(a1), Variable(a2)), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
- case _ =>
- None
- }
+ val onSuccess = simpleCombine { case List(s1, s2) => IfExpr(Equals(Variable(a1), Variable(a2)), s1, s2) }
Some(decomp(List(sub1, sub2), onSuccess, s"Eq. Split on '$a1' and '$a2'"))
case _ =>
diff --git a/src/main/scala/leon/synthesis/rules/IndependentSplit.scala b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
index 72be06b9cff76a63ced4506ef086a58622326bef..2873eaf42c0a2be2aa3203b4681d031c9c8c7929 100644
--- a/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
@@ -4,13 +4,10 @@ package leon
package synthesis
package rules
-import leon.utils._
-import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
import purescala.Constructors._
import purescala.Common._
-import purescala.Types.CaseClassType
case object IndependentSplit extends NormalizingRule("IndependentSplit") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -68,7 +65,7 @@ case object IndependentSplit extends NormalizingRule("IndependentSplit") {
letTuple(xs, term, expr)
}
- Some(Solution(andJoin(sols.map(_.pre)), sols.map(_.defs).flatten.toSet, term, sols.forall(_.isTrusted)))
+ Some(Solution(andJoin(sols.map(_.pre)), sols.flatMap(_.defs).toSet, term, sols.forall(_.isTrusted)))
}
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 8b728930a10ad7d73c121762bde43637ce988fbc..71fd516d88b51825cd35b348cebc5205a3579103 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -10,8 +10,6 @@ import purescala.Constructors._
import purescala.Extractors._
import purescala.Common._
-import scala.concurrent.duration._
-
case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
// We approximate knowledge of equality based on facts found at the top-level
@@ -43,24 +41,17 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
candidates.collect {
case List(a1, a2) =>
- val onSuccess: List[Solution] => Option[Solution] = {
+ val onSuccess = simpleCombine {
case sols@List(sLT, sEQ, sGT) =>
- val pre = orJoin(sols.map(_.pre))
- val defs = sLT.defs ++ sEQ.defs ++ sGT.defs
-
- val term = IfExpr(
+ IfExpr(
LessThan(Variable(a1), Variable(a2)),
- sLT.term,
+ sLT,
IfExpr(
Equals(Variable(a1), Variable(a2)),
- sEQ.term,
- sGT.term
+ sEQ,
+ sGT
)
)
-
- Some(Solution(pre, defs, term, sols.forall(_.isTrusted)))
- case _ =>
- None
}
val subTypes = List(p.outType, p.outType, p.outType)
diff --git a/src/main/scala/leon/synthesis/rules/InputSplit.scala b/src/main/scala/leon/synthesis/rules/InputSplit.scala
index 4b9ffef53793528b628b41485c0a9156e171f188..b7566af94ae5e9908890e3cf4dd7085413ee9322 100644
--- a/src/main/scala/leon/synthesis/rules/InputSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InputSplit.scala
@@ -4,44 +4,40 @@ package leon
package synthesis
package rules
-import leon.purescala.Common.Identifier
import purescala.Expressions._
-import purescala.Extractors._
import purescala.ExprOps._
import purescala.Constructors._
import purescala.Types._
-import solvers._
-
-import scala.concurrent.duration._
-
case object InputSplit extends Rule("In. Split") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
p.as.filter(_.getType == BooleanType).flatMap { a =>
- def getProblem(v: Boolean): Problem = {
- def replaceA(e: Expr) = replaceFromIDs(Map(a -> BooleanLiteral(v)), e)
-
- p.copy(
- as = p.as.filterNot(_ == a),
- ws = replaceA(p.ws),
- pc = replaceA(p.pc),
- phi = replaceA(p.phi),
- eb = p.qeb.removeIns(Set(a))
- )
- }
-
- val sub1 = getProblem(true)
- val sub2 = getProblem(false)
-
- val onSuccess: List[Solution] => Option[Solution] = {
- case List(s1, s2) =>
- Some(Solution(or(and(Equals(Variable(a), BooleanLiteral(true)), s1.pre),
- and(Equals(Variable(a), BooleanLiteral(false)), s2.pre)),
- s1.defs ++ s2.defs,
- IfExpr(Variable(a), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
- case _ =>
- None
- }
+ def getProblem(v: Boolean): Problem = {
+ def replaceA(e: Expr) = replaceFromIDs(Map(a -> BooleanLiteral(v)), e)
+
+ val tests = QualifiedExamplesBank(p.as, p.xs, p.qeb.filterIns(m => m(a) == BooleanLiteral(v)))
+
+ p.copy(
+ as = p.as.filterNot(_ == a),
+ ws = replaceA(p.ws),
+ pc = replaceA(p.pc),
+ phi = replaceA(p.phi),
+ eb = tests.removeIns(Set(a))
+ )
+ }
+
+ val sub1 = getProblem(true)
+ val sub2 = getProblem(false)
+
+ val onSuccess: List[Solution] => Option[Solution] = {
+ case List(s1, s2) =>
+ Some(Solution(or(and(Equals(Variable(a), BooleanLiteral(true)), s1.pre),
+ and(Equals(Variable(a), BooleanLiteral(false)), s2.pre)),
+ s1.defs ++ s2.defs,
+ IfExpr(Variable(a), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
+ case _ =>
+ None
+ }
Some(decomp(List(sub1, sub2), onSuccess, s"Split on '$a'"))
}
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e50d0c72a49e5a40f36985101a36df04c5aa9725
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala
@@ -0,0 +1,90 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import evaluators.DefaultEvaluator
+import purescala.Definitions.Program
+import purescala.Extractors.TopLevelAnds
+import purescala.Expressions._
+import purescala.Constructors._
+import purescala.Common._
+import Witnesses.Terminating
+import utils.Helpers.terminatingCalls
+
+case object IntroduceRecCall extends NormalizingRule("Introduce rec. calls") {
+
+ private class NoChooseEvaluator(ctx: LeonContext, prog: Program) extends DefaultEvaluator(ctx, prog) {
+ override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
+ case ch: Choose =>
+ throw EvalError("Encountered choose!")
+ case _ =>
+ super.e(expr)
+ }
+ }
+
+ def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ val evaluator = new NoChooseEvaluator(hctxToCtx, hctx.program)
+
+ val calls = terminatingCalls(hctx.program, p.ws, p.pc, None, false)
+
+ calls.map { case (newCall, _) =>
+ val rec = FreshIdentifier("rec", newCall.getType, alwaysShowUniqueID = true)
+
+ val newWs = {
+ val TopLevelAnds(ws) = p.ws
+ andJoin(ws filter {
+ case Terminating(tfd, _) if tfd == newCall.tfd =>
+ false
+ case _ =>
+ true
+ })
+ }
+
+ // Assume the postcondition of recursive call
+ val post = application(
+ newCall.tfd.withParamSubst(newCall.args, newCall.tfd.postOrTrue),
+ Seq(rec.toVariable)
+ )
+
+ val onSuccess = forwardMap(Let(rec, newCall, _))
+
+ new RuleInstantiation(s"Introduce recursive call $newCall", SolutionBuilderDecomp(List(p.outType), onSuccess)) {
+
+ def apply(nohctx: SearchContext) = {
+
+ val psol = new PartialSolution(hctx.search.g, true)
+ .solutionAround(hctx.currentNode)(Error(p.outType, "Encountered choose!"))
+ .getOrElse(hctx.sctx.context.reporter.fatalError("Unable to get outer solution"))
+ .term
+
+ val origImpl = hctx.sctx.functionContext.fullBody
+ hctx.sctx.functionContext.fullBody = psol
+
+ def mapExample(e: Example): List[Example] = {
+ val res = evaluator.eval(newCall, p.as.zip(e.ins).toMap)
+ res.result.toList map { e match {
+ case InExample(ins) =>
+ v => InExample(ins :+ v)
+ case InOutExample(ins, outs) =>
+ v => InOutExample(ins :+ v, outs)
+ }}
+ }
+
+ val newProblem = p.copy(
+ as = p.as :+ rec,
+ pc = and(p.pc, post),
+ ws = newWs,
+ eb = p.eb.map(mapExample)
+ )
+
+ hctx.sctx.functionContext.fullBody = origImpl
+
+ RuleExpanded(List(newProblem))
+ }
+ }
+
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 4bfedc4acbe59440ac7f3382c8187ae201775f02..aafd55eae040ece537e5494bc81658e2e7383193 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -40,12 +40,12 @@ object Helpers {
* For each returned call, one argument is substituted by a "smaller" one, while the rest are left as holes.
*
* @param prog The current program
- * @param tpe The expected type for the returned function calls
* @param ws Helper predicates that contain [[Terminating]]s with the initial calls
* @param pc The path condition
+ * @param tpe The expected type for the returned function calls. If absent, all types are permitted.
* @return A list of pairs of (safe function call, holes), where holes stand for the rest of the arguments of the function.
*/
- def terminatingCalls(prog: Program, tpe: TypeTree, ws: Expr, pc: Expr): List[(FunctionInvocation, Set[Identifier])] = {
+ def terminatingCalls(prog: Program, ws: Expr, pc: Expr, tpe: Option[TypeTree], introduceHoles: Boolean): List[(FunctionInvocation, Option[Set[Identifier]])] = {
val TopLevelAnds(wss) = ws
val TopLevelAnds(clauses) = pc
@@ -78,13 +78,13 @@ object Helpers {
}
val res = gs.flatMap {
- case Terminating(tfd, args) if isSubtypeOf(tfd.returnType, tpe) =>
+ case Terminating(tfd, args) if tpe forall (isSubtypeOf(tfd.returnType, _)) =>
val ids = tfd.params.map(vd => FreshIdentifier("<hole>", vd.getType, true)).toList
for (((a, i), tpe) <- args.zipWithIndex zip tfd.params.map(_.getType);
smaller <- argsSmaller(a, tpe)) yield {
- val args = ids.map(_.toVariable).updated(i, smaller)
- (FunctionInvocation(tfd, args), ids.toSet - ids(i))
+ val newArgs = (if (introduceHoles) ids.map(_.toVariable) else args).updated(i, smaller)
+ (FunctionInvocation(tfd, newArgs), if(introduceHoles) Some(ids.toSet - ids(i)) else None)
}
case _ =>
Nil
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 2875bf3ed074756c5089896c327b487cc029fe34..d8184447b38c43395d389c2ae97db3f564e8f1c9 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -3,25 +3,7 @@
package leon
package verification
-import utils.DebugSectionSynthesis
-import utils.DebugSectionVerification
-import leon.purescala
import purescala.Definitions.Program
-import purescala.Expressions._
-import purescala.Types.StringType
-import purescala.TypeOps
-import purescala.Quantification._
-import purescala.Constructors._
-import purescala.ExprOps._
-import purescala.Expressions.{Pattern, Expr}
-import purescala.Extractors._
-import purescala.TypeOps._
-import purescala.Types._
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Definitions._
-import purescala.SelfPrettyPrinter
-import leon.solvers.{ PartialModel, Model, SolverFactory }
case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
diff --git a/testcases/synthesis/etienne-thesis/AddressBook/Make.scala b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
index 1fd12466c2c6f932f776c893a66e1a290d2212ca..612effe382140cfc87bd0c12d791c4de9ddfae8e 100644
--- a/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
+++ b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
@@ -49,5 +49,18 @@ object AddressBookMake {
def makeAddressBook[A](as: AddressList[A]): AddressBook[A] = {
choose( (res: AddressBook[A]) => res.content == as.content && res.invariant )
+
+ /* as match {
+ case Nil() => AddressBook[A](Nil[A](), Nil[A]())
+ case Cons(x, xs) =>
+ val AddressBook(b, p) = makeAddressBook(xs)
+ if(x.priv) AddressBook(b, Cons(x, p))
+ else AddressBook(Cons(x, b), p)
+ }
+
+ } ensuring {
+ res => res.content == as.content && res.invariant */
}
+
+
}
diff --git a/testcases/synthesis/etienne-thesis/List/Split.scala b/testcases/synthesis/etienne-thesis/List/Split.scala
index fb98204096f3e4a97b990527e588b655e8b93fac..f37e68264a8b5c4030fa283abc630f22ef98cd6e 100644
--- a/testcases/synthesis/etienne-thesis/List/Split.scala
+++ b/testcases/synthesis/etienne-thesis/List/Split.scala
@@ -30,10 +30,6 @@ object Complete {
if(i < 0) -i else i
} ensuring(_ >= 0)
- def dispatch(es: (BigInt, BigInt), rest: (List, List)): (List, List) = {
- (Cons(es._1, rest._1), Cons(es._2, rest._2))
- }
-
def split(list : List) : (List,List) = {
choose { (res : (List,List)) => splitSpec(list, res) }
}