From e2f4b0a58451cd28b4351c5012064e60356f4164 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 23 Mar 2016 14:57:03 +0100
Subject: [PATCH] Fixed evaluation of ADT function fields in model extraction
---
.../scala/leon/solvers/unrolling/QuantificationManager.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
index 84f7d0ae5..af31e6543 100644
--- a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
@@ -1194,8 +1194,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
partials.get(encoded).orElse(types.get(tpe)).map { domain =>
val conditionals = domain.flatMap { case (b, m) =>
extract(b, m).map { args =>
- val result = evaluator.eval(application(value, args)).result.getOrElse {
- scala.sys.error("Unexpectedly failed to evaluate " + application(value, args))
+ val result = evaluator.eval(application(f, args)).result.getOrElse {
+ scala.sys.error("Unexpectedly failed to evaluate " + application(f, args))
}
val cond = if (m.args.exists(arg => isQuantifier(arg.encoded))) {
--
GitLab