Skip to content
Snippets Groups Projects
Commit b621f391 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Fix Choose handling in ImperativeCodeElimitation

parent 70b011d7
Branches
Tags
No related merge requests found
...@@ -252,8 +252,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef ...@@ -252,8 +252,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
} }
case c @ Choose(ids, b) => { case c @ Choose(ids, b) => {
//Recall that Choose cannot mutate variables from the scope //Recall that Choose cannot mutate variables from the scope
val (bodyRes, bodyScope, bodyFun) = toFunction(b) (c, (b2: Expr) => b2, Map())
(bodyRes, (b2: Expr) => Choose(ids, bodyScope(b2)).copiedFrom(c), bodyFun)
} }
case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map()) case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
case n @ NAryOperator(args, recons) => { case n @ NAryOperator(args, recons) => {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment