diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 5377ffa2e2bcf8f110742fa5f02a137ec430a2cc..41974dccd80ff7028c7f1f50ae78f425d30e279b 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