diff --git a/packages/CLPBN/horus/LiftedCircuit.cpp b/packages/CLPBN/horus/LiftedCircuit.cpp
index 666d895e4..dd021bffb 100644
--- a/packages/CLPBN/horus/LiftedCircuit.cpp
+++ b/packages/CLPBN/horus/LiftedCircuit.cpp
@@ -156,10 +156,9 @@ TrueNode::weight (void) const
 double
 CompilationFailedNode::weight (void) const
 {
-  // we should not perform model counting
-  // in compilation failed nodes
-  // abort();
-  return 0.0;
+  // weighted model counting in compilation
+  // failed nodes should give nan
+  return 0.0 / 0.0;
 }
 
 
@@ -168,21 +167,33 @@ LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf)
     : lwcnf_(lwcnf)
 {
   root_ = 0;
+  compilationSucceeded_ = true;
   Clauses clauses = lwcnf->clauses();
   compile (&root_, clauses);
   if (Globals::verbosity > 1) {
     smoothCircuit (root_);
     exportToGraphViz("circuit.smooth.dot");
-    double wmc = LogAware::exp (getWeightedModelCount());
-    cout << "WEIGHTED MODEL COUNT: " << wmc << endl << endl;
+    if (compilationSucceeded_) {
+      double wmc = LogAware::exp (getWeightedModelCount());
+      cout << "WEIGHTED MODEL COUNT: " << wmc << endl << endl;
+    }
   }
 }
 
 
 
+bool
+LiftedCircuit::isCompilationSucceeded (void) const
+{
+  return compilationSucceeded_;
+}
+
+
+
 double
 LiftedCircuit::getWeightedModelCount (void) const
 {
+  assert (compilationSucceeded_);
   return root_->weight();
 }
 
@@ -211,6 +222,11 @@ LiftedCircuit::compile (
     CircuitNode** follow,
     Clauses& clauses)
 {
+  if (compilationSucceeded_ == false
+      && Globals::verbosity <= 1) {
+    return;
+  }
+
   if (clauses.empty()) {
     *follow = new TrueNode ();
     return;
@@ -245,8 +261,8 @@ LiftedCircuit::compile (
     return;
   }
 
-  // assert (false);
   *follow = new CompilationFailedNode (clauses);
+  compilationSucceeded_ = false;
 }
 
 
diff --git a/packages/CLPBN/horus/LiftedCircuit.h b/packages/CLPBN/horus/LiftedCircuit.h
index 12af4d6ee..cc0263d52 100644
--- a/packages/CLPBN/horus/LiftedCircuit.h
+++ b/packages/CLPBN/horus/LiftedCircuit.h
@@ -209,7 +209,9 @@ class CompilationFailedNode : public CircuitNode
 class LiftedCircuit
 {
   public:
-    LiftedCircuit (const LiftedWCNF* lwcnf);    
+    LiftedCircuit (const LiftedWCNF* lwcnf);
+
+    bool isCompilationSucceeded (void) const;
 
     double getWeightedModelCount (void) const;
 
@@ -266,6 +268,7 @@ class LiftedCircuit
 
     CircuitNode*       root_;
     const LiftedWCNF*  lwcnf_;
+    bool               compilationSucceeded_;
 };
 
 #endif // HORUS_LIFTEDCIRCUIT_H
diff --git a/packages/CLPBN/horus/LiftedKc.cpp b/packages/CLPBN/horus/LiftedKc.cpp
index 6c0aba622..d9560f6df 100644
--- a/packages/CLPBN/horus/LiftedKc.cpp
+++ b/packages/CLPBN/horus/LiftedKc.cpp
@@ -21,6 +21,10 @@ LiftedKc::solveQuery (const Grounds& query)
   LiftedOperations::runWeakBayesBall (pfList_, query);
   lwcnf_ = new LiftedWCNF (pfList_);
   circuit_ = new LiftedCircuit (lwcnf_);
+  if (circuit_->isCompilationSucceeded() == false) {
+    cerr << "error: compilation failed" << endl;
+    abort();
+  }
   vector<PrvGroup> groups;
   Ranges ranges;
   for (size_t i = 0; i < query.size(); i++) {