From 136a6f1be19126893a7957ed1a87f952cf99057e Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 7 Nov 2016 09:40:51 +0100
Subject: [PATCH] Registered UnrollingSolver as interrupt handler
---
.../scala/inox/solvers/unrolling/QuantificationTemplates.scala | 2 +-
src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala | 2 ++
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index fdb065d00..ac9635208 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -317,7 +317,7 @@ trait QuantificationTemplates { self: Templates =>
if (handledMatchers(relevantBlockers -> matcher)) {
Seq.empty
} else if (interrupted) {
- ignoredMatchers += ((currentGeneration + 1, blockers, matcher))
+ ignoredMatchers += ((currentGeneration, blockers, matcher))
Seq.empty
} else {
ctx.reporter.debug(" -> instantiating matcher " + blockers.mkString("{",",","}") + " ==> " + matcher)
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index b21b0ce92..fae2c9e23 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -97,6 +97,8 @@ trait AbstractUnrollingSolver extends Solver { self =>
freeVars.reset()
}
+ ctx.interruptManager.registerForInterrupts(this)
+
override def interrupt(): Unit = {
interrupted = true
}
--
GitLab