diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala index 3034ea26a01b6ec5233f2e28030b1a28f293b349..7af24d851c3f15d9f5c2044c0b0236e2023501e0 100644 --- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala +++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala @@ -155,7 +155,7 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu def matchesPattern(pat: Pattern, expr: Expr, exprFromScrut: Expr): Option[Map[Identifier, (Expr, Expr)]] = (pat, expr) match { case (InstanceOfPattern(ob, pct), e) => if (isSubtypeOf(e.getType, pct)) { - Some(obind(ob, e, exprFromScrut)) + Some(obind(ob, e, AsInstanceOf(exprFromScrut, pct))) } else { None }