We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 18f40f6 commit 232997bCopy full SHA for 232997b
src/main/scala/inox/ast/SymbolOps.scala
@@ -460,7 +460,10 @@ trait SymbolOps { self: TypeOps =>
460
// @nv: we make sure NOT to normalize choose ids as we may need to
461
// report models for unnormalized chooses!
462
case c: Choose =>
463
- replaceFromSymbols(variablesOf(c).map(v => v -> transformVar(v)).toMap, c)
+ replaceFromSymbols(variablesOf(c).map(v => v -> {
464
+ if (vars(v) || locals(v)) transformVar(v)
465
+ else getVariable(v, v.getType)
466
+ }).toMap, c)
467
468
// Make sure we don't lift applications to applications when they have basic shapes
469
case Application(liftable(_), args) if args.forall(liftable.unapply(_).isEmpty) =>
0 commit comments