diff --git a/src/main/scala/org/kframework/kale/SubstitutionApply.scala b/src/main/scala/org/kframework/kale/SubstitutionApply.scala
index 6ddcd97..4881621 100644
--- a/src/main/scala/org/kframework/kale/SubstitutionApply.scala
+++ b/src/main/scala/org/kframework/kale/SubstitutionApply.scala
@@ -1,6 +1,7 @@
 package org.kframework.kale
 
 import org.kframework.kale.transformer.Unary
+import org.kframework.kale.transformer.Unary.Apply
 
 object Var {
   def apply(solver: SubstitutionApply)(v: Variable): Term = solver.substitution.get(v).getOrElse(v)
@@ -13,9 +14,14 @@ class SubstitutionApply(val substitution: Substitution)(implicit penv: Environme
   def ExistsSub(solver: SubstitutionApply)(v: Exists): Term =
     substitutionMaker(solver.substitution.remove(v.v))(v.p)
 
+  def HLPF(solver: SubstitutionApply)(t: FreeNode1): Term = {
+    t.copy(solver(t._1))
+  }
+
   override def processingFunctions = definePartialFunction[Term, this.type]({
     case `Variable` => Var.apply _
     case Exists => ExistsSub _
+    case l: HasLabelPredicateFunction => HLPF _
   }) orElse env.unaryProcessingFunctions
 
   override def apply(t: Term): Term = {
diff --git a/src/main/scala/org/kframework/kale/builtin/MAP.scala b/src/main/scala/org/kframework/kale/builtin/MAP.scala
index 2758a62..a216532 100644
--- a/src/main/scala/org/kframework/kale/builtin/MAP.scala
+++ b/src/main/scala/org/kframework/kale/builtin/MAP.scala
@@ -99,7 +99,10 @@ trait MapMixin extends Mixin {
 
 }
 
-case class MapLabel(name: String, indexFunction: Term => Term, identity: Term)(implicit val env: Environment) extends NonPrimitiveMonoidLabel with Constructor {
+case class MapLabel(name: String, indexFunction: Term => Term, identity: Term)
+                   (implicit val env: Environment)
+  extends NonPrimitiveMonoidLabel with Constructor {
+
   override val isPredicate: Option[Boolean] = Some(false)
 
   def isIndexable(t: Term) =
diff --git a/src/main/scala/org/kframework/kale/builtin/SET.scala b/src/main/scala/org/kframework/kale/builtin/SET.scala
index c5b43ac..d000975 100644
--- a/src/main/scala/org/kframework/kale/builtin/SET.scala
+++ b/src/main/scala/org/kframework/kale/builtin/SET.scala
@@ -4,7 +4,10 @@ import org.kframework.kale._
 
 import scala.collection.{Iterable, Set}
 
-case class SetLabel(name: String, identity: Term)(implicit val env: Environment with BooleanMixin) extends NonPrimitiveMonoidLabel with Constructor {
+case class SetLabel(name: String, identity: Term)
+                   (implicit val env: Environment with BooleanMixin)
+  extends NonPrimitiveMonoidLabel with Constructor {
+
   override val isPredicate: Option[Boolean] = Some(false)
 
   override def construct(l: Iterable[Term]): Term = SET(this, l.toSet)
diff --git a/src/main/scala/org/kframework/kale/context/pattern.scala b/src/main/scala/org/kframework/kale/context/pattern.scala
index febc5e1..e912261 100644
--- a/src/main/scala/org/kframework/kale/context/pattern.scala
+++ b/src/main/scala/org/kframework/kale/context/pattern.scala
@@ -12,7 +12,8 @@ import scala.collection.Set
 trait PatternContextMixin extends Mixin {
   _: Environment with standard.MatchingLogicMixin with HasMatcher with HolesMixin =>
 
-  case class PatternContextApplicationLabel(name: String)(implicit val env: Environment with standard.MatchingLogicMixin)
+  case class PatternContextApplicationLabel(name: String)
+                                           (implicit val env: Environment with standard.MatchingLogicMixin)
     extends Context1ApplicationLabel with CluelessRoaring {
 
     //  val C = env.Variable("GENERIC_CONTEXT_VAR")
diff --git a/src/main/scala/org/kframework/kale/function.scala b/src/main/scala/org/kframework/kale/function.scala
index 8c168b1..153de7e 100644
--- a/src/main/scala/org/kframework/kale/function.scala
+++ b/src/main/scala/org/kframework/kale/function.scala
@@ -3,9 +3,6 @@ package org.kframework.kale
 import cats.Monoid
 import org.kframework.kale.highcats._
 import org.kframework.kale.standard.AssocWithIdList
-import org.roaringbitmap.RoaringBitmap
-
-import scala.annotation.switch
 
 trait FunctionLabel extends NodeLabel with CluelessRoaring {
   val name: String
@@ -17,6 +14,12 @@ trait PureFunctionLabel {
   override lazy val isPredicate = Some(false)
 }
 
+trait PredicateFunctionLabel {
+  self: FunctionLabel =>
+
+  override lazy val isPredicate = Some(true)
+}
+
 trait FunctionLabel0 extends Label0 with FunctionLabel {
   def f(): Option[Term]
 
@@ -37,6 +40,10 @@ trait FunctionLabel2 extends Label2 with FunctionLabel {
   override def apply(_1: Term, _2: Term): Term = env.bottomize(_1, _2) {
     f(_1, _2) getOrElse FreeNode2(this, _1, _2)
   }
+  // testing only
+  def applyBuild(_1: Term, _2: Term): Term = env.bottomize(_1, _2) {
+    FreeNode2(this, _1, _2)
+  }
 }
 
 trait FunctionLabel3 extends Label3 with FunctionLabel {
@@ -55,7 +62,9 @@ trait FunctionLabel4 extends Label4 with FunctionLabel {
   }
 }
 
-case class PrimitiveFunction1[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], primitiveF: A => R)(implicit val env: Environment) extends FunctionLabel1 with PureFunctionLabel {
+case class PrimitiveFunction1[A, R]
+(name: String, aLabel: UpDown[A], rLabel: Up[R], primitiveF: A => R)
+(implicit val env: Environment) extends FunctionLabel1 with PureFunctionLabel {
   def f(_1: Term): Option[Term] = _1 match {
     case aLabel.extract(a) => Some(rLabel.up(primitiveF(a)))
     case _ => None
@@ -67,11 +76,51 @@ object PrimitiveFunction1 {
     PrimitiveFunction1(name, aLabel, aLabel, f)
 }
 
-case class PrimitiveFunction2[A, B, R](name: String, aLabel: UpDown[A], bLabel: UpDown[B], rLabel: Up[R], primitiveF: (A, B) => R)(implicit val env: Environment)
+case class HasLabelPredicateFunction(name: String, label: Label)
+                                    (implicit val env: Environment)
+  extends FunctionLabel1 with PredicateFunctionLabel {
+
+  def f(_1: Term): Option[Term] = {
+    if (_1.label.isInstanceOf[VariableLabel]) {
+      None
+    } else if (_1.label == label) {
+      Some(env.Top)
+    } else _1 match {
+      case v: SymbolicVariable if v.givenLabel == label =>
+        Some(env.Top)
+      case _ =>
+        Some(env.Bottom)
+    }
+  }
+}
+
+case class PredicateFunction1(functionLabel: FunctionLabel1)
+                             (implicit val env: Environment)
+  extends FunctionLabel1 with PredicateFunctionLabel {
+  override def f(_1: Term) = {
+    if (_1.label.isInstanceOf[VariableLabel]) {
+      None
+    } else {
+      functionLabel.f(_1)
+    }
+  }
+
+  override val name = "pred" + functionLabel.name
+}
+
+case class PrimitiveFunction2[A, B, R](name: String,
+                                       aLabel: UpDown[A], bLabel: UpDown[B], rLabel: Up[R],
+                                       primitiveF: (A, B) => R)
+                                      (implicit val env: Environment)
   extends FunctionLabel2 with PureFunctionLabel {
 
   def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
     case (aLabel.extract(a), bLabel.extract(b)) => Some(rLabel.up(primitiveF(a, b)))
+    case (_: SymbolicVariable, bLabel.extract(_))
+         |(aLabel.extract(_), _: SymbolicVariable)
+         | (_: SymbolicVariable, _: SymbolicVariable) =>
+      val newVar: SymbolicVariable = env.SymbolicVariable.freshVariable(rLabel.label)
+      Some(env.And(newVar, env.Equality(newVar, FreeNode2(this, _1, _2))))
     case _ => None
   }
 }
@@ -149,10 +198,12 @@ case class PrimitiveMonoid[O: Monoid : UpDown](name: String)(implicit val env: E
 
 
 object PrimitiveFunction2 {
-  def apply[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], f: (A, A) => R)(implicit env: Environment): PrimitiveFunction2[A, A, R] =
+  def apply[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], f: (A, A) => R)
+                 (implicit env: Environment): PrimitiveFunction2[A, A, R] =
     PrimitiveFunction2(name, aLabel, aLabel, rLabel, f)
 
-  def apply[A](name: String, aLabel: UpDown[A], f: (A, A) => A)(implicit env: Environment): PrimitiveFunction2[A, A, A] =
+  def apply[A](name: String, aLabel: UpDown[A], f: (A, A) => A)
+              (implicit env: Environment): PrimitiveFunction2[A, A, A] =
     PrimitiveFunction2(name, aLabel, aLabel, aLabel, f)
 }
 
diff --git a/src/main/scala/org/kframework/kale/highcats/Free.scala b/src/main/scala/org/kframework/kale/highcats/Free.scala
index 9b7fb8c..be9ac98 100644
--- a/src/main/scala/org/kframework/kale/highcats/Free.scala
+++ b/src/main/scala/org/kframework/kale/highcats/Free.scala
@@ -4,7 +4,7 @@ import cats._
 import cats.implicits._
 import cats.{Apply, Eq}
 import org.kframework.kale.util.LabelNamed
-import org.kframework.kale.{Environment, FreeLabel1, FreeLabel2, FreeLabel3, Term}
+import org.kframework.kale.{Environment, FreeLabel1, FreeLabel2, FreeLabel3, Label, Term}
 
 trait Free {
   _: Environment =>
@@ -21,6 +21,8 @@ trait Free {
         case (a) => a.down[A] map companionObject
       }
       override def up(o: R): Term = apply(split(o))
+
+      override def label: Label = this
     }
 
   def free2[A: UpDown, B: UpDown, R <: Product](companionObject: (A, B) => R) =
@@ -35,6 +37,8 @@ trait Free {
       override def up(o: R) = split(o) match {
         case (a, b) => apply(a, b)
       }
+
+      override def label: Label = this
     }
 
   def free3[A: UpDown, B: UpDown, C: UpDown, R <: Product](companionObject: (A, B, C) => R) =
@@ -51,6 +55,8 @@ trait Free {
           case (a, b, c) => apply(a, b, c)
         }
       }
+
+      override def label: Label = this
     }
 
 }
diff --git a/src/main/scala/org/kframework/kale/highcats/UpDown.scala b/src/main/scala/org/kframework/kale/highcats/UpDown.scala
index dffff21..acc3f68 100644
--- a/src/main/scala/org/kframework/kale/highcats/UpDown.scala
+++ b/src/main/scala/org/kframework/kale/highcats/UpDown.scala
@@ -1,9 +1,10 @@
 package org.kframework.kale.highcats
 
-import org.kframework.kale.{LeafLabel, Term}
+import org.kframework.kale.{Label, LeafLabel, Term}
 
 trait Up[O] {
   def up(o: O): Term
+  def label: Label
 }
 
 trait Down[O] {
@@ -17,12 +18,17 @@ trait Down[O] {
 object UpDown {
   final def apply[O](implicit instance: Up[O]): Up[O] = instance
 
-  final def apply[O](f: O => Term): Up[O] = (o: O) => f(o)
+  final def apply[O](f: O => Term, l: LeafLabel[O]): Up[O] = new Up[O] {
+    override def up(o: O) = f(o)
+    override def label: LeafLabel[O] = l
+  }
 
   final implicit def updownFromLeafLabel[O](implicit l: LeafLabel[O]): UpDown[O] = new UpDown[O] {
     override def down(t: Term) = l.unapply(t)
 
     override def up(o: O) = l.apply(o)
+
+    override def label: LeafLabel[O] = l
   }
 }
 
diff --git a/src/main/scala/org/kframework/kale/highcats/liftedCats.scala b/src/main/scala/org/kframework/kale/highcats/liftedCats.scala
index 9fc024a..915d164 100644
--- a/src/main/scala/org/kframework/kale/highcats/liftedCats.scala
+++ b/src/main/scala/org/kframework/kale/highcats/liftedCats.scala
@@ -4,7 +4,7 @@ import cats._
 import cats.implicits._
 import org.kframework.kale.standard.ReferenceLabel
 import org.kframework.kale.util.LabelNamed
-import org.kframework.kale.{Environment, FunctionLabel, FunctionLabel1, Label1, Label2, Mixin, MonoidLabel, PrimitiveFunction1, PrimitiveFunction2, PrimitiveFunction3, PrimitiveMonoid, Term, highcats}
+import org.kframework.kale.{Environment, FunctionLabel, FunctionLabel1, Label, Label1, Label2, LeafLabel, Mixin, MonoidLabel, PrimitiveFunction1, PrimitiveFunction2, PrimitiveFunction3, PrimitiveMonoid, Term, highcats}
 
 trait Convert[A, B] {
   def convert(a: A): B
@@ -58,16 +58,18 @@ trait LiftedCatsMixin extends Mixin with highcats.Free {
   implicit def upMonoidLabeled[O[_] : MonoidLabeled : Traverse : Applicative : MonoidK, E: UpDown]: UpDown[O[E]] = new UpDown[O[E]] {
     val eUpDown = implicitly[UpDown[E]]
     val fTraverse = implicitly[Traverse[O]]
-    val label = implicitly[MonoidLabeled[O]].monoidLabel
+    val mLabel = implicitly[MonoidLabeled[O]].monoidLabel
     val oMonoid = implicitly[MonoidK[O]].algebra[E]
     val oApplicative = implicitly[Applicative[O]]
 
+    override def label: Label = mLabel
+
     override def up(o: O[E]): Term = {
-      fTraverse.foldMap(o)(eUpDown.up)(label)
+      fTraverse.foldMap(o)(eUpDown.up)(mLabel)
     }
 
     override def down(t: Term): Option[O[E]] = t match {
-      case label.iterable(seq: Iterable[Term]) =>
+      case mLabel.iterable(seq: Iterable[Term]) =>
         def ff(t: Term) = oApplicative.pure(eUpDown.down(t).get)
 
         Some(implicitly[Traverse[scala.List]].foldMap(seq.toList)(ff)(oMonoid))
diff --git a/src/main/scala/org/kframework/kale/matchingLogic.scala b/src/main/scala/org/kframework/kale/matchingLogic.scala
index c96647e..e8fa8cd 100644
--- a/src/main/scala/org/kframework/kale/matchingLogic.scala
+++ b/src/main/scala/org/kframework/kale/matchingLogic.scala
@@ -1,6 +1,6 @@
 package org.kframework.kale
 
-import org.kframework.kale.standard.{MightBeSolved}
+import org.kframework.kale.standard.MightBeSolved
 import org.kframework.kore.implementation.DefaultBuilders
 import org.kframework.{kale, kore}
 
@@ -15,6 +15,7 @@ trait MatchingLogicMixin extends Mixin {
 
   // Labels
   val Variable: VariableLabel
+  val SymbolicVariable: SymbolicVariableLabel
   val And: AndLabel
   val Or: OrLabel
   val Rewrite: RewriteLabel
@@ -79,6 +80,28 @@ trait VariableLabel extends LeafLabel[(Name, Sort)] {
   def apply(name: kale.Name): Variable = apply((name, standard.Sort.K))
 }
 
+trait SymbolicVariableLabel extends LeafLabel[(Name, Sort, Label)] {
+  def apply(name: String, givenLabel: Label): SymbolicVariable =
+    apply((standard.Name(name), standard.Sort.K, givenLabel))
+
+  def apply(name: String, sort: kale.Sort, givenLabel: Label): SymbolicVariable =
+    apply((standard.Name(name), sort, givenLabel))
+
+  def apply(v: (Name, Sort, Label)): SymbolicVariable
+
+  def apply(name: kale.Name, givenLabel: Label): SymbolicVariable =
+    apply((name, standard.Sort.K, givenLabel))
+
+  private var counter = 0
+
+  def freshVariable(givenLabel: Label): SymbolicVariable = {
+    counter += 1
+    generatedVariable(givenLabel, counter)
+  }
+
+  def generatedVariable(givenLabel: Label, count: Int): SymbolicVariable
+}
+
 trait Name extends kore.Name {
   override def toString = str
 }
@@ -108,6 +131,31 @@ trait Variable extends Leaf[(Name, Sort)] with kore.SortedVariable {
   override val variables: Set[Variable] = Set(this)
 }
 
+trait SymbolicVariable extends Leaf[(Name, Sort, Label)] {
+  val name: Name
+  val givenLabel: Label  // TODO: Should use the sort instead.
+
+  val label: SymbolicVariableLabel
+  override val isGround = true
+  override val sort: Sort
+  override lazy val data: (Name, Sort, Label) = (name, sort, givenLabel)
+  override lazy val isPredicate: Boolean = false
+
+  override def toString: String = name.str + (
+    if (sort.name == "K")
+      ""
+    else
+      ":" + sort.name
+    ) + ":" + givenLabel.name
+
+  override def canEqual(o: Any): Boolean = o.isInstanceOf[SymbolicVariable]
+
+  override def equals(o: Any): Boolean = o match {
+    case v: SymbolicVariable => v.name == this.name
+    case _ => false
+  }
+}
+
 trait TruthLabel extends LeafLabel[Boolean] {
   override protected[this] def internalInterpret(s: String): Boolean = s.toBoolean
 }
diff --git a/src/main/scala/org/kframework/kale/standard/ac.scala b/src/main/scala/org/kframework/kale/standard/ac.scala
index e8caa07..4336759 100644
--- a/src/main/scala/org/kframework/kale/standard/ac.scala
+++ b/src/main/scala/org/kframework/kale/standard/ac.scala
@@ -141,7 +141,9 @@ case class CollectionSize(collectionLabel: CollectionLabel)(implicit env: Enviro
   override val isPredicate: Option[Boolean] = Some(false)
 }
 
-private[standard] class MonoidListLabel(val name: String, val identity: Term)(implicit val env: Environment with IntMixin) extends NonPrimitiveMonoidLabel with Constructor {
+private[standard] class MonoidListLabel(val name: String, val identity: Term)
+                                       (implicit val env: Environment with IntMixin)
+  extends NonPrimitiveMonoidLabel with Constructor {
 
   val size = CollectionSize(this)
 
diff --git a/src/main/scala/org/kframework/kale/standard/function.scala b/src/main/scala/org/kframework/kale/standard/function.scala
index be4721b..f2e141c 100644
--- a/src/main/scala/org/kframework/kale/standard/function.scala
+++ b/src/main/scala/org/kframework/kale/standard/function.scala
@@ -83,7 +83,10 @@ trait FunctionDefinedByRewriting extends FunctionLabel with PureFunctionLabel wi
     }
 }
 
-case class FunctionDefinedByRewritingLabel0(name: String)(implicit val env: StandardEnvironment) extends FunctionDefinedByRewriting with FunctionLabel0 {
+case class FunctionDefinedByRewritingLabel0(name: String)
+                                           (implicit val env: StandardEnvironment)
+  extends FunctionDefinedByRewriting with FunctionLabel0 {
+
   def f(): Option[Term] = tryToApply(FreeNode0(this))
 }
 
diff --git a/src/main/scala/org/kframework/kale/standard/matchingLogic.scala b/src/main/scala/org/kframework/kale/standard/matchingLogic.scala
index c346c8c..8902607 100644
--- a/src/main/scala/org/kframework/kale/standard/matchingLogic.scala
+++ b/src/main/scala/org/kframework/kale/standard/matchingLogic.scala
@@ -21,6 +21,7 @@ trait MatchingLogicMixin extends Mixin {
   override val Or: DNFOrLabel = DNFOrLabel()
   override val Not: NotLabel = NotLabel()
   override val Variable: StandardVariableLabel = standard.StandardVariableLabel()
+  override val SymbolicVariable: StandardSymbolicVariableLabel = standard.StandardSymbolicVariableLabel()
   override val Equality: EqualityLabel = standard.StandardEqualityLabel()
 
   override val Exists: ExistsLabel = standard.SimpleExistsLabel()
@@ -195,9 +196,25 @@ private[standard] case class StandardVariableLabel()(implicit override val env:
 
   var counter = 0
 
-  def freshVariable() = {
+  def freshVariable(): Variable = freshVariable(Sort.K)
+
+  def freshVariable(sort: Sort): Variable = {
     counter += 1
-    this ((Name("_" + counter), Sort("K")))
+    this ((Name("_" + counter), sort))
+  }
+
+  override val isPredicate: Option[Boolean] = Some(false)
+}
+
+private[standard] case class StandardSymbolicVariableLabel()(implicit override val env: Environment)
+  extends LabelNamed("#SymbolicVariable") with SymbolicVariableLabel with CluelessRoaring { // TODO: Is is really CluelessRoaring?
+  override def apply(nameSortLabel: (kale.Name, kale.Sort, Label)): SymbolicVariable =
+    StandardSymbolicVariable(nameSortLabel._1, nameSortLabel._2, nameSortLabel._3)
+
+  override protected[this] def internalInterpret(s: String): (kale.Name, kale.Sort, Label) = ???
+
+  override def generatedVariable(givenLabel: Label, counter: Int): SymbolicVariable = {
+    this ((Name("_" + counter), Sort("K"), givenLabel))
   }
 
   override val isPredicate: Option[Boolean] = Some(false)
@@ -209,7 +226,20 @@ private[standard] case class StandardVariable(name: kale.Name, givenSort: kale.S
   val label = env.Variable
 }
 
-private[standard] case class StandardTruthLabel()(implicit val env: Environment) extends NameFromObject with TruthLabel with RoaringLabelsFromTerm {
+private[standard] case class StandardSymbolicVariable(override val name: kale.Name,
+                                                      givenSort: kale.Sort,
+                                                      override val givenLabel: Label)
+                                                     (implicit env: Environment)
+  extends SymbolicVariable with kore.Variable {
+
+  override lazy val sort: kale.Sort = givenSort
+  override val label: SymbolicVariableLabel = env.SymbolicVariable
+}
+
+private[standard] case class StandardTruthLabel()
+                                               (implicit val env: Environment)
+  extends NameFromObject with TruthLabel with RoaringLabelsFromTerm {
+
   def apply(v: Boolean) = if (v) env.Top else env.Bottom
 
   override val isPredicate: Option[Boolean] = Some(true)
@@ -291,7 +321,8 @@ private[kale] class Matches(val _1: Term, val _2: Term)(implicit env: StandardEn
   val label = env.Match
 }
 
-private[standard] case class StandardEqualityLabel()(implicit override val env: Environment with MatchingLogicMixin) extends LabelNamed("=") with EqualityLabel {
+private[standard] case class StandardEqualityLabel()(implicit override val env: Environment with MatchingLogicMixin)
+  extends LabelNamed("=") with EqualityLabel {
   override def apply(_1: Term, _2: Term): Term = {
     val lhsOrElements = env.Or.asSet(_1)
     val rhsOrElements = env.Or.asSet(_2)
@@ -307,7 +338,7 @@ private[standard] case class StandardEqualityLabel()(implicit override val env:
     if (_1 == _2)
       env.Top
     else if (_1.isGround && _2.isGround) {
-      if (env.isSealed) {
+      if (env.isSealed && !_1.isInstanceOf[SymbolicVariable] && !_2.isInstanceOf[SymbolicVariable]) {
         env.And.onlyPredicate(env.unify(_1, _2))
       } else
         new Equals(_1, _2)
diff --git a/src/main/scala/org/kframework/km/rewrite.scala b/src/main/scala/org/kframework/km/rewrite.scala
index 8f964fe..c6dca9b 100644
--- a/src/main/scala/org/kframework/km/rewrite.scala
+++ b/src/main/scala/org/kframework/km/rewrite.scala
@@ -11,7 +11,8 @@ class rewrite(val symbols: Seq[Seq[term.Symbol]]) {
 
   val z3 = new z3(symbols)
 
-  def applyRule(rule: SimpleRewrite, term: SimplePattern): Seq[SimplePattern] = { val cntRename = term.counter + 1
+  def applyRule(rule: SimpleRewrite, term: SimplePattern): Seq[SimplePattern] = {
+    val cntRename = term.counter + 1
     // rule:  l => r if c
     lazy val l = rule.l.rename(cntRename)
     lazy val r = rule.r.rename(cntRename)
diff --git a/src/main/scala/org/kframework/km/z3.scala b/src/main/scala/org/kframework/km/z3.scala
index 2d368d9..0332f4f 100644
--- a/src/main/scala/org/kframework/km/z3.scala
+++ b/src/main/scala/org/kframework/km/z3.scala
@@ -87,7 +87,7 @@ class z3(val symbolsSeq: Seq[Seq[term.Symbol]]) {
 object z3 {
 
   // TODO: set proper z3 path
-  private val z3 = "./z3/bin/z3" // "z3-4.5.0-x64-osx-10.11.6/bin/z3"
+  private val z3 = "/home/virgil/runtime-verification/z3/build/z3" // "/usr/bin/z3" // "./z3/bin/z3" // "z3-4.5.0-x64-osx-10.11.6/bin/z3"
 
   val cmd = Seq(z3, "-smt2", "-in")
 
diff --git a/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala b/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala
new file mode 100644
index 0000000..daa5408
--- /dev/null
+++ b/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala
@@ -0,0 +1,134 @@
+package org.kframework.kale.symbolic
+
+import org.kframework.kale
+import org.kframework.kale.standard.{NotLabel, Sort, StandardEnvironment, StandardSymbolicVariable}
+import org.kframework.kale.{AndLabel, Environment, EqualityLabel, FreeNode1, HasLabelPredicateFunction, IMPCommonSignature, Label, NonPrimitiveMonoidLabel, RewriteLabel, Rewriter, SymbolicVariableLabel, Term, VariableLabel}
+import org.scalatest.{FlatSpec, Matchers}
+
+import scala.collection.Seq
+
+class IntegrationTest extends FlatSpec with Matchers {
+
+  val intSort = Sort("Int")
+
+  trait ABitOfSortingSortingMixin extends Environment {
+    def sort(l: Label, children: Seq[Term]): kale.Sort = sort(l)
+
+    def sort(l: Label): Sort = l match {
+      case INT.Int => intSort
+      case INT.plus => intSort
+      case plus => intSort
+      case _ => Sort.Top
+    }
+
+    override def isSort(left: org.kframework.kore.Sort, term: Term): Boolean =
+      if (left == Sort.Top) {
+        true
+      } else {
+        term.sort == left
+      }
+  }
+
+  private val env: StandardEnvironment = new StandardEnvironment with ABitOfSortingSortingMixin
+  private val signature = new IMPCommonSignature()(env)
+
+  import signature._
+
+  private val Rewrite: RewriteLabel = env.Rewrite
+  private val And: AndLabel = env.And
+  private val Not: NotLabel = env.Not
+  private val Equality: EqualityLabel = env.Equality
+
+  private val INT = env.INT
+  private val Variable = env.Variable
+
+  private val SymbI = Variable("I", intSort)
+  private val I1 = Variable("I1", intSort)
+  private val I2 = Variable("I2", intSort)
+  private val S = Variable("S")
+  private val R = Variable("R")
+  private val kseq: NonPrimitiveMonoidLabel = env.AssocWithIdLabel("_~>_", emptyk())
+
+  "Rewriting" should "match label predicate functions" in {
+
+
+    val rules: Set[Term] = Set(
+      T(k(kseq(
+        Rewrite(
+          plus(I1, I2),
+          INT.plus(I1, I2)),
+        R)), S)
+    ) map (t => Rewrite(lhs(t), rhs(t)))
+
+    env.seal()
+
+    val rewrite = Rewriter(env)(rules)
+
+    val term = T(k(kseq(plus(INT.Int(1), INT.Int(2)))), state(statesMap()))
+
+    val result = rewrite.searchStep(term)
+    result should equal(T(k(kseq(INT.Int(3))), state(statesMap())))
+  }
+
+  "Rewriting" should "use functions over variables." in {
+    val rules: Set[Term] = Set(
+      T(k(kseq(
+        Rewrite(
+          plus(I1, I2),
+          INT.plus(I1, I2)),
+        R)), S)
+    ) map (t => Rewrite(lhs(t), rhs(t)))
+
+    env.seal()
+
+    val rewrite = Rewriter(env)(rules)
+
+    val term = T(k(kseq(plus(INT.Int(1), SymbI))), state(statesMap()))
+
+    val result = rewrite.searchStep(term)
+    val v1 = Variable.freshVariable(intSort)
+    val equalPred = Equality(v1, INT.plus.applyBuild(INT.Int(1), SymbI))
+    // result should equal (And(T(k(kseq(v1)), state(statesMap())), equalPred)
+//    result should equal(T(k(kseq(And(v1, equalPred))), state(statesMap())))
+    result should equal(T(k(INT.plus(INT.Int(1), SymbI)), state(statesMap())))
+  }
+
+  "Rewriting" should "evaluate complex expressions with variables." in {
+
+    val rules: Set[Term] = Set(
+      /*
+      T(k(kseq(
+        Rewrite(
+          plus(And(I1, isInt(I1)), And(I2, isInt(I2))),
+          INT.plus(I1, I2)),
+        R)), S),
+      */
+      T(k(kseq(
+        Rewrite(
+          plus(I1, I2),
+          kseq(I2, plus(I1, env.Hole))),
+        R)), S),
+      /*
+      T(k(kseq(
+        Rewrite(
+          kseq(And(I2, isInt(I2)), plus(I1, env.Hole)),
+          kseq(plus(I1, I2))),
+        R)), S),
+        */
+    ) map (t => Rewrite(lhs(t), rhs(t)))
+
+    env.seal()
+
+    val rewrite = Rewriter(env)(rules)
+
+    val term = T(k(kseq(plus(INT.Int(1), plus(INT.Int(1), SymbI)))), state(statesMap()))
+    // statesMap(
+
+    val result = rewrite.searchStep(term)
+    // all rules have an implicit forall for all variables wrapping the entire rule
+    // as many variables get bounded, most of the forall dissapear
+    // as the Hole is free, the forall remains and is lowered to the smallest context
+    // hm, not sure if forall is correct here or we should wrap it explicitly into an exists, or maybe leave it free
+    result should equal(T(k(kseq(plus(INT.Int(1), SymbI), plus(INT.Int(1), env.ForAll(env.Hole, env.Hole)))), state(statesMap())))
+  }
+}