From 0ecddfff842eadb1abe8d04fe8714f006b88acb3 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 1 Nov 2016 15:44:37 +0100
Subject: [PATCH] You know where this is going by now...
---
.../inox/solvers/unrolling/QuantificationTemplates.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 705ec1905..0cce88476 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -593,7 +593,9 @@ trait QuantificationTemplates { self: Templates =>
handledMatchers.containsAll(ms.map(_.substitute(substituter, msubst)))
}
- if (isOpt) 0 else 3
+ if (isOpt) 0
+ else if (grounds(q)(bs, m.args(i))) 10
+ else 3
}
(bs, map, c + cost)
--
GitLab