Skip to content

Commit 0157b1b

Browse files
authored
Merge pull request #138 from jad-hamza/fix-109
Attempt fix for #109 (@samarion)
2 parents 18f40f6 + 232997b commit 0157b1b

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/main/scala/inox/ast/SymbolOps.scala

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -460,7 +460,10 @@ trait SymbolOps { self: TypeOps =>
460460
// @nv: we make sure NOT to normalize choose ids as we may need to
461461
// report models for unnormalized chooses!
462462
case c: Choose =>
463-
replaceFromSymbols(variablesOf(c).map(v => v -> transformVar(v)).toMap, c)
463+
replaceFromSymbols(variablesOf(c).map(v => v -> {
464+
if (vars(v) || locals(v)) transformVar(v)
465+
else getVariable(v, v.getType)
466+
}).toMap, c)
464467

465468
// Make sure we don't lift applications to applications when they have basic shapes
466469
case Application(liftable(_), args) if args.forall(liftable.unapply(_).isEmpty) =>

0 commit comments

Comments
 (0)