Skip to content
Snippets Groups Projects
Commit 36e65536 authored by Régis Blanc's avatar Régis Blanc
Browse files

some TODO we should not forget

parent 60269746
No related branches found
No related tags found
No related merge requests found
...@@ -433,7 +433,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ ...@@ -433,7 +433,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
reporter.info("UNSAT BECAUSE: "+core.mkString(" AND ")) reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
if (!forceStop) { if (!forceStop) {
if (Settings.luckyTest && false) { if (Settings.luckyTest && false) { //TODO: something with false
// we need the model to perform the additional test // we need the model to perform the additional test
reporter.info(" - Running search without blocked literals (w/ lucky test)") reporter.info(" - Running search without blocked literals (w/ lucky test)")
} else { } else {
...@@ -450,7 +450,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ ...@@ -450,7 +450,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore)) foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) => case Some(true) =>
//reporter.info("SAT WITHOUT Blockers") //reporter.info("SAT WITHOUT Blockers")
if (Settings.luckyTest && !forceStop) { if (Settings.luckyTest && !forceStop) { //TODO: still with the above "false"
// we might have been lucky :D // we might have been lucky :D
luckyTime.start luckyTime.start
val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC) val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment