1 files changed, 14 insertions, 14 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 047a78d11..529ef037f 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -55,20 +55,20 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   for (const Node& s : symset)
   {
     TypeNode tn = s.getType();
-    if (tn.isFirstClass())
-    {
-      std::stringstream ss;
-      ss << s;
-      Node var = nm->mkBoundVar(tn);
-      syms.push_back(s);
-      vars.push_back(var);
-      Node vlv = nm->mkBoundVar(ss.str(), tn);
-      varlist.push_back(vlv);
-      varlistTypes.push_back(tn);
-      // set that this variable encodes the term s
-      SygusVarToTermAttribute sta;
-      vlv.setAttribute(sta, s);
-    }
+    // Notice that we allow for non-first class (e.g. function) variables here.
+    // This is applicable to the case where we are doing get-abduct in a logic
+    // with UF.
+    std::stringstream ss;
+    ss << s;
+    Node var = nm->mkBoundVar(tn);
+    syms.push_back(s);
+    vars.push_back(var);
+    Node vlv = nm->mkBoundVar(ss.str(), tn);
+    varlist.push_back(vlv);
+    varlistTypes.push_back(tn);
+    // set that this variable encodes the term s
+    SygusVarToTermAttribute sta;
+    vlv.setAttribute(sta, s);
   }
   // make the sygus variable list
   Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist);