diff --git a/packages/CLPBN/horus/LiftedCircuit.cpp b/packages/CLPBN/horus/LiftedCircuit.cpp
index 4012aa8a8..2edc0d2c9 100644
--- a/packages/CLPBN/horus/LiftedCircuit.cpp
+++ b/packages/CLPBN/horus/LiftedCircuit.cpp
@@ -101,9 +101,7 @@ LeafNode::weight (void) const
   lvs -= clause_->negCountedLogVars();
   unsigned nrGroundings = 1;
   if (lvs.empty() == false) {
-    ConstraintTree ct = clause_->constr();
-    ct.project (lvs);
-    nrGroundings = ct.size();
+    nrGroundings = clause_->constr().projectedCopy (lvs).size();
   }
   if (clause_->posCountedLogVars().empty() == false) {
     nrGroundings *= std::pow (SetOrNode::nrPositives(),
@@ -113,7 +111,7 @@ LeafNode::weight (void) const
     nrGroundings *= std::pow (SetOrNode::nrNegatives(),
         clause_->nrNegCountedLogVars());
   }
-  return Globals::logDomain 
+  return Globals::logDomain
       ? weight * nrGroundings
       : std::pow (weight, nrGroundings);
 }
@@ -134,9 +132,7 @@ SmoothNode::weight (void) const
     lvs -= cs[i]->negCountedLogVars();
     unsigned nrGroundings = 1;
     if (lvs.empty() == false) {
-      ConstraintTree ct = cs[i]->constr();
-      ct.project (lvs);
-      nrGroundings = ct.size();
+      nrGroundings = cs[i]->constr().projectedCopy (lvs).size();
     }
     if (cs[i]->posCountedLogVars().empty() == false) {
       nrGroundings *= std::pow (SetOrNode::nrPositives(), 
@@ -169,7 +165,7 @@ double
 CompilationFailedNode::weight (void) const
 {
   // weighted model counting in compilation
-  // failed nodes should give nan
+  // failed nodes should give NaN
   return 0.0 / 0.0;
 }
 
@@ -474,13 +470,11 @@ LiftedCircuit::tryInclusionExclusion (
       for (size_t j = 0; j < indepLits.size(); j++) {
         c2->addLiteral (indepLits[j]);
       }
+  
+      clauses.erase (clauses.begin() + i);
       Clauses plus1Clauses = Clause::copyClauses (clauses);
       Clauses plus2Clauses = Clause::copyClauses (clauses);
 
-      plus1Clauses.erase (plus1Clauses.begin() + i);
-      plus2Clauses.erase (plus2Clauses.begin() + i);
-      clauses.erase (clauses.begin() + i);
-
       plus1Clauses.push_back (c1);
       plus2Clauses.push_back (c2);
       clauses.push_back (c1);
@@ -744,7 +738,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
       propagLits |= lids2;
       break;
     }
-  
+
     case CircuitNodeType::AND_NODE: {
       AndNode* casted = dynamic_cast<AndNode*>(node);
       LitLvTypesSet lids1 = smoothCircuit (*casted->leftBranch());
@@ -785,13 +779,13 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
       }
       break;
     }
-    
+
     case CircuitNodeType::SET_AND_NODE: {
       SetAndNode* casted = dynamic_cast<SetAndNode*>(node);
       propagLits = smoothCircuit (*casted->follow());
       break;
     }
-    
+
     case CircuitNodeType::INC_EXC_NODE: {
       IncExcNode* casted = dynamic_cast<IncExcNode*>(node);
       LitLvTypesSet lids1 = smoothCircuit (*casted->plus1Branch());
@@ -804,18 +798,18 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
       propagLits |= lids2;
       break;
     }
-    
+
     case CircuitNodeType::LEAF_NODE: {
       LeafNode* casted = dynamic_cast<LeafNode*>(node);    
       propagLits.insert (LitLvTypes (
           casted->clause()->literals()[0].lid(),
           casted->clause()->logVarTypes(0)));
     }
- 
+
     default:
       break;
   }
-  
+
   return propagLits;
 }
 
@@ -828,9 +822,14 @@ LiftedCircuit::createSmoothNode (
 {
   if (missingLits.empty() == false) {
     if (Globals::verbosity > 1) {
-      // assert (Util::contains (originClausesMap_, prev));
-      backupClauses_ = originClausesMap_[*prev]; // TODO Clause::copyClauses ?
-    }  
+      unordered_map<CircuitNode*, Clauses>::iterator it;
+      it = originClausesMap_.find (*prev);
+      if (it != originClausesMap_.end()) {
+        backupClauses_ = it->second;
+      } else {
+        backupClauses_ = { ((dynamic_cast<LeafNode*>(*prev))->clause()) };
+      }
+    }
     Clauses clauses;
     for (size_t i = 0; i < missingLits.size(); i++) {
       LiteralId lid = missingLits[i].lid();
@@ -1127,21 +1126,18 @@ LiftedCircuit::printClauses (
   if (Util::contains (originClausesMap_, node)) {
     clauses = originClausesMap_[node];
   } else if (getCircuitNodeType (node) == CircuitNodeType::LEAF_NODE) {
-    clauses  = { (dynamic_cast<LeafNode*>(node))->clause() } ;
+    clauses = { (dynamic_cast<LeafNode*>(node))->clause() } ;
   } else if (getCircuitNodeType (node) == CircuitNodeType::SMOOTH_NODE) {
-    clauses  = (dynamic_cast<SmoothNode*>(node))->clauses();
+    clauses = (dynamic_cast<SmoothNode*>(node))->clauses();
   }
-  if (clauses.empty() == false) {
-    os << escapeNode (node);
-    os << " [shape=box," << extraOptions << "label=\"" ;  
-    for (size_t i = 0; i < clauses.size(); i++) {
-      if (i != 0) os << "\\n" ;
-      os << *clauses[i];
-    }
-    os << "\"]" ;
-    os << endl;
-  } else {
-    os << " [shape=box]" << endl;  
+  assert (clauses.empty() == false);
+  os << escapeNode (node);
+  os << " [shape=box," << extraOptions << "label=\"" ;
+  for (size_t i = 0; i < clauses.size(); i++) {
+    if (i != 0) os << "\\n" ;
+    os << *clauses[i];
   }
+  os << "\"]" ;
+  os << endl;
 }
 
diff --git a/packages/CLPBN/horus/LiftedWCNF.cpp b/packages/CLPBN/horus/LiftedWCNF.cpp
index 5394a51a8..33d0c87ca 100644
--- a/packages/CLPBN/horus/LiftedWCNF.cpp
+++ b/packages/CLPBN/horus/LiftedWCNF.cpp
@@ -33,11 +33,6 @@ Literal::toString (
 {
   stringstream ss;
   negated_ ? ss << "¬" : ss << "" ;
-  // if (negated_ == false) {
-  //   posWeight_ < 0.0 ? ss << "λ" : ss << "Θ" ;
-  // } else {
-  //   negWeight_ < 0.0 ? ss << "λ" : ss << "Θ" ;  
-  // }
   ss << "λ" ;
   ss << lid_ ;
   if (logVars_.empty() == false) {
@@ -480,16 +475,14 @@ LiftedWCNF::createClause (LiteralId lid) const
     const Literals& literals = clauses_[i]->literals();
     for (size_t j = 0; j < literals.size(); j++) {
       if (literals[j].lid() == lid) {
-        // TODO projectedCopy ?
-        ConstraintTree ct = clauses_[i]->constr();
-        ct.project (literals[j].logVars());
+        ConstraintTree ct = clauses_[i]->constr().projectedCopy (
+            literals[j].logVars());
         Clause* c = new Clause (ct);
         c->addLiteral (literals[j]);
         return c;
       }
     }
   }
-  abort(); // we should not reach this point
   return 0;
 }
 
@@ -512,8 +505,8 @@ LiftedWCNF::addIndicatorClauses (const ParfactorList& pfList)
     const ProbFormulas& formulas = (*it)->arguments();
     for (size_t i = 0; i < formulas.size(); i++) {
       if (Util::contains (map_, formulas[i].group()) == false) {
-        ConstraintTree tempConstr = *(*it)->constr();
-        tempConstr.project (formulas[i].logVars());
+        ConstraintTree tempConstr = (*it)->constr()->projectedCopy(
+            formulas[i].logVars());
         Clause* clause = new Clause (tempConstr);
         vector<LiteralId> lids;
         for (size_t j = 0; j < formulas[i].range(); j++) {
@@ -524,8 +517,8 @@ LiftedWCNF::addIndicatorClauses (const ParfactorList& pfList)
         clauses_.push_back (clause);
         for (size_t j = 0; j < formulas[i].range() - 1; j++) {
           for (size_t k = j + 1; k < formulas[i].range(); k++) {
-            ConstraintTree tempConstr2 = *(*it)->constr();
-            tempConstr2.project (formulas[i].logVars());
+            ConstraintTree tempConstr2 = (*it)->constr()->projectedCopy (
+                formulas[i].logVars());
             Clause* clause2 = new Clause (tempConstr2);
             clause2->addLiteralComplemented (Literal (clause->literals()[j]));
             clause2->addLiteralComplemented (Literal (clause->literals()[k]));
@@ -598,8 +591,8 @@ LiftedWCNF::printFormulaIndicators (void) const
       if (Util::contains (allGroups, formulas[i].group()) == false) {
         allGroups.insert (formulas[i].group());
         cout << formulas[i] << " | " ;
-        ConstraintTree tempCt = *(*it)->constr();
-        tempCt.project (formulas[i].logVars());
+        ConstraintTree tempCt = (*it)->constr()->projectedCopy (
+            formulas[i].logVars());
         cout << tempCt.tupleSet();
         cout << " indicators => " ;
         vector<LiteralId> indicators =