From cc37598c2dd7786ded026f16fdb4c831bc3a8e54 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 9 Feb 2016 14:12:24 +0100
Subject: [PATCH] Tweaks
---
src/main/scala/leon/SharedOptions.scala | 15 ++++++---------
.../scala/leon/synthesis/rules/CEGISLike.scala | 2 +-
.../scala/leon/verification/InjectAsserts.scala | 1 -
3 files changed, 7 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 839dda206..b68e64c83 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -5,12 +5,11 @@ package leon
import leon.utils.{DebugSections, DebugSection}
import OptionParsers._
-/*
- * This object contains options that are shared among different modules of Leon.
- *
- * Options that determine the pipeline of Leon are not stored here,
- * but in MainComponent in Main.scala.
- */
+/** This object contains options that are shared among different modules of Leon.
+ *
+ * Options that determine the pipeline of Leon are not stored here,
+ * but in [[Main.MainComponent]] instead.
+ */
object SharedOptions extends LeonComponent {
val name = "sharedOptions"
@@ -45,7 +44,7 @@ object SharedOptions extends LeonComponent {
val name = "debug"
val description = {
val sects = DebugSections.all.toSeq.map(_.name).sorted
- val (first, second) = sects.splitAt(sects.length/2)
+ val (first, second) = sects.splitAt(sects.length/2 + 1)
"Enable detailed messages per component.\nAvailable:\n" +
" " + first.mkString(", ") + ",\n" +
" " + second.mkString(", ")
@@ -61,8 +60,6 @@ object SharedOptions extends LeonComponent {
Set(rs)
case None =>
throw new IllegalArgumentException
- //initReporter.error("Section "+s+" not found, available: "+DebugSections.all.map(_.name).mkString(", "))
- //Set()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index a5fceaad8..291e485d7 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -916,7 +916,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
case None =>
result = Some(RuleFailed())
}
-
+
timers.loop.stop()
}
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 4e126827b..1bd9a6957 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -8,7 +8,6 @@ import Expressions._
import ExprOps._
import Definitions._
import Constructors._
-import xlang.Expressions._
object InjectAsserts extends SimpleLeonPhase[Program, Program] {
--
GitLab