1234567891011121314151617181920212223242526 |
- (declare-const x (_ BitVec 8))
- (declare-const y (_ BitVec 8))
- (declare-const avgu (_ BitVec 8))
- (declare-const realavg Int)
- (push)
- ; again we try to find a counterexample by asserting the premise but not the conclusion
- ; the conclusion is that the function computes something different than the requested value
- ; the result is checked in the domain of integers!
- (assert (= avgu (bvadd (bvand x y) (bvlshr (bvxor x y) #x01))))
- (assert (= realavg (div (+ (bv2nat x) (bv2nat y)) 2)))
- (assert (not (= (bv2nat avgu) realavg)))
- (check-sat)
- ;(get-model)
- (pop)
- (push)
- ; we do the same, but this time using arithmetic shift to see whether there is any difference
- (assert (= avgu (bvadd (bvand x y) (bvashr (bvxor x y) #x01))))
- (assert (= realavg (div (+ (bv2nat x) (bv2nat y)) 2)))
- (assert (not (= (bv2nat avgu) realavg)))
- ;(check-sat)
- ;(get-model)
|