From d39332d2b77c7efb24419402b8919f57a346e90d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 15 Oct 2015 13:03:39 +0200
Subject: [PATCH] Catch exceptions thrown in assertCnstr
---
.../leon/evaluators/RecursiveEvaluator.scala | 18 +++++++++++-------
.../solvers/combinators/PortfolioSolver.scala | 2 +-
2 files changed, 12 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 68709c64e..9e97c6c7b 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 b2003d101..79ee4c3cf 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
}
--
GitLab