Unknown variable crash in evaluator on code that works in scala repl

[vkuncak]

I wrote a small lambda calculus evaluator and was testing it using --eval (no pun intended). This reveals what seems like a bug in evaluating closures in our evaluator.

[Internal] Evaluator error (No value for variable v1 in mapping Map(ValDef(op, (Int, Int) => Int, Set()) -> (x$64: Int, x$65: Int) => { [Internal] require(true) [Internal] x$64 + x$65 [Internal] })) while evaluating stdEnv's body. [Internal] Please inform the authors of Inox about this message [Internal] inox.package$FatalError: Evaluator error (No value for variable v1 in mapping Map(ValDef(op, (Int, Int) => Int, Set()) -> (x$64: Int, x$65: Int) => { [Internal] require(true) [Internal] x$64 + x$65 [Internal] })) while evaluating stdEnv's body. [Internal] Please inform the authors of Inox about this message [Internal] java.util.concurrent.ExecutionException: java.lang.RuntimeException: inox.package$FatalError: inox.package$FatalError: Evaluator error (No value for variable v1 in mapping Map(ValDef(op, (Int, Int) => Int, Set()) -> (x$64: Int, x$65: Int) => { [Internal] require(true) [Internal] x$64 + x$65 [Internal] })) while evaluating stdEnv's body. [Internal] Please inform the authors of Inox about this message

Lambda.scala.txt

[mantognini]

I've minimised the program to this: https://github.com/epfl-lara/stainless/issues/141#issuecomment-352815498

It appears that the issue is not with the evaluator itself but with how preconditions are inserted during internal tree transformations, as shown by this trace:

[ Debug  ] Calling lift: typed def lift[]'s full body:
[ Debug  ] require(v1.isInstanceOf[IntegerValue] ==> {
[ Debug  ]   val c1: Int = v1.asInstanceOf[IntegerValue].c
[ Debug  ]   v2.isInstanceOf[IntegerValue] ==> {
[ Debug  ]     val c2: Int = v2.asInstanceOf[IntegerValue].c
[ Debug  ]     op.pre(c1, c2)
[ Debug  ]   }
[ Debug  ] })
[ Debug  ] FunctionValue((v1: Value) => {
[ Debug  ]   require(true)
[ Debug  ]   v1 match {
[ Debug  ]     case IntegerValue(c1) =>
[ Debug  ]       FunctionValue((v2: Value) => {
[ Debug  ]         require(v2.isInstanceOf[IntegerValue] ==> {
[ Debug  ]           val c2: Int = v2.asInstanceOf[IntegerValue].c
[ Debug  ]           op.pre(c1, c2)
[ Debug  ]         })
[ Debug  ]         v2 match {
[ Debug  ]           case IntegerValue(c2) =>
[ Debug  ]             IntegerValue(op(c1, c2))
[ Debug  ]         }
[ Debug  ]       })
[ Debug  ]   }
[ Debug  ] })

Because the bug seems related to #141 I mark this one as a duplicate and continue the discussion over there.