diff --git a/src/main/scala/leon/purescala/Path.scala b/src/main/scala/leon/purescala/Path.scala
index f8a70316e0564aa99b537aa1777492067182e759..0a78f0b6dd7355485f60b9acd88f67cca43f68d0 100644
--- a/src/main/scala/leon/purescala/Path.scala
+++ b/src/main/scala/leon/purescala/Path.scala
@@ -32,11 +32,16 @@ object Path {
 class Path private[purescala](
   private[purescala] val elements: Seq[Either[(Identifier, Expr), Expr]]) extends Printable {
 
+  /** Add a binding to this [[Path]] */
   def withBinding(p: (Identifier, Expr)) = new Path(elements :+ Left(p))
   def withBindings(ps: Iterable[(Identifier, Expr)]) = new Path(elements ++ ps.map(Left(_)))
+  /** Add a condition to this [[Path]] */
   def withCond(e: Expr) = new Path(elements :+ Right(e))
   def withConds(es: Iterable[Expr]) = new Path(elements ++ es.map(Right(_)))
 
+  /** Remove bound variables from this [[Path]]
+    * @param ids the bound variables to remove
+    */
   def --(ids: Set[Identifier]) = new Path(elements.filterNot(_.left.exists(p => ids(p._1))))
 
   /** Appends `that` path at the end of `this` */
@@ -116,7 +121,6 @@ class Path private[purescala](
 
   lazy val bindings: Seq[(Identifier, Expr)] = elements.collect { case Left(p) => p }
   lazy val boundIds = bindings map (_._1)
-  lazy val bindingsAsEqs = bindings map { case (id,e) => Equals(id.toVariable, e) }
   lazy val conditions: Seq[Expr] = elements.collect { case Right(e) => e }
 
   def isBound(id: Identifier): Boolean = bindings.exists(p => p._1 == id)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 2a9b113e761d3aa820cd76f3cfb15c0c1ca23791..5e97203c37498c7d74680c9a133af5261066cc67 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -10,7 +10,7 @@ import purescala.Types._
 import purescala.Common._
 import purescala.Constructors._
 import purescala.Extractors._
-import leon.purescala.Definitions.FunDef
+import purescala.Definitions.FunDef
 import Witnesses._
 
 /** Defines a synthesis triple of the form:
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 17a4c0d072c1d9a86156371565e812f11ec89314..7faa06871bc54ee5d305a2faf14563a279923e29 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -45,7 +45,7 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
 
     val facts: Set[Fact] = {
       val TopLevelAnds(fromPhi) = p.phi
-      (fromPhi.toSet ++ p.pc.conditions ++ p.pc.bindingsAsEqs) flatMap getFacts
+      (fromPhi.toSet ++ p.pc.conditions ++ p.pc.bindings.map { case (id,e) => Equals(id.toVariable, e) }) flatMap getFacts
     }
 
     val candidates =