Skip to content
Snippets Groups Projects
Commit ff1c8857 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

No longer report warnings for empty unsat cores, as they represent a valid...

No longer report warnings for empty unsat cores, as they represent a valid scenario where unrolling is insufficient.
parent cb4d9d00
No related branches found
No related tags found
No related merge requests found
...@@ -173,7 +173,8 @@ case object CEGIS extends Rule("CEGIS", 150) { ...@@ -173,7 +173,8 @@ case object CEGIS extends Rule("CEGIS", 150) {
//println(synth.solver.solveSAT(And(mustBeUnsat +: bssAssumptions.toSeq))) //println(synth.solver.solveSAT(And(mustBeUnsat +: bssAssumptions.toSeq)))
//println("maxcore: "+bssAssumptions) //println("maxcore: "+bssAssumptions)
if (core.isEmpty) { 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() Set()
} else { } else {
core core
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment