diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-09-23 06:00:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-23 08:00:59 -0500 |
| commit | 9967954ba1b7b405b6d92d83ebc0adc43f6623b9 (patch) | |
| tree | d2c08b4b644a23e1092f31a4d242949f3c5a293f /test/regress/regress0/bv/bv_to_int1.smt2 | |
| parent | cfe0fc1346c41048fa76f7e0fc582afbe95364a2 (diff) | |
bv2int: new options for bvand translation (#5096)
Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):
bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).
Diffstat (limited to 'test/regress/regress0/bv/bv_to_int1.smt2')
| -rw-r--r-- | test/regress/regress0/bv/bv_to_int1.smt2 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index 970a9fd75..9111ac25c 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) |