From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 May 2018 23:12:54 +0000 (-0500)
Subject: Parse error for sygus grammar term with multiple let bodies (#1961)
X-Git-Tag: cvc5-1.0.0~5023
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eab7fae2c02ce635500dbe7c743a5c0d7f39137d;p=cvc5.git

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 133cc12c1..e0769f88a 100644
--- 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;