diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-01 20:06:10 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-01 20:06:10 +0000 |
| commit | f4918a518a69090ed0ba2547fb21cd8f418c648b (patch) | |
| tree | 51dc3b180d20ef8358eba3f1ca4d66d17ba446c2 /src/parser/smt/Smt.g | |
| parent | ed25d7b7527691442ab48d02353e20c87ab8e2da (diff) | |
Changing min/maxArity to use metakind info.
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 9bcee54fd..93b8560d0 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -158,12 +158,12 @@ annotatedFormula[CVC4::Expr& expr] } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK - { PARSER_STATE->checkArity(kind, args.size()); - if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { + { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); } else { + PARSER_STATE->checkArity(kind, args.size()); expr = MK_EXPR(kind, args); } } |