diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 68709c64e1bcd21df8de780c4a6c317af6384581..9e97c6c7bfc097c811d86bc825e5082a9be7c7c1 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -652,15 +652,16 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
         val solverf = SolverFactory.getFromSettings(ctx, program)
         val solver  = solverf.getNewSolver()
 
-        val eqs = p.as.map {
-          case id =>
-            Equals(Variable(id), rctx.mappings(id))
-        }
-
-        val cnstr = andJoin(eqs ::: p.pc :: p.phi :: Nil)
-        solver.assertCnstr(cnstr)
 
         try {
+          val eqs = p.as.map {
+            case id =>
+              Equals(Variable(id), rctx.mappings(id))
+          }
+
+          val cnstr = andJoin(eqs ::: p.pc :: p.phi :: Nil)
+          solver.assertCnstr(cnstr)
+
           solver.check match {
             case Some(true) =>
               val model = solver.getModel
@@ -681,6 +682,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
             case _ =>
               throw RuntimeError("Timeout exceeded")
           }
+        } catch {
+          case e: Throwable =>
+            throw EvalError("Runtime synthesis of choose failed: "+e.getMessage)
         } finally {
           solverf.reclaim(solver)
           solverf.shutdown()
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index b2003d1012dcd35fab90c3cbc3d0f450e505f94b..79ee4c3cfdf4d2bf6d514df270fef164455c47ac 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -65,7 +65,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
         r
       case None =>
         context.reporter.debug("No solver succeeded")
-        fs.foreach(f => println(f.value))
+        //fs.foreach(f => println(f.value))
         None
     }