Parse error for sygus grammar term with multiple let bodies (#1961)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 133cc12c13908aa81357e210e004f83b107493d9..e0769f88a20f7a92823c8953906ee9e5e3ded5ff 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -930,7 +930,16 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
   cargs[index][dindex].pop_back();
   collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
 
-  Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
+  Debug("parser-sygus") << "Make define-fun with "
+                        << cargs[index][dindex].size()
+                        << " operator arguments and " << let_define_args.size()
+                        << " provided arguments..." << std::endl;
+  if (cargs[index][dindex].size() != let_define_args.size())
+  {
+    std::stringstream ss;
+    ss << "Wrong number of let body terms." << std::endl;
+    parseError(ss.str());
+  }
   std::vector<CVC4::Type> fsorts;
   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
     Debug("parser-sygus") << "  " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;