Handle (degenerate) case of synthesis conjectures for constants. Disable delta lemmas.

2 files changed, 8 insertions, 1 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 7553eb736..ea97513b8 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -505,7 +505,11 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       }
       if( !(Trace.isOn("cegqi-stats")) ){
         out << "(define-fun " << f << " ";
-        out << dt.getSygusVarList() << " ";
+        if( dt.getSygusVarList().isNull() ){
+          out << "() ";
+        }else{
+          out << dt.getSygusVarList() << " ";
+        }
         out << dt.getSygusType() << " ";
         if( status==0 ){
           out << sol;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index b3c1e1eaa..a612db872 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -637,6 +637,8 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std:
 //check if delta has a lower bound L
 // if so, add lemma L>0 => L>d
 void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
+  return;
+  /*  disable for now
   if( !d_n_delta.isNull() ){
     Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH );
     if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){
@@ -701,6 +703,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
       }
     }
   }
+  */
 }
 
 void CegInstantiator::check() {