diff options
Diffstat (limited to 'test/regress/regress0/bv')
-rw-r--r-- | test/regress/regress0/bv/bvsmod.smt2 | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/bvsmod.smt2 b/test/regress/regress0/bv/bvsmod.smt2 new file mode 100644 index 000000000..384e3c7b8 --- /dev/null +++ b/test/regress/regress0/bv/bvsmod.smt2 @@ -0,0 +1,28 @@ +(set-logic QF_BV) + +(set-info :status unsat) + +(define-fun bvsmod_def ((s (_ BitVec 13)) (t (_ BitVec 13))) (_ BitVec 13) + (let ((msb_s ((_ extract 12 12) s)) + (msb_t ((_ extract 12 12) t))) + (let ((abs_s (ite (= msb_s #b0) s (bvneg s))) + (abs_t (ite (= msb_t #b0) t (bvneg t)))) + (let ((u (bvurem abs_s abs_t))) + (ite (= u (_ bv0 13)) + u + (ite (and (= msb_s #b0) (= msb_t #b0)) + u + (ite (and (= msb_s #b1) (= msb_t #b0)) + (bvadd (bvneg u) t) + (ite (and (= msb_s #b0) (= msb_t #b1)) + (bvadd u t) + (bvneg u))))))))) + +(define-fun a () (_ BitVec 13) (_ bv30 13)) +(define-fun b () (_ BitVec 13) (_ bv8190 13)) + +(assert (not (= (bvsmod_def a b) (bvsmod a b)))) + +(check-sat) + +(exit) |