1 files changed, 0 insertions, 12 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 0c844f92d..75e37151a 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -22,9 +22,6 @@
 #include "base/output.h"
 #include "expr/attribute.h"
 
-#include "theory/quantifiers/term_database.h"
-
-
 using namespace std;
 
 namespace CVC4 {
@@ -113,15 +110,6 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
       for(iterator i = begin(); i != end() && !hasBv; ++i) {
         hasBv = (*i).hasBoundVar();
       }
-      if( !hasBv ){
-        //FIXME : this is a hack to handle synthesis conjectures
-        // the issue is that we represent second-order quantification in synthesis conjectures via a Node:
-        //  exists x forall y P[f,y], where x is a dummy variable that maps to f through attribute SygusSynthFunVarListAttributeId
-        //  when asked whether a node has a bound variable, we want to treat f as if it were a bound (second-order) variable. -AJR
-        if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){
-          hasBv = true;
-        }
-      }
     }
     setAttribute(HasBoundVarAttr(), hasBv);
     setAttribute(HasBoundVarComputedAttr(), true);