diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress2/bv_to_int_shifts.smt2 | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 index 998234a17..d213b0c3d 100644 --- a/test/regress/regress2/bv_to_int_shifts.smt2 +++ b/test/regress/regress2/bv_to_int_shifts.smt2 @@ -1,17 +1,18 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) -(declare-fun s () (_ BitVec 64)) -(declare-fun t () (_ BitVec 64)) -(declare-fun splust () (_ BitVec 64)) -(declare-fun shift1 () (_ BitVec 64)) -(declare-fun shift2 () (_ BitVec 64)) -(declare-fun negshift1 () (_ BitVec 64)) +(declare-fun s () (_ BitVec 4)) +(declare-fun t () (_ BitVec 4)) +(declare-fun splust () (_ BitVec 4)) +(declare-fun shift1 () (_ BitVec 4)) +(declare-fun shift2 () (_ BitVec 4)) +(declare-fun negshift1 () (_ BitVec 4)) (assert (= shift1 (bvlshr s splust))) (assert (= shift2 (bvlshr t splust))) (assert (= negshift1 (bvneg shift1))) (assert (= splust (bvadd s t))) (assert (distinct negshift1 shift2)) +(assert (distinct s (bvshl s (_ bv4 4)))) (check-sat) |