Skip to content
Snippets Groups Projects
Commit 8eb42928 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Don't refresh ids in problem if not needed

parent 61bdb4ae
No related branches found
No related tags found
No related merge requests found
......@@ -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)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment