diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 3e716313b9a171542bf3540eef7b41c4359cb03a..c374d664a60e7cb644ec668d0d2dc90c40c6321a 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -78,6 +78,12 @@ object DefOps {
     }
   }
 
+  def visibleFunDefsFromMain(p: Program): Set[FunDef] = {
+    p.units.filter(_.isMainUnit).toSet.flatMap{ (u: UnitDef) =>
+      visibleFunDefsFrom(u) ++ u.definedFunctions
+    }
+  }
+
   /** Returns true for strict superpackage */ 
   def isSuperPackageOf(p1:PackageRef, p2 : PackageRef) = 
     (p2.length > p1.length) && 
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index d903334843456d2c46ceeddc348450784e0bf29a..e4273dd852ea28638049284af5cb28c1da2cc14a 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -5,10 +5,11 @@ package termination
 
 import purescala.Definitions._
 import purescala.Trees._
+import purescala.DefOps._
 
 abstract class TerminationChecker(val context: LeonContext, val program: Program) extends LeonComponent {
 
-  val functions = program.definedFunctions.toSet
+  val functions = visibleFunDefsFromMain(program)
 
   def initialize() : Unit
   def terminates(funDef : FunDef) : TerminationGuarantee
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index 727f9dda41e55491633b591480ba0a6632ff92f3..eeba3a0ad0bd3eb2a6444bd7842f065df69c6fae 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -4,6 +4,7 @@ package leon
 package termination
 
 import purescala.Definitions._
+import purescala.DefOps._
 
 object TerminationPhase extends LeonPhase[Program,TerminationReport] {
   val name = "Termination"
@@ -17,7 +18,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
 
     tc.initialize()
 
-    val results = program.definedFunctions.toList.sortWith(_.getPos < _.getPos).map { funDef =>
+    val results = visibleFunDefsFromMain(program).toList.sortWith(_.getPos < _.getPos).map { funDef =>
       (funDef -> tc.terminates(funDef))
     }
     val endTime = System.currentTimeMillis
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index bc203c2b817a738baa20e41056ed85d3e0132621..2234f9ff363ef6856598e2920501a52fc2eb84ee 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -38,11 +38,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
   }
 
   private def mkCall(name : String, args : Expr*)(implicit p : Program) = {
-    p.definedFunctions.foreach { fd =>
-      println(fullName(fd))
-    }
-
-    val fn = s"<empty>.Program.$name"
+    val fn = s"Program.$name"
 
     searchByFullName(fn, p) match {
       case Some(fd: FunDef) =>