From 064fa2a048134dd767b266f6c87e3fc657ff2bb3 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 23 Apr 2016 02:33:20 +0200
Subject: [PATCH] Small fix to termination checker for NoGuarantee cases
---
.../leon/termination/ProcessingPipeline.scala | 16 ++++++++--------
1 file changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala
index 30cc87f55..4c979cadc 100644
--- a/src/main/scala/leon/termination/ProcessingPipeline.scala
+++ b/src/main/scala/leon/termination/ProcessingPipeline.scala
@@ -86,15 +86,15 @@ abstract class ProcessingPipeline(context: LeonContext, initProgram: Program) ex
private val unsolved : MutableSet[Problem] = MutableSet.empty
private val dependencies : MutableSet[Problem] = MutableSet.empty
- def isProblem(fd: FunDef): Boolean =
+ def isProblem(fd: FunDef): Boolean = {
+ lazy val callees = program.callGraph.transitiveCallees(fd)
+ lazy val problemDefs = problems.flatMap(_._1.funDefs).toSet
unsolved.exists(_.contains(fd)) ||
- dependencies.exists(_.contains(fd)) || {
- val problemDefs = problems.flatMap(_._1.funDefs).toSet
- problemDefs(fd) || {
- val callees = program.callGraph.transitiveCallees(fd)
- (problemDefs intersect callees).nonEmpty
- }
- }
+ dependencies.exists(_.contains(fd)) ||
+ unsolved.exists(_.funDefs exists callees) ||
+ dependencies.exists(_.funDefs exists callees) ||
+ problemDefs(fd) || (problemDefs intersect callees).nonEmpty
+ }
private def printQueue() {
val sb = new StringBuilder()
--
GitLab