blob: 384e3c7b835fb5f44c423ac70e73efd9387ae11a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
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)
|
