From bf159267759cc088cf9941fe8e2d3a4a4758e8d8 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 4 Mar 2015 18:10:06 +0100
Subject: [PATCH] Make terminating per phase optional
---
src/main/scala/leon/Pipeline.scala | 2 +-
src/main/scala/leon/Settings.scala | 1 +
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 64a618129..124f79e9f 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -8,7 +8,7 @@ abstract class Pipeline[-F, +T] {
def andThen[G](thenn: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
def run(ctx : LeonContext)(v : F) : G = {
val s = self.run(ctx)(v)
- ctx.reporter.terminateIfError()
+ if(ctx.settings.terminateAfterEachPhase) ctx.reporter.terminateIfError()
thenn.run(ctx)(s)
}
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index ef9cdf7b0..ad77182a8 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -6,6 +6,7 @@ import utils.DebugSection
case class Settings(
val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
+ val terminateAfterEachPhase: Boolean = true, // Terminates Leon after each phase if an error occured
val debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
val termination: Boolean = false,
val repair: Boolean = false,
--
GitLab