summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-09-09 22:34:36 -0500
committerGitHub <noreply@github.com>2020-09-09 22:34:36 -0500
commitb85ef5a122127f50b38380ec452023c26fdbbc66 (patch)
tree39e3cc7adbcd9b810fc7aeb31fc03c9a7caa7b35
parent98f808f01735c6cebfbf945fcb072da3ba6cff6c (diff)
Parser error for wrong number of datatypes (#5049)
Fixes #4973.
-rw-r--r--src/parser/smt2/Smt2.g4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4bb253603..ea0c3b714 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1265,6 +1265,10 @@ datatypesDef[bool isCo,
RPAREN_TOK
)+
{
+ if (dts.size() != dnames.size())
+ {
+ PARSER_STATE->parseError("Wrong number of datatypes provided.");
+ }
PARSER_STATE->popScope();
cmd->reset(new DatatypeDeclarationCommand(
api::sortVectorToTypes(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback