diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp
index 1e64ffbc5..b820f4e3e 100644
--- a/Indexing/ClauseCodeTree.cpp
+++ b/Indexing/ClauseCodeTree.cpp
@@ -245,7 +245,7 @@ void ClauseCodeTree::remove(Clause* cl)
     }
 
   iteration_restart:
-    if(!rlm->next()) {
+    if(!rlm->execute()) {
       if(depth==0) {
         ASSERTION_VIOLATION;
         INVALID_OPERATION("clause to be removed was not found");
@@ -286,7 +286,7 @@ void ClauseCodeTree::remove(Clause* cl)
 void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_,
     size_t linfoCnt_, ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_)
 {
-  RemovingMatcher::init(entry_, linfos_, linfoCnt_, tree_, firstsInBlocks_);
+  Matcher::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_);
 
   ALWAYS(prepareLiteral());
 }
@@ -326,10 +326,7 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
 {
   ASS_G(linfoCnt_,0);
 
-  Matcher::init(tree_,entry_);
-
-  linfos=linfos_;
-  linfoCnt=linfoCnt_;
+  Matcher::init(tree_,entry_,linfos_,linfoCnt_);
 
   _eagerlyMatched=false;
   eagerResults.reset();
@@ -341,7 +338,7 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
     //(and those must be at the entry point or its alternatives)
 
     _eagerlyMatched=true;
-    _fresh=false;
+    fresh=false;
     CodeOp* sop=entry;
     while(sop) {
       if(sop->isSuccess()) {
diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp
index 9d1b6df0e..a6eb6298a 100644
--- a/Indexing/ClauseCodeTree.hpp
+++ b/Indexing/ClauseCodeTree.hpp
@@ -55,7 +55,7 @@ class ClauseCodeTree : public CodeTree
   bool removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks);
 
   struct RemovingLiteralMatcher
-  : public RemovingMatcher<false>
+  : public Matcher</*removing*/true,false>
   {
     void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
 	ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
@@ -69,7 +69,7 @@ class ClauseCodeTree : public CodeTree
    *
    * Here the actual execution of the code of the tree takes place */
   struct LiteralMatcher
-  : public Matcher
+  : public Matcher</*removing*/false,false>
   {
     void init(CodeTree* tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess=false);
     bool next();
diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp
index 0c6f0ea6c..b5c139330 100644
--- a/Indexing/CodeTree.cpp
+++ b/Indexing/CodeTree.cpp
@@ -519,7 +519,249 @@ CodeTree::CodeOp*& CodeTree::SearchStructImpl<k>::targetOp(const T& val)
   return targets[left];
 }
 
-inline bool CodeTree::BaseMatcher::doCheckGroundTerm()
+//////////////// Matcher ////////////////////
+
+template<bool removing, bool checkRange>
+bool CodeTree::Matcher<removing, checkRange>::execute()
+{
+  if(fresh) {
+    fresh=false;
+  }
+  else {
+    //we backtrack from what we found in the previous run
+    if(!backtrack()) {
+      return false;
+    }
+  }
+
+  bool shouldBacktrack=false;
+  for(;;) {
+    if(op->alternative()) {
+      if constexpr (removing) {
+        btStack.push(BTPointRemoving(tp, op->alternative(), RemovingBase::firstsInBlocks->size()));
+      } else {
+        btStack.push(BTPoint(tp, op->alternative()));
+      }
+    }
+    switch(op->_instruction()) {
+      case SUCCESS_OR_FAIL:
+        if(op->isFail()) {
+          shouldBacktrack=true;
+          break;
+        }
+        if constexpr (removing) {
+          if (RemovingBase::matchingClauses) {
+            //we can succeed only in certain depth and that will be handled separately
+            shouldBacktrack=true;
+          }
+          else {
+            //we are matching terms in a TermCodeTree
+            return true;
+          }
+        } else {
+          //yield successes only in the first round (we don't want to yield the
+          //same thing for each query literal)
+          if(curLInfo==0) {
+            return true;
+          }
+          else {
+            shouldBacktrack=true;
+          }
+        }
+        break;
+      case LIT_END:
+        if constexpr (removing) {
+          ASS(RemovingBase::matchingClauses);
+        }
+        return true;
+      case CHECK_GROUND_TERM:
+        shouldBacktrack=!doCheckGroundTerm();
+        break;
+      case CHECK_FUN:
+        shouldBacktrack=!doCheckFun();
+        break;
+      case ASSIGN_VAR:
+        if constexpr (removing) {
+          shouldBacktrack=!doAssignVar();
+        } else {
+          doAssignVar();
+        }
+        break;
+      case CHECK_VAR:
+        shouldBacktrack=!doCheckVar();
+        break;
+      case SEARCH_STRUCT:
+        if(doSearchStruct()) {
+          //a new value of @b op is assigned, so restart the loop
+          continue;
+        }
+        else {
+          shouldBacktrack=true;
+        }
+        break;
+    }
+    if(shouldBacktrack) {
+      if(!backtrack()) {
+        return false;
+      }
+      shouldBacktrack=false;
+    }
+    else {
+      //the SEARCH_STRUCT operation does not appear in CodeBlocks
+      ASS(!op->isSearchStruct());
+      //In each CodeBlock there is always either operation LIT_END or FAIL.
+      //As we haven't encountered one yet, we may safely increase the
+      //operation pointer
+      op++;
+    }
+  }
+}
+
+template<bool removing, bool checkRange>
+void CodeTree::Matcher<removing, checkRange>::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack<CodeOp*>* firstsInBlocks_)
+{
+  tree=tree_;
+  entry=entry_;
+
+  linfos=linfos_;
+  linfoCnt=linfoCnt_;
+
+  if constexpr (removing) {
+    RemovingBase::firstsInBlocks=firstsInBlocks_;
+    RemovingBase::initFIBDepth=RemovingBase::firstsInBlocks->size();
+    RemovingBase::matchingClauses=tree->_clauseCodeTree;
+  }
+
+  fresh=true;
+  _matched=false;
+  curLInfo=0;
+
+  bindings.ensure(tree->_maxVarCnt);
+  btStack.reset();
+}
+
+/**
+ * Is called when we need to retrieve a new result.
+ * It does not only backtrack to the next alternative to try,
+ * but if there are no more alternatives, it goes back to the
+ * entry point and starts evaluating new literal info (if there
+ * is some left).
+ */
+template<bool removing, bool checkRange>
+bool CodeTree::Matcher<removing, checkRange>::backtrack()
+{
+  if(btStack.isEmpty()) {
+    curLInfo++;
+    return prepareLiteral();
+  }
+  auto bp=btStack.pop();
+  tp=bp.tp;
+  op=bp.op;
+  if constexpr (removing) {
+    RemovingBase::firstsInBlocks->truncate(bp.fibDepth);
+    RemovingBase::firstsInBlocks->push(op);
+  }
+  return true;
+}
+
+template<bool removing, bool checkRange>
+bool CodeTree::Matcher<removing, checkRange>::prepareLiteral()
+{
+  if constexpr (removing) {
+    RemovingBase::firstsInBlocks->truncate(RemovingBase::initFIBDepth);
+  }
+  if(curLInfo>=linfoCnt) {
+    return false;
+  }
+  ft=linfos[curLInfo].ft;
+  tp=0;
+  op=entry;
+  return true;
+}
+
+template<bool removing, bool checkRange>
+inline bool CodeTree::Matcher<removing, checkRange>::doAssignVar()
+{
+  ASS_EQ(op->_instruction(), ASSIGN_VAR);
+
+  unsigned var=op->_arg();
+  const FlatTerm::Entry* fte=&(*ft)[tp];
+  if(fte->isVar()) {
+    if constexpr (checkRange) {
+      if (!RemovingBase::range.insert(fte->_number())) {
+        return false;
+      }
+    }
+    bindings[var]=TermList::var(fte->_number());
+    tp++;
+  }
+  else {
+    // in the removing case we are looking for variants
+    // and they match only other variables into variables
+    if constexpr (removing) {
+      return false;
+    }
+    ASS(fte->isFun());
+    fte++;
+    ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
+    ASS(fte->_term());
+    bindings[var]=TermList(fte->_term());
+    fte++;
+    ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
+    tp+=fte->_number();
+  }
+  return true;
+}
+
+template<bool removing, bool checkRange>
+inline bool CodeTree::Matcher<removing, checkRange>::doCheckVar()
+{
+  ASS_EQ(op->_instruction(), CHECK_VAR);
+
+  unsigned var=op->_arg();
+  const FlatTerm::Entry* fte=&(*ft)[tp];
+  if (fte->isVar()) {
+    if(bindings[var]!=TermList::var(fte->_number())) {
+      return false;
+    }
+    tp++;
+  }
+  else {
+    // in the removing case we are looking for variants
+    // and they match only other variables into variables
+    if constexpr (removing) {
+      return false;
+    }
+    ASS(fte->isFun());
+    fte++;
+    ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
+    if(bindings[var]!=TermList(fte->_term())) {
+      return false;
+    }
+    fte++;
+    ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
+    tp+=fte->_number();
+  }
+  return true;
+}
+
+template<bool removing, bool checkRange>
+inline bool CodeTree::Matcher<removing, checkRange>::doCheckFun()
+{
+  ASS_EQ(op->_instruction(), CHECK_FUN);
+
+  unsigned functor=op->_arg();
+  FlatTerm::Entry& fte=(*ft)[tp];
+  if(!fte.isFun(functor)) {
+    return false;
+  }
+  fte.expand();
+  tp+=FlatTerm::FUNCTION_ENTRY_COUNT;
+  return true;
+}
+
+template<bool removing, bool checkRange>
+inline bool CodeTree::Matcher<removing, checkRange>::doCheckGroundTerm()
 {
   ASS_EQ(op->_instruction(), CHECK_GROUND_TERM);
 
@@ -542,6 +784,27 @@ inline bool CodeTree::BaseMatcher::doCheckGroundTerm()
   return true;
 }
 
+template<bool removing, bool checkRange>
+inline bool CodeTree::Matcher<removing, checkRange>::doSearchStruct()
+{
+  ASS_EQ(op->_instruction(), SEARCH_STRUCT);
+
+  const FlatTerm::Entry* fte=&(*ft)[tp];
+  CodeOp* target=op->getSearchStruct()->getTargetOp(fte);
+  if(!target) {
+    return false;
+  }
+  op=target;
+  if constexpr (removing) {
+    RemovingBase::firstsInBlocks->push(op);
+  }
+  return true;
+}
+
+template struct CodeTree::Matcher<true, false>;
+template struct CodeTree::Matcher<true, true>;
+template struct CodeTree::Matcher<false, false>;
+
 //////////////// auxiliary ////////////////////
 
 CodeTree::CodeTree()
@@ -1147,201 +1410,6 @@ void CodeTree::optimizeMemoryAfterRemoval(Stack<CodeOp*>* firstsInBlocks, CodeOp
   }
 }
 
-template<bool checkRange>
-void CodeTree::RemovingMatcher<checkRange>::init(CodeOp* entry_, LitInfo* linfos_,
-    size_t linfoCnt_, CodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_)
-{
-  fresh=true;
-  entry=entry_;
-  linfos=linfos_;
-  linfoCnt=linfoCnt_;
-  tree=tree_;
-  firstsInBlocks=firstsInBlocks_;
-
-  initFIBDepth=firstsInBlocks->size();
-
-  matchingClauses=tree->_clauseCodeTree;
-  bindings.ensure(tree->_maxVarCnt);
-  btStack.reset();
-  range.reset();
-
-  curLInfo=0;
-}
-
-template<bool checkRange>
-bool CodeTree::RemovingMatcher<checkRange>::next()
-{
-  if(fresh) {
-    fresh=false;
-  }
-  else {
-    //we backtrack from what we found in the previous run
-    if(!backtrack()) {
-      return false;
-    }
-  }
-
-
-  bool shouldBacktrack=false;
-  for(;;) {
-    if(op->alternative()) {
-      btStack.push(BTPoint(tp, op->alternative(), firstsInBlocks->size()));
-    }
-    switch(op->_instruction()) {
-      case SUCCESS_OR_FAIL:
-        if(op->isFail()) {
-          shouldBacktrack=true;
-          break;
-        }
-        if(matchingClauses) {
-          //we can succeed only in certain depth and that will be handled separately
-          shouldBacktrack=true;
-        }
-        else {
-          //we are matching terms in a TermCodeTree
-          return true;
-        }
-        break;
-      case LIT_END:
-        ASS(matchingClauses);
-        return true;
-      case CHECK_GROUND_TERM:
-        shouldBacktrack=!doCheckGroundTerm();
-        break;
-      case CHECK_FUN:
-        shouldBacktrack=!doCheckFun();
-        break;
-      case ASSIGN_VAR:
-        shouldBacktrack=!doAssignVar();
-        break;
-      case CHECK_VAR:
-        shouldBacktrack=!doCheckVar();
-        break;
-      case SEARCH_STRUCT:
-        if(doSearchStruct()) {
-          //a new value of @b op is assigned, so restart the loop
-          continue;
-        }
-        else {
-          shouldBacktrack=true;
-        }
-        break;
-    }
-    if(shouldBacktrack) {
-      if(!backtrack()) {
-        return false;
-      }
-      // dead store, left here in case it should have been a static?
-      // shouldBacktrack = false;
-    }
-    else {
-      //the SEARCH_STRUCT operation does not appear in CodeBlocks
-      ASS(!op->isSearchStruct());
-      //In each CodeBlock there is always either operation LIT_END or FAIL.
-      //As we haven't encountered one yet, we may safely increase the
-      //operation pointer
-      op++;
-    }
-  }
-}
-
-template<bool checkRange>
-bool CodeTree::RemovingMatcher<checkRange>::backtrack()
-{
-  if(btStack.isEmpty()) {
-    curLInfo++;
-    return prepareLiteral();
-  }
-  BTPoint bp=btStack.pop();
-  tp=bp.tp;
-  op=bp.op;
-  firstsInBlocks->truncate(bp.fibDepth);
-  firstsInBlocks->push(op);
-  return true;
-}
-
-template<bool checkRange>
-bool CodeTree::RemovingMatcher<checkRange>::prepareLiteral()
-{
-  firstsInBlocks->truncate(initFIBDepth);
-  if(curLInfo>=linfoCnt) {
-    return false;
-  }
-  ft=linfos[curLInfo].ft;
-  tp=0;
-  op=entry;
-  return true;
-}
-
-template<bool checkRange>
-inline bool CodeTree::RemovingMatcher<checkRange>::doSearchStruct()
-{
-  ASS_EQ(op->_instruction(), SEARCH_STRUCT);
-
-  const FlatTerm::Entry* fte=&(*ft)[tp];
-  CodeOp* target=op->getSearchStruct()->getTargetOp(fte);
-  if(!target) {
-    return false;
-  }
-  op=target;
-  firstsInBlocks->push(op);
-  return true;
-}
-
-template<bool checkRange>
-inline bool CodeTree::RemovingMatcher<checkRange>::doCheckFun()
-{
-  ASS_EQ(op->_instruction(), CHECK_FUN);
-
-  unsigned functor=op->_arg();
-  FlatTerm::Entry& fte=(*ft)[tp];
-  if(!fte.isFun(functor)) {
-    return false;
-  }
-  fte.expand();
-  tp+=FlatTerm::FUNCTION_ENTRY_COUNT;
-  return true;
-}
-
-template<bool checkRange>
-inline bool CodeTree::RemovingMatcher<checkRange>::doAssignVar()
-{
-  ASS_EQ(op->_instruction(), ASSIGN_VAR);
-
-  //we are looking for variants and they match only other variables into variables
-  unsigned var=op->_arg();
-  const FlatTerm::Entry* fte=&(*ft)[tp];
-  if(fte->_tag()!=FlatTerm::VAR) {
-    return false;
-  }
-  bindings[var]=fte->_number();
-  if constexpr (checkRange) {
-    if (!range.insert(fte->_number())) {
-      return false;
-    }
-  }
-  tp++;
-  return true;
-}
-
-template<bool checkRange>
-inline bool CodeTree::RemovingMatcher<checkRange>::doCheckVar()
-{
-  ASS_EQ(op->_instruction(), CHECK_VAR);
-
-  //we are looking for variants and they match only other variables into variables
-  unsigned var=op->_arg();
-  const FlatTerm::Entry* fte=&(*ft)[tp];
-  if(fte->_tag()!=FlatTerm::VAR || bindings[var]!=fte->_number()) {
-    return false;
-  }
-  tp++;
-  return true;
-}
-
-template struct CodeTree::RemovingMatcher<false>;
-template struct CodeTree::RemovingMatcher<true>;
-
 //////////////// retrieval ////////////////////
 
 void CodeTree::incTimeStamp()
@@ -1353,191 +1421,4 @@ void CodeTree::incTimeStamp()
   }
 }
 
-void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entry_)
-{
-  tree=tree_;
-  entry=entry_;
-
-  _fresh=true;
-  _matched=false;
-  curLInfo=0;
-  btStack.reset();
-  bindings.ensure(tree->_maxVarCnt);
-}
-
-bool CodeTree::Matcher::execute()
-{
-  if(_fresh) {
-    _fresh=false;
-  }
-  else {
-    //we backtrack from what we found in the previous run
-    if(!backtrack()) {
-      return false;
-    }
-  }
-
-
-  bool shouldBacktrack=false;
-  for(;;) {
-    if(op->alternative()) {
-      btStack.push(BTPoint(tp, op->alternative()));
-    }
-    switch(op->_instruction()) {
-      case SUCCESS_OR_FAIL:
-        if(op->isFail()) {
-          shouldBacktrack=true;
-          break;
-        }
-        //yield successes only in the first round (we don't want to yield the
-        //same thing for each query literal)
-        if(curLInfo==0) {
-          return true;
-        }
-        else {
-          shouldBacktrack=true;
-        }
-        break;
-      case LIT_END:
-        return true;
-      case CHECK_GROUND_TERM:
-        shouldBacktrack=!doCheckGroundTerm();
-        break;
-      case CHECK_FUN:
-        shouldBacktrack=!doCheckFun();
-        break;
-      case ASSIGN_VAR:
-        doAssignVar();
-        break;
-      case CHECK_VAR:
-        shouldBacktrack=!doCheckVar();
-        break;
-      case SEARCH_STRUCT:
-        if(doSearchStruct()) {
-          //a new value of @b op is assigned, so restart the loop
-          continue;
-        }
-        else {
-          shouldBacktrack=true;
-        }
-        break;
-    }
-    if(shouldBacktrack) {
-      if(!backtrack()) {
-	return false;
-      }
-      shouldBacktrack=false;
-    }
-    else {
-      //the SEARCH_STRUCT operation does not appear in CodeBlocks
-      ASS(!op->isSearchStruct());
-      //In each CodeBlock there is always either operation LIT_END or FAIL.
-      //As we haven't encountered one yet, we may safely increase the
-      //operation pointer
-      op++;
-    }
-  }
-}
-
-/**
- * Is called when we need to retrieve a new result.
- * It does not only backtrack to the next alternative to try,
- * but if there are no more alternatives, it goes back to the
- * entry point and starts evaluating new literal info (if there
- * is some left).
- */
-bool CodeTree::Matcher::backtrack()
-{
-  if(btStack.isEmpty()) {
-    curLInfo++;
-    return prepareLiteral();
-  }
-  BTPoint bp=btStack.pop();
-  tp=bp.tp;
-  op=bp.op;
-  return true;
-}
-
-bool CodeTree::Matcher::prepareLiteral()
-{
-  if(curLInfo>=linfoCnt) {
-    return false;
-  }
-  tp=0;
-  op=entry;
-  ft=linfos[curLInfo].ft;
-  return true;
-}
-
-inline bool CodeTree::Matcher::doSearchStruct()
-{
-  ASS_EQ(op->_instruction(), SEARCH_STRUCT);
-
-  const FlatTerm::Entry* fte=&(*ft)[tp];
-  op=op->getSearchStruct()->getTargetOp(fte);
-  return op;
-}
-
-inline bool CodeTree::Matcher::doCheckFun()
-{
-  ASS_EQ(op->_instruction(), CHECK_FUN);
-
-  unsigned functor=op->_arg();
-  FlatTerm::Entry& fte=(*ft)[tp];
-  if(!fte.isFun(functor)) {
-    return false;
-  }
-  fte.expand();
-  tp+=FlatTerm::FUNCTION_ENTRY_COUNT;
-  return true;
-}
-
-inline void CodeTree::Matcher::doAssignVar()
-{
-  ASS_EQ(op->_instruction(), ASSIGN_VAR);
-
-  unsigned var=op->_arg();
-  const FlatTerm::Entry* fte=&(*ft)[tp];
-  if(fte->_tag()==FlatTerm::VAR) {
-    bindings[var]=TermList(fte->_number(),false);
-    tp++;
-  }
-  else {
-    ASS(fte->isFun());
-    fte++;
-    ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
-    ASS(fte->_term());
-    bindings[var]=TermList(fte->_term());
-    fte++;
-    ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
-    tp+=fte->_number();
-  }
-}
-
-inline bool CodeTree::Matcher::doCheckVar()
-{
-  ASS_EQ(op->_instruction(), CHECK_VAR);
-
-  unsigned var=op->_arg();
-  const FlatTerm::Entry* fte=&(*ft)[tp];
-  if(fte->_tag()==FlatTerm::VAR) {
-    if(bindings[var]!=TermList(fte->_number(),false)) {
-      return false;
-    }
-    tp++;
-  }
-  else {
-    ASS(fte->isFun());
-    fte++;
-    ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
-    if(bindings[var]!=TermList(fte->_term())) {
-      return false;
-    }
-    fte++;
-    ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
-    tp+=fte->_number();
-  }
-  return true;
-}
-
 }
diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp
index d68f08a57..58ab1e56c 100644
--- a/Indexing/CodeTree.hpp
+++ b/Indexing/CodeTree.hpp
@@ -196,7 +196,7 @@ class CodeTree
       return _data<Term>();
     }
 
-    template<class T> inline T* getSuccessResult() { ASS(isSuccess()); return _data<T>(); }
+    template<class T> inline T* getSuccessResult() const { ASS(isSuccess()); return _data<T>(); }
 
     inline ILStruct* getILS() { ASS(isLitEnd()); return _data<ILStruct>(); }
     inline const ILStruct* getILS() const { return _data<ILStruct>(); }
@@ -303,10 +303,66 @@ class CodeTree
 
   typedef Vector<CodeOp> CodeBlock;
   typedef Stack<CodeOp> CodeStack;
+  typedef DArray<TermList> BindingArray;
+
+  // This holds the parts relevant only for Matcher<true,...>
+  struct RemovingBase {
+    Stack<CodeOp*>* firstsInBlocks;
+    size_t initFIBDepth;
+    bool matchingClauses;
+    DHSet<unsigned> range;
+  };
 
-  struct BaseMatcher
+  struct NonRemovingBase {};
+
+  /**
+   * Context for finding matches of literals
+   *
+   * Here the actual execution of the code of the tree takes place.
+   *
+   * The object is not initialized not only by constructor, but also by
+   * a call to the @b init function (inheritors should implement their
+   * own @b init function (possibly with other arguments) that will call
+   * this one. After use, the @b deinit function should be called (if
+   * present). This allows for reuse of a single object.
+   */
+  template<bool removing, bool checkRange>
+  struct Matcher
+    : public std::conditional<removing, RemovingBase, NonRemovingBase>::type
   {
-  public:
+    // we only want to enable checkRange if
+    // removing, which works on variables
+    static_assert(removing || !checkRange);
+
+    /**
+     * Backtracking point for the interpretation of the code tree.
+     */
+    struct BTPoint
+    {
+      BTPoint(size_t tp, CodeOp* op) : tp(tp), op(op) {}
+
+      /** Position in the flat term */
+      size_t tp;
+      /** Pointer to the next operation */
+      CodeOp* op;
+    };
+
+    struct BTPointRemoving
+    {
+      BTPointRemoving(size_t tp, CodeOp* op, size_t fibDepth)
+      : tp(tp), op(op), fibDepth(fibDepth) {}
+
+      size_t tp;
+      CodeOp* op;
+      size_t fibDepth;
+    };
+
+    inline bool finished() const { return !fresh && !_matched; }
+    inline bool matched() const { return _matched && op->isLitEnd(); }
+    inline bool success() const { return _matched && op->isSuccess(); }
+
+    bool execute();
+
     /**
      * Pointer to the current operation
      *
@@ -314,9 +370,30 @@ class CodeTree
      * a call to the @b prepareLiteral function).
      */
     CodeOp* op;
+
+    BindingArray bindings;
+
+    bool keepRecycled() const
+    {
+      if constexpr (removing) {
+        return bindings.keepRecycled() || btStack.keepRecycled()
+          || (RemovingBase::firstsInBlocks && RemovingBase::firstsInBlocks->keepRecycled());
+      } else {
+        return bindings.keepRecycled() || btStack.keepRecycled();
+      }
+    }
+
   protected:
+    void init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_ = 0,
+      size_t linfoCnt_ = 0, Stack<CodeOp*>* firstsInBlocks_ = 0);
 
+    bool backtrack();
+    bool prepareLiteral();
+    bool doAssignVar();
+    bool doCheckVar();
+    bool doCheckFun();
     bool doCheckGroundTerm();
+    bool doSearchStruct();
 
     /**
      * Position in the flat term
@@ -333,6 +410,34 @@ class CodeTree
      */
     FlatTerm* ft;
 
+    /** the matcher object is initialized but no execution of code was done yet */
+    bool fresh;
+    bool _matched;
+
+    /** Stack containing backtracking points */
+    Stack<std::conditional_t<removing,BTPointRemoving,BTPoint>> btStack;
+
+    CodeOp* entry;
+    CodeTree* tree;
+
+    /**
+     * Array of alternative LitInfo objects
+     *
+     * Must be initialized by inheritor.
+     */
+    LitInfo* linfos;
+    /**
+     * Length of the @b linfos array
+     *
+     * Must be initialized by inheritor.
+     */
+    size_t linfoCnt;
+
+    /**
+     * Currently matched LitInfo object in case LitInfo objects
+     * are used (they are not in TermCodeTree::TermMatcher).
+     */
+    size_t curLInfo;
   };
 
   //////// auxiliary methods //////////
@@ -383,155 +488,10 @@ class CodeTree
 
   void optimizeMemoryAfterRemoval(Stack<CodeOp*>* firstsInBlocks, CodeOp* removedOp);
 
-  template<bool checkRange>
-  struct RemovingMatcher
-  : public BaseMatcher
-  {
-  public:
-    bool next();
-
-    bool keepRecycled() const
-    { return bindings.keepRecycled() 
-        || btStack.keepRecycled() 
-        || (firstsInBlocks && firstsInBlocks->keepRecycled()); }
-
-  protected:
-    void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
-	CodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
-
-
-    bool prepareLiteral();
-    bool backtrack();
-    bool doSearchStruct();
-    bool doCheckFun();
-    bool doAssignVar();
-    bool doCheckVar();
-
-
-    struct BTPoint
-    {
-      BTPoint(size_t tp, CodeOp* op, size_t fibDepth)
-      : tp(tp), op(op), fibDepth(fibDepth) {}
-
-      size_t tp;
-      CodeOp* op;
-      size_t fibDepth;
-    };
-
-    /** Variable bindings */
-    DArray<unsigned> bindings;
-    DHSet<unsigned> range;
-
-    Stack<BTPoint> btStack;
-    Stack<CodeOp*>* firstsInBlocks;
-    bool fresh;
-    size_t curLInfo;
-
-    CodeOp* entry;
-    size_t initFIBDepth;
-
-    LitInfo* linfos;
-    size_t linfoCnt;
-
-    bool matchingClauses;
-    CodeTree* tree;
-  };
-
-  //////// retrieval //////////
-
-  /**
-   * Backtracking point for the interpretation of the code tree.
-   */
-  struct BTPoint
-  {
-    BTPoint() {}
-    BTPoint(size_t tp, CodeOp* op) : tp(tp), op(op) {}
-
-    /** Position in the flat term */
-    size_t tp;
-    /** Pointer to the next operation */
-    CodeOp* op;
-  };
-
-  typedef Stack<BTPoint> BTStack;
-  typedef DArray<TermList> BindingArray;
-
-  /**
-   * Context for finding matches of literals
-   *
-   * Here the actual execution of the code of the tree takes place.
-   *
-   * The object is not initialized not only by constructor, but also by
-   * a call to the @b init function (inheritors should implement their
-   * own @b init function (possibly with other arguments) that will call
-   * this one. After use, the @b deinit function should be called (if
-   * present). This allows for reuse of a single object.
-   */
-  struct Matcher
-  : public BaseMatcher
-  {
-    void init(CodeTree* tree, CodeOp* entry_);
-
-    inline bool finished() const { return !_fresh && !_matched; }
-    inline bool matched() const { return _matched && op->isLitEnd(); }
-    inline bool success() const { return _matched && op->isSuccess(); }
-
-
-
-  private:
-    bool backtrack();
-    bool doSearchStruct();
-    bool doCheckFun();
-    void doAssignVar();
-    bool doCheckVar();
-
-  protected:
-    bool execute();
-    bool prepareLiteral();
-
-  public:
-    /** Variable bindings */
-    BindingArray bindings;
-    bool keepRecycled() const { return bindings.keepRecycled(); }
-
-  protected:
-    /** the matcher object is initialized but no execution of code was done yet */
-    bool _fresh;
-    bool _matched;
-
-    /** Stack containing backtracking points */
-    BTStack btStack;
-
-    CodeOp* entry;
-
-    CodeTree* tree;
-    /**
-     * Array of alternative LitInfo objects
-     *
-     * Must be initialized by inheritor.
-     */
-    LitInfo* linfos;
-    /**
-     * Length of the @b linfos array
-     *
-     * Must be initialized by inheritor.
-     */
-    size_t linfoCnt;
-
-    /**
-     * Currently matched LitInfo object in case LitInfo objects
-     * are used (they are not in TermCodeTree::TermMatcher).
-     */
-    size_t curLInfo;
-
-  };
-
-
   void incTimeStamp();
 
   //////// member variables //////////
 
-
   bool _clauseCodeTree;
   unsigned _curTimeStamp;
 
@@ -544,4 +504,3 @@ class CodeTree
 }
 
 #endif // __CodeTree__
-
diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp
index f25ee8549..b4822683b 100644
--- a/Indexing/TermCodeTree.cpp
+++ b/Indexing/TermCodeTree.cpp
@@ -78,7 +78,7 @@ void TermCodeTree<Data>::remove(const Data& data)
   
   Data* dptr = nullptr;
   for(;;) {
-    if (!rtm.next()) {
+    if (!rtm.execute()) {
       ASSERTION_VIOLATION;
       INVALID_OPERATION("term being removed was not found");
     }
@@ -122,7 +122,7 @@ template<class Data>
 void TermCodeTree<Data>::RemovingTermMatcher::init(FlatTerm* ft_,
 					     TermCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_)
 {
-  RemovingMatcher::init(tree_->getEntryPoint(), 0, 0, tree_, firstsInBlocks_);
+  Matcher::init(tree_, tree_->getEntryPoint(), 0, 0, firstsInBlocks_);
   
   firstsInBlocks->push(entry);
 
diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp
index deed75195..75aa8f790 100644
--- a/Indexing/TermCodeTree.hpp
+++ b/Indexing/TermCodeTree.hpp
@@ -43,7 +43,7 @@ class TermCodeTree : public CodeTree
 
 private:
   struct RemovingTermMatcher
-  : public RemovingMatcher<false>
+  : public Matcher</*removing*/true,false>
   {
   public:
     void init(FlatTerm* ft_, TermCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
@@ -52,7 +52,7 @@ class TermCodeTree : public CodeTree
 
 public:
   struct TermMatcher
-  : public Matcher
+  : public Matcher</*removing*/false,false>
   {
     TermMatcher();
 
diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp
index dc4e82515..0f2755db3 100644
--- a/Shell/PartialRedundancyHandler.cpp
+++ b/Shell/PartialRedundancyHandler.cpp
@@ -94,7 +94,7 @@ class PartialRedundancyHandler::ConstraintIndex
       FlatTerm* ft = FlatTerm::createUnexpanded(ts);
       vm.init(ft, this, &firstsInBlocks);
 
-      if (vm.next()) {
+      if (vm.execute()) {
         ASS(vm.op->isSuccess());
         auto container = vm.op->template getSuccessResult<EntryContainer>();
         container->tod->insert(ptr->ordCons, ptr);
@@ -246,7 +246,7 @@ class PartialRedundancyHandler::ConstraintIndex
   }
 
   struct SubstMatcher
-  : public Matcher
+  : public Matcher</*removing*/false,false>
   {
     void init(CodeTree* tree, const TermStack& ts)
     {
@@ -281,11 +281,11 @@ class PartialRedundancyHandler::ConstraintIndex
   };
 
   struct VariantMatcher
-  : public RemovingMatcher<true>
+  : public Matcher</*removing*/true,true>
   {
   public:
     void init(FlatTerm* ft_, CodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_) {
-      RemovingMatcher::init(tree_->getEntryPoint(), 0, 0, tree_, firstsInBlocks_);
+      Matcher::init(tree_, tree_->getEntryPoint(), 0, 0, firstsInBlocks_);
       ft=ft_;
       tp=0;
       op=entry;