Change sygus output for failed reconstruction case.

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index cb8e6f200775c6a0e21e53aa3c61c01ac31e67e3..9ee79af1f06040cd2ac9a4b8d1c32323a8972a05 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -1002,7 +1002,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
           Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl;
         }
       }
-      if( !(Trace.isOn("cegqi-stats")) ){
+      if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){
         out << "(define-fun " << f << " ";
         if( dt.getSygusVarList().isNull() ){
           out << "() ";
@@ -1013,12 +1013,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
         if( status==0 ){
           out << sol;
         }else{
-          if( sol.isNull() ){
-            out << "?";
-          }else{
-            std::vector< Node > lvs;
-            TermDbSygus::printSygusTerm( out, sol, lvs );
-          }
+          std::vector< Node > lvs;
+          TermDbSygus::printSygusTerm( out, sol, lvs );
         }
         out << ")" << std::endl;
       }