diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala index 8c135880502a438204336f277cea58c895144c1d..a6cc136245cf040595c7ecaec2bc36370c8c2bab 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