diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-16 12:11:37 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2019-04-16 12:11:37 -0700 |
| commit | 2f7131c81078a964a4043ef79186cdcf91951974 (patch) | |
| tree | 14fe132462c8be51f19578448033acd3f08b7eff /test/regress/CMakeLists.txt | |
| parent | a47b722aa31cdd036f83425b2a805e6a572a974b (diff) | |
Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)
The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`. This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.
References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2c6acf69c..97ca9a1be 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -534,6 +534,7 @@ set(regress_0_tests regress0/options/invalid_dump.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 + regress0/parser/bv_arity_smt2.6.smt2 regress0/parser/constraint.smt2 regress0/parser/declarefun-emptyset-uf.smt2 regress0/parser/shadow_fun_symbol_all.smt2 |