exercise7.smt2 844 B

1234567891011121314151617181920212223242526
  1. (declare-const x (_ BitVec 8))
  2. (declare-const y (_ BitVec 8))
  3. (declare-const avgu (_ BitVec 8))
  4. (declare-const realavg Int)
  5. (push)
  6. ; again we try to find a counterexample by asserting the premise but not the conclusion
  7. ; the conclusion is that the function computes something different than the requested value
  8. ; the result is checked in the domain of integers!
  9. (assert (= avgu (bvadd (bvand x y) (bvlshr (bvxor x y) #x01))))
  10. (assert (= realavg (div (+ (bv2nat x) (bv2nat y)) 2)))
  11. (assert (not (= (bv2nat avgu) realavg)))
  12. (check-sat)
  13. ;(get-model)
  14. (pop)
  15. (push)
  16. ; we do the same, but this time using arithmetic shift to see whether there is any difference
  17. (assert (= avgu (bvadd (bvand x y) (bvashr (bvxor x y) #x01))))
  18. (assert (= realavg (div (+ (bv2nat x) (bv2nat y)) 2)))
  19. (assert (not (= (bv2nat avgu) realavg)))
  20. ;(check-sat)
  21. ;(get-model)