From 232997bfc4b63026bd85a876b145093f0087e171 Mon Sep 17 00:00:00 2001 From: Jad Hamza Date: Wed, 21 Apr 2021 14:43:09 +0200 Subject: [PATCH] Attempt fix for #109 (@samarion) --- src/main/scala/inox/ast/SymbolOps.scala | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala index 02c12f8da..8bf3e1635 100644 --- a/src/main/scala/inox/ast/SymbolOps.scala +++ b/src/main/scala/inox/ast/SymbolOps.scala @@ -460,7 +460,10 @@ trait SymbolOps { self: TypeOps => // @nv: we make sure NOT to normalize choose ids as we may need to // report models for unnormalized chooses! case c: Choose => - replaceFromSymbols(variablesOf(c).map(v => v -> transformVar(v)).toMap, c) + replaceFromSymbols(variablesOf(c).map(v => v -> { + if (vars(v) || locals(v)) transformVar(v) + else getVariable(v, v.getType) + }).toMap, c) // Make sure we don't lift applications to applications when they have basic shapes case Application(liftable(_), args) if args.forall(liftable.unapply(_).isEmpty) =>