diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala index e8f8af4bbd600aa7c127a53ef6a0b6629189a306..ea4bff382d1d20b52ba27823cdf92dbaf62d851c 100644 --- a/src/main/scala/leon/purescala/DefOps.scala +++ b/src/main/scala/leon/purescala/DefOps.scala @@ -556,7 +556,7 @@ object DefOps { case None => if(fdMapFCached(fd).isDefined || p.callGraph.transitiveCallees(fd).exists(fd => fdMapFCached(fd).isDefined)) { duplicateParents(fd) - } else { // Verify that for all + } else { fdMapCache += fd -> None } fdMapCache(fd).getOrElse(fd) @@ -612,7 +612,9 @@ object DefOps { } for(fd <- newP.definedFunctions) { - fd.fullBody = replaceClassDefsUse(fd.fullBody) + if(fdMapCache.getOrElse(fd, None).isDefined) { + fd.fullBody = replaceClassDefsUse(fd.fullBody) + } } (newP, cdMapCache.collect{case (cd, Some(new_cd)) => cd -> new_cd},