From b621f3916b2e41ea052488c498b61f22adce8bff Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 20 Feb 2014 16:08:35 +0100
Subject: [PATCH] Fix Choose handling in ImperativeCodeElimitation
---
src/main/scala/leon/xlang/ImperativeCodeElimination.scala | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 7042557ea..397744e10 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -252,8 +252,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
}
case c @ Choose(ids, b) => {
//Recall that Choose cannot mutate variables from the scope
- val (bodyRes, bodyScope, bodyFun) = toFunction(b)
- (bodyRes, (b2: Expr) => Choose(ids, bodyScope(b2)).copiedFrom(c), bodyFun)
+ (c, (b2: Expr) => b2, Map())
}
case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
case n @ NAryOperator(args, recons) => {
--
GitLab