From c19cd7b8d62c104ffe0f7db2087456cb92fac424 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 26 Oct 2015 15:10:16 +0100
Subject: [PATCH] Don't need to create untyped Expr
---
src/main/scala/leon/synthesis/ChooseInfo.scala | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 43e351086..20eeb723f 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -42,7 +42,6 @@ object ChooseInfo {
def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef): Seq[ChooseInfo] = {
- val actualBody = and(fd.precOrTrue, fd.body.get)
val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
val eFinder = new ExamplesFinder(ctx, prog)
@@ -50,7 +49,7 @@ object ChooseInfo {
// We are synthesizing, so all examples are valid ones
val functionEb = eFinder.extractFromFunDef(fd, partition = false)
- for ((ch, path) <- new ChooseCollectorWithPaths().traverse(actualBody)) yield {
+ for ((ch, path) <- new ChooseCollectorWithPaths().traverse(fd.fullBody)) yield {
val outerEb = if (path == BooleanLiteral(true)) {
functionEb
} else {
--
GitLab