diff --git a/src/duality/duality.h b/src/duality/duality.h
index c6dfc906d..033cea660 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -672,6 +672,8 @@ namespace Duality {
 
       TermTree *GetGoalTree(Node *root);
 
+      int EvalTruth(hash_map<ast,int> &memo, Edge *e, const Term &f);
+
     private:
       
 
@@ -733,10 +735,8 @@ namespace Duality {
 
      Term ProjectFormula(std::vector<Term> &keep_vec, const Term &f);
 
-    public:
       int SubtermTruth(hash_map<ast,int> &memo, const Term &);
 
-    private:
       void ImplicantRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
 			hash_set<ast> *done, bool truth, hash_set<ast> &dont_cares);
 
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 38f00b4b0..13752401b 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -833,6 +833,10 @@ namespace Duality {
     return res;
   }
 
+  int RPFP::EvalTruth(hash_map<ast,int> &memo, Edge *e, const Term &f){
+    Term tl = Localize(e, f);
+    return SubtermTruth(memo,tl);
+  }
 
 #ifdef Z3OPS
   static Z3_subterm_truth *stt;
diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index c8a048a6a..e2ee25a2f 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -270,7 +270,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
     hash_map<ast,int> memo;
     for(unsigned j = 0; j < labels.size(); j++){
       RPFP::label_struct &lab = labels[j];
-      int truth = cex.tree->SubtermTruth(memo,lab.value);
+      int truth = cex.tree->EvalTruth(memo,&edge,lab.value);
       if(truth == 1 && lab.pos || truth == 0 && !lab.pos)
 	out << " " << lab.name;
     }