From 3f1a23c0c671c723929c4e5c2768672de11d8897 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 9 Feb 2016 14:14:15 +0100
Subject: [PATCH] Small fix to DualEvaluator
---
src/main/scala/leon/evaluators/DualEvaluator.scala | 3 +--
src/main/scala/leon/evaluators/RecursiveEvaluator.scala | 2 --
src/main/scala/leon/solvers/combinators/UnrollingSolver.scala | 1 -
3 files changed, 1 insertion(+), 5 deletions(-)
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index 6fc5b856d..7976dbfc2 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -37,8 +37,7 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams)
val (className, methodName, _) = unit.leonFunDefToJVMInfo(tfd.fd).get
- val allArgs =
- (if (params.requireMonitor) Seq(monitor) else Seq()) ++
+ val allArgs = Seq(monitor) ++
(if (tfd.fd.tparams.nonEmpty) Seq(tfd.tps.map(unit.registerType(_)).toArray) else Seq()) ++
args
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index e7ff08ba6..22aa09a4d 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -567,8 +567,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
ctx.reporter.debug("Verification took "+total+"ms")
ctx.reporter.debug("Finished forall evaluation with: "+res)
- println(fargs.map(_.id),replaceFromIDs(mapping, body))
- println(res)
frlCache += (f, context) -> res
res
case _ =>
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 6d7af0ba4..f97085857 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -263,7 +263,6 @@ trait AbstractUnrollingSolver[T]
private def getTotalModel: Model = {
val wrapped = solverGetModel
- println(wrapped)
val typeInsts = templateGenerator.manager.typeInstantiations
val partialInsts = templateGenerator.manager.partialInstantiations
--
GitLab