1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index a838a6a0c..a380dcbf2 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -72,11 +72,10 @@ void CegConjecture::assign( Node q ) {
     // carry the templates
     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
       Node v = q[0][i];
-      Node sf = v.getAttribute(SygusSynthFunAttribute());
-      Node templ = d_ceg_si->getTemplate(sf);
+      Node templ = d_ceg_si->getTemplate(v);
       if( !templ.isNull() ){
-        templates[sf] = templ;
-        templates_arg[sf] = d_ceg_si->getTemplateArg(sf);
+        templates[v] = templ;
+        templates_arg[v] = d_ceg_si->getTemplateArg(v);
       }
     }
   }
@@ -562,7 +561,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         status = 1;
         
         //check if there was a template
-        Node sf = d_quant[0][i].getAttribute(SygusSynthFunAttribute());
+        Node sf = d_quant[0][i];
         Node templ = d_ceg_si->getTemplate( sf );
         if( !templ.isNull() ){
           Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl;