diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 89c37883a..6919c86c4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -206,7 +206,15 @@ term[CVC4::Expr& expr] } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK - { if( !PARSER_STATE->strictModeEnabled() && + { + if( kind == CVC4::kind::EQUAL && + args.size() > 0 && + args[0].getType() == EXPR_MANAGER->booleanType() ) { + /* Use IFF for boolean equalities. */ + kind = CVC4::kind::IFF; + } + + if( !PARSER_STATE->strictModeEnabled() && (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. |