1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 262085a23..e45ca49e0 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -22,6 +22,8 @@
 #include "base/output.h"
 #include "expr/attribute.h"
 
+#include "theory/quantifiers/term_database.h"
+
 
 using namespace std;
 
@@ -111,6 +113,11 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
       for(iterator i = begin(); i != end() && !hasBv; ++i) {
         hasBv = (*i).hasBoundVar();
       }
+      if( !hasBv ){
+        if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){
+          hasBv = true;
+        }
+      }
     }
     setAttribute(HasBoundVarAttr(), hasBv);
     setAttribute(HasBoundVarComputedAttr(), true);