Skip to content
Snippets Groups Projects
Commit 3f1a23c0 authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

Small fix to DualEvaluator

parent 827d8f01
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
......@@ -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 _ =>
......
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment