diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index f0a0a7def85195c0e2e06cad8b1c06df1d554fcd..32016af41d295e5486506f123e7d801914accc7f 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -457,11 +457,11 @@ trait QuantificationTemplates { self: Templates =>
   }
 
   private class MatcherSet extends BlockedSet[Matcher] {
-    private val keys = new IncrementalSet[MatcherKey]
-    def contains(m: Matcher): Boolean = keys(matcherKey(m))
+    private val keys = new IncrementalSet[(MatcherKey, Seq[Arg])]
+    def contains(m: Matcher): Boolean = keys(matcherKey(m) -> m.args)
 
     override def +=(p: (Set[Encoded], Matcher)): Unit = {
-      keys += matcherKey(p._2)
+      keys += matcherKey(p._2) -> p._2.args
       super.+=(p)
     }
 
diff --git a/src/main/scala/inox/utils/IncrementalSet.scala b/src/main/scala/inox/utils/IncrementalSet.scala
index ae329af5dc3d93dc8eeeaa867adf2a9d95756ece..8bbdf40f26309f00b6719656b9421cfec94e7038 100644
--- a/src/main/scala/inox/utils/IncrementalSet.scala
+++ b/src/main/scala/inox/utils/IncrementalSet.scala
@@ -13,11 +13,12 @@ class IncrementalSet[A] extends IncrementalState
                         with Builder[A, IncrementalSet[A]] {
 
   private[this] val stack = new Stack[MSet[A]]()
-  override def repr = stack.flatten.toSet
+  override def repr = stack.head.toSet
 
   /** Removes all the elements */
   override def clear(): Unit = {
     stack.clear()
+    push()
   }
 
   /** Removes all the elements and creates a new set */
@@ -28,7 +29,11 @@ class IncrementalSet[A] extends IncrementalState
 
   /** Creates one more set level */
   def push(): Unit = {
-    stack.push(MSet())
+    if (stack.isEmpty) {
+      stack.push(MSet())
+    } else {
+      stack.push(stack.head.clone)
+    }
   }
 
   /** Removes one set level */
@@ -37,16 +42,16 @@ class IncrementalSet[A] extends IncrementalState
   }
 
   /** Returns true if the set contains elem */
-  def apply(elem: A) = repr.contains(elem)
+  def apply(elem: A) = stack.head.contains(elem)
   /** Returns true if the set contains elem */
-  def contains(elem: A) = repr.contains(elem)
+  def contains(elem: A) = stack.head.contains(elem)
 
   /** Returns an iterator over all the elements */
-  def iterator = stack.flatten.iterator
+  def iterator = stack.head.iterator
   /** Add an element to the head set */
   def += (elem: A) = { stack.head += elem; this }
   /** Removes an element from all stacked sets */
-  def -= (elem: A) = { stack.foreach(_ -= elem); this }
+  def -= (elem: A) = { stack.head -= elem; this }
 
   override def newBuilder = new scala.collection.mutable.SetBuilder(Set.empty[A])
   def result = this