From 45963f7c266eeed146a3caa1df6560007f527611 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 13 Dec 2012 17:04:55 +0100
Subject: [PATCH] Fix buggy stop() on non-parallel synthesis searches
---
src/main/scala/leon/synthesis/SimpleSearch.scala | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 88a51b805..d3ddd5153 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -68,8 +68,12 @@ class SimpleSearch(synth: Synthesizer,
}
}
+ var shouldStop = false
+
def search(): Option[Solution] = {
- while (!g.tree.isSolved) {
+ shouldStop = false
+
+ while (!g.tree.isSolved && !shouldStop) {
nextLeaf() match {
case Some(l) =>
l match {
@@ -86,4 +90,10 @@ class SimpleSearch(synth: Synthesizer,
}
g.tree.solution
}
+
+ override def stop() {
+ super.stop()
+ shouldStop = true
+ sctx.solver.halt()
+ }
}
--
GitLab