diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala index 64a618129f07c0f825be8eeacaf861c62c692f63..124f79e9f6b0c58ee37ab13cd9c8bd64919d711e 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 ef9cdf7b032f242f49c2b214412c54ef9a4af72f..ad77182a864910fa69c06f9467e83b349f6e4d99 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,