From 8eb42928d5ff835131d3bab59e5f8278dc80dbf7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 17 May 2016 12:40:25 +0200
Subject: [PATCH] Don't refresh ids in problem if not needed
---
src/main/scala/leon/synthesis/Problem.scala | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 8d7677d32..903d9e25f 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -67,10 +67,13 @@ object Problem {
eb: ExamplesBank = ExamplesBank.empty,
fd: Option[FunDef] = None
): Problem = {
- val xs = {
- val tps = spec.getType.asInstanceOf[FunctionType].from
- tps map (FreshIdentifier("x", _, alwaysShowUniqueID = true))
- }.toList
+ val xs = (spec match {
+ case Lambda(args, _) => args.map(_.id)
+ case IsTyped(_, FunctionType(from, to)) =>
+ from map (FreshIdentifier("x", _, alwaysShowUniqueID = true))
+ case _ =>
+ throw LeonFatalError(s"$spec is the spec of a choose but is not a function?")
+ }).toList
val phi = application(simplifyLets(spec), xs map { _.toVariable})
val as = (variablesOf(phi) ++ pc.variables -- xs).toList.sortBy(_.name)
--
GitLab