diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-22 18:12:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-22 18:12:54 -0500 |
commit | eab7fae2c02ce635500dbe7c743a5c0d7f39137d (patch) | |
tree | 88115e6ccf45c3320c4afd4b62e6a0bde5ff9ecd /src/parser | |
parent | 7b3494856e47945dd5c9774d2063f095f46fc4df (diff) |
Parse error for sygus grammar term with multiple let bodies (#1961)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
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; |