diff options
Diffstat (limited to 'src/parser/smt/Smt.g')
-rw-r--r-- | src/parser/smt/Smt.g | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index b03188b3c..2a3a79125 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -218,6 +218,10 @@ annotatedFormula[CVC4::Expr& expr] args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); + } else if(!PARSER_STATE->strictModeEnabled() && + kind == CVC4::kind::MINUS && args.size() == 1) { + /* Special fix-up for unary minus improperly used in some benchmarks */ + expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); } else { PARSER_STATE->checkArity(kind, args.size()); expr = MK_EXPR(kind, args); |