diff options
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 07dd3de5b..cfe41316c 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -187,6 +187,8 @@ annotatedFormula[CVC4::Expr& expr] /* 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 if( (kind == CVC4::kind::AND || kind == CVC4::kind::OR) ) { + expr = EXPR_MANAGER->mkAssociative(kind,args); } else { PARSER_STATE->checkArity(kind, args.size()); expr = MK_EXPR(kind, args); |