From ac4ad2f84e9105770d7c9c12451f6096f6bf2433 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 28 Oct 2016 14:24:52 +0200
Subject: [PATCH] Fixed quantifier template unrolling for deferred ground
instantiations
---
.../inox/solvers/unrolling/QuantificationTemplates.scala | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 8c1358805..a6cc13624 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -246,7 +246,12 @@ trait QuantificationTemplates { self: Templates =>
for ((gen, qs) <- ignoredGrounds.toSeq if gen <= currentGeneration; q <- qs) {
clauses ++= q.ensureGrounds
- ignoredGrounds += gen -> (ignoredGrounds.getOrElse(gen, Set.empty) - q)
+ val remaining = ignoredGrounds.getOrElse(gen, Set.empty) - q
+ if (remaining.nonEmpty) {
+ ignoredGrounds += gen -> remaining
+ } else {
+ ignoredGrounds -= gen
+ }
}
clauses.toSeq
--
GitLab