diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 19f44bb33c859aadceb0914d634a8f637283d800..f4d8395368128db22b2ed19d6be39eece5151266 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -84,6 +84,11 @@ object Solution {
     new Solution(BooleanLiteral(true), Set(), simplestValue(t))
   }
 
+  def failed(implicit p: Problem): Solution = {
+    val tpe = tupleTypeWrap(p.xs.map(_.getType))
+    Solution(BooleanLiteral(false), Set(), Error(tpe, "Rule failed!"))
+  }
+
   def UNSAT(implicit p: Problem): Solution = {
     val tpe = tupleTypeWrap(p.xs.map(_.getType))
     Solution(BooleanLiteral(false), Set(), Error(tpe, p.phi+" is UNSAT!"))
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 6ba4adebfe311713013dc52ce9b4a77866cbd814..46ecb4e33b6a98530471c6c6ab22a57415b37313 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -27,6 +27,8 @@ class Synthesizer(val context : LeonContext,
 
   val reporter = context.reporter
 
+  lazy val sctx = SynthesisContext.fromSynthesizer(this)
+
   def getSearch(): Search = {
     if (settings.manualSearch.isDefined) {
       new ManualSearch(context, ci, problem, settings.costModel, settings.manualSearch)
@@ -41,8 +43,6 @@ class Synthesizer(val context : LeonContext,
   def synthesize(): (Search, Stream[Solution]) = {
     val s = getSearch();
 
-    val sctx = SynthesisContext.fromSynthesizer(this)
-
     val t = context.timers.synthesis.search.start()
 
     val sols = s.search(sctx)