From 5ad9f1e8a19d9658a86203fe2db8ad9fb329cd8e Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 10 Jun 2015 16:43:03 +0200
Subject: [PATCH] Bug fix parsing constant constructor sygus.

---
 src/parser/smt2/Smt2.g | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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;
-- 
2.30.2