From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Aug 2017 10:00:43 +0000 (-0500)
Subject: Change sygus output for failed reconstruction case.
X-Git-Tag: cvc5-1.0.0~5693
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6eee137dc64e3f2c467d70edf2bb18abd6b3b071;p=cvc5.git

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 cb8e6f200..9ee79af1f 100644
--- 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;
       }