summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g3
1 files changed, 2 insertions, 1 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback