diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index 63db3ca0a70d718ae6aacd84b7c449d29efa866b..c5ae914f2f41572bf27aadd4eb65ee7553fd8113 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -51,7 +51,8 @@ class Synthesizer(val reporter: Reporter, } } - while (!workList.isEmpty) { + var continue = true + while (!workList.isEmpty && continue) { val task = workList.dequeue() val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root")) @@ -78,7 +79,19 @@ class Synthesizer(val reporter: Reporter, if (timeoutExpired()) { warning("Timeout reached") - workList.clear() + continue = false + } + } + + if (!workList.isEmpty) { + // We flush the worklist by solving everything with chooses, that should + // rebuild a partial solution + while (!workList.isEmpty) { + val t = workList.dequeue() + + if (t.parent ne null) { + t.parent.partlySolvedBy(t, Solution.choose(t.problem)) + } } }