diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 69f9b2269fbb89b604b91efeb30c24c6c4d134b6..fda6fb737c635180f3d9e9febf0f4b45cd4a27f3 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -93,8 +93,8 @@ trait Definitions { self: Trees =>
         with Constructors
         with Paths { self0: Symbols =>
 
-    protected[ast] val classes: Map[Identifier, ClassDef]
-    protected[ast] val functions: Map[Identifier, FunDef]
+    val classes: Map[Identifier, ClassDef]
+    val functions: Map[Identifier, FunDef]
 
     private[ast] val trees: self.type = self
     protected val symbols: this.type = this
diff --git a/src/main/scala/inox/grammars/utils/Helpers.scala b/src/main/scala/inox/grammars/utils/Helpers.scala
index 2cc09813127ce1539fd7b0089b2d2f4994e07c07..24a689970e7ebbd9e2200bfb3ace4d82044ead1c 100644
--- a/src/main/scala/inox/grammars/utils/Helpers.scala
+++ b/src/main/scala/inox/grammars/utils/Helpers.scala
@@ -103,9 +103,5 @@ trait Helpers { self: GrammarsUniverse =>
    *  - all functions in main units
    *  - all functions imported, or methods of classes imported
    */
-  def functionsAvailable(p: Program): Set[FunDef]// = {
-  //  visibleFunDefsFromMain(p)
-  //}
-
-
+  def functionsAvailable(p: Program): Set[p.trees.FunDef] = p.symbols.functions.values.toSet
 }
diff --git a/src/main/scala/inox/solvers/EnumerationSolver.scala b/src/main/scala/inox/solvers/EnumerationSolver.scala
index 1863547a872fbb3f3ff62a1a56c96c078dd87d42..51a7b7db089db80e5bd4c401dd3f73769b1dba99 100644
--- a/src/main/scala/inox/solvers/EnumerationSolver.scala
+++ b/src/main/scala/inox/solvers/EnumerationSolver.scala
@@ -59,7 +59,6 @@ trait EnumerationSolver extends Solver { self =>
         val evaluator: DeterministicEvaluator { val program: self.program.type } = self.evaluator
         val grammar: grammars.ExpressionGrammar = grammars.ValueGrammar
         val program: self.program.type = self.program
-        def functionsAvailable(p: Program): Set[FunDef] = Set()
       })
 
       if (interrupted) {
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 392898a0590402b65e8df1badf413b25c6312314..1d6b48f41851aad983316dd0b14d5e9b174f61ce 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -3,6 +3,8 @@
 package inox
 package solvers
 
+import inox.grammars.GrammarsUniverse
+
 trait SolverFactory {
   val program: Program
 
@@ -38,7 +40,8 @@ object SolverFactory {
     "nativez3" -> "Native Z3 with z3-templates for unrolling (default)",
     "unrollz3" -> "Native Z3 with leon-templates for unrolling",
     "smt-cvc4" -> "CVC4 through SMT-LIB",
-    "smt-z3"   -> "Z3 through SMT-LIB"
+    "smt-z3"   -> "Z3 through SMT-LIB",
+    "enum"     -> "Enumeration-based counter-example finder"
   )
 
   def getFromName(name: String)
@@ -88,6 +91,16 @@ object SolverFactory {
       } with smtlib.Z3Solver
     })
 
+    case "enum" => create(p)(name, () => new {
+      val program: p.type = p
+      val options = opts
+    } with EnumerationSolver with TimeoutSolver {
+      val evaluator = ev
+      val grammars: GrammarsUniverse {val program: p.type} = new GrammarsUniverse {
+        val program: p.type = p
+      }
+    })
+
     case _ => throw FatalError("Unknown solver: " + name)
   }