From ff1c8857cf673b3ba8333ddb965834fd8fb8f974 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 29 Nov 2012 15:58:08 +0100
Subject: [PATCH] No longer report warnings for empty unsat cores, as they
represent a valid scenario where unrolling is insufficient.
---
src/main/scala/leon/synthesis/rules/Cegis.scala | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 5377ffa2e..41974dccd 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -173,7 +173,8 @@ case object CEGIS extends Rule("CEGIS", 150) {
//println(synth.solver.solveSAT(And(mustBeUnsat +: bssAssumptions.toSeq)))
//println("maxcore: "+bssAssumptions)
if (core.isEmpty) {
- sctx.reporter.warning("Got empty core, must be unsat without assumptions!")
+ // This happens if unrolling level is insufficient, it becomes unsat no matter what the assumptions are.
+ //sctx.reporter.warning("Got empty core, must be unsat without assumptions!")
Set()
} else {
core
--
GitLab