diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 10 |
1 files changed, 3 insertions, 7 deletions
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; } |