diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 579e1803c770ba740f3c6d915ed6d9ca1579c558..71b49841f1c647c6cb851f529da76a1864037c5e 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -57,7 +57,6 @@ object Main {
     val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
     val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
     val optLazyEval   	= LeonFlagOptionDef("lazy",    "Handles programs that may use the lazy construct",   false)
-    //val optMemoize   	= LeonFlagOptionDef("memoize",    "Handles programs that uses memoization",   false)
 
     override val definedOptions: Set[LeonOptionDef[Any]] =
       Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval)
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index 032ace5c3a38e2d1ebf9b2d7a86e5844605cac78..a85a7d4f5b9f55af812da50d577ec36d350b7ce5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -25,7 +25,7 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
   protected val tru = BooleanLiteral(true)
   //protected val zero = IntLiteral(0)
 
-  private val dumpVCtoConsole = true
+  private val dumpVCtoConsole = false
   private val dumpVCasText = false
 
   /**
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 0c54c5570a7f1024287ca60983ff00efca47264a..abfd45aacd140c5cd28bf99bc56e2568f07cb190 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -56,6 +56,9 @@ object LazinessEliminationPhase extends TransformationPhase {
 
   // options that control behavior
   val optRefEquality = LeonFlagOptionDef("refEq", "Uses reference equality for comparing closures", false)
+  val optUseOrb = LeonFlagOptionDef("useOrb", "Use Orb to infer constants", false)
+
+  override val definedOptions: Set[LeonOptionDef[Any]] = Set(optUseOrb)
 
   /**
    * TODO: add inlining annotations for optimization.