From 1d97ed471cff9bb17a5a424643d57e99779c16ad Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 22 Apr 2015 15:12:38 +0200
Subject: [PATCH] Display something when we abort discovery due to too many
programs
---
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 9db05c70e..908ff0e10 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -143,8 +143,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
*/
def allPrograms(): Traversable[Set[Identifier]] = {
- if (allProgramsCount() > nProgramsLimit) {
- return Seq()
+ val allCount = allProgramsCount()
+ if (allCount > nProgramsLimit) {
+ ctx.reporter.debug(s"Exceeded program limit: $allCount > $nProgramsLimit")
+ return Seq()
}
var cache = Map[Identifier, Seq[Set[Identifier]]]()
--
GitLab