diff --git a/src/main/scala/leon/evaluators/EvaluatorContexts.scala b/src/main/scala/leon/evaluators/EvaluatorContexts.scala index b5d3b4b5fd04db0e9118a653c058d04304c5d63e..859e960d5d7aadbc63de656fd3c340fbc60b30f1 100644 --- a/src/main/scala/leon/evaluators/EvaluatorContexts.scala +++ b/src/main/scala/leon/evaluators/EvaluatorContexts.scala @@ -15,34 +15,16 @@ trait RecContext[RC <: RecContext[RC]] { def newVars(news: Map[Identifier, Expr]): RC def withNewVar(id: Identifier, v: Expr): RC = { - if(!purescala.ExprOps.isValue(v)) { - println(s"Trying to add $id -> $v in context butnot a value") - println(Thread.currentThread().getStackTrace.map(_.toString).mkString("\n")) - System.exit(0) - } newVars(mappings + (id -> v)) } def withNewVars(news: Map[Identifier, Expr]): RC = { - if(news.exists{ case (k, v) => !purescala.ExprOps.isValue(v) }) { - println(s"Trying to add $news in context but not a value") - println(Thread.currentThread().getStackTrace.map(_.toString).mkString("\n")) - System.exit(0) - } newVars(mappings ++ news) } } case class DefaultRecContext(mappings: Map[Identifier, Expr]) extends RecContext[DefaultRecContext] { def newVars(news: Map[Identifier, Expr]) = copy(news) - - mappings.find{ case (k, v) => !purescala.ExprOps.isValue(v) } match { - case None => - case Some(a) => - println(s"Trying to add $mappings in context but $a has not a value as second argument (of type ${a._2.getType}) and class ${a._2.getClass} because ${purescala.ExprOps.msgs}") - println(Thread.currentThread().getStackTrace.map(_.toString).mkString("\n")) - System.exit(0) - } } class GlobalContext(val model: Model, val maxSteps: Int, val check: Boolean) { diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala index 1645b7bccd8c892b855f8b06c2bb42f5cbfd84a6..bdeff625545a1081700de01c57d0f317e0411d2d 100644 --- a/src/main/scala/leon/repair/rules/Focus.scala +++ b/src/main/scala/leon/repair/rules/Focus.scala @@ -66,7 +66,7 @@ case object Focus extends PreprocessingRule("Focus") { def existsFailing(e: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator): Boolean = { p.eb.invalids.exists { ex => - evaluator.evalEnvExpr(e, (p.as zip ex.ins).toMap ++ env) match { + evaluator.evalEnvExpr(e, (p.as zip ex.ins).toMap ++ env).result match { case Some(BooleanLiteral(b)) => b case _ => true }