diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 3 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 20 |
2 files changed, 17 insertions, 6 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5c5b87f38..00f2e944d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1886,7 +1886,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Kind lassocKind = CVC4::kind::UNDEFINED_KIND; if (args.size() >= 2) { - if (kind == CVC4::kind::INTS_DIVISION) + if (kind == CVC4::kind::INTS_DIVISION + || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6())) { // Builtin operators that are not tokenized, are left associative, // but not internally variadic must set this. diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 171642c7e..7a3c3b0c3 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -319,15 +319,25 @@ private: // that CVC4 permits as N-ary but the standard requires is binary if(strictModeEnabled()) { switch(kind) { - case kind::BITVECTOR_CONCAT: case kind::BITVECTOR_AND: - case kind::BITVECTOR_OR: - case kind::BITVECTOR_XOR: case kind::BITVECTOR_MULT: + case kind::BITVECTOR_OR: case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_XOR: + if (numArgs != 2 && !v2_6()) + { + parseError( + "Operator requires exactly 2 arguments in strict SMT-LIB " + "compliance mode (for versions <2.6): " + + kindToString(kind)); + } + break; + case kind::BITVECTOR_CONCAT: if(numArgs != 2) { - parseError("Operator requires exact 2 arguments in strict SMT-LIB " - "compliance mode: " + kindToString(kind)); + parseError( + "Operator requires exactly 2 arguments in strict SMT-LIB " + "compliance mode: " + + kindToString(kind)); } break; default: |