From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 10 Jun 2015 14:43:03 +0000 (+0200)
Subject: Bug fix parsing constant constructor sygus.
X-Git-Tag: cvc5-1.0.0~6296
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ad9f1e8a19d9658a86203fe2db8ad9fb329cd8e;p=cvc5.git

Bug fix parsing constant constructor sygus.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 54938a686..aa56d1f2e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -878,10 +878,11 @@ sygusGTerm[int index,
             PARSER_STATE->parseError(std::string("Must provide single sort for constant/variable Sygus constructor."));
           }
           cargs[index].pop_back();
-          Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << std::endl;
-          if( gtermType==2 ){
+          Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << ", gterm type=" << sub_gtermType << std::endl;
+          if( sub_gtermType==2 ){
             std::vector< Expr > consts;
             PARSER_STATE->mkSygusConstantsForType( t, consts );
+            Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
             for( unsigned i=0; i<consts.size(); i++ ){
               std::stringstream ss;
               ss << consts[i];
@@ -891,6 +892,7 @@ sygusGTerm[int index,
               cargs[index].push_back( std::vector< CVC4::Type >() );
             }
           }else if( sub_gtermType==3 ){
+            Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
             for( unsigned i=0; i<sygus_vars.size(); i++ ){
               if( sygus_vars[i].getType()==t ){
                 std::stringstream ss;