My Z3 proof snippets
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;popcnt expl ;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const V (_ BitVec 64))
(declare-const I1 (_ BitVec 64))
(declare-const I2 (_ BitVec 64))
(assert
(not
(=
(bvlshr V #x0000000000000040)
#x0000000000000000
))
)
(check-sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;popcnt expl ;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const V (_ BitVec 64))
(declare-const I1 (_ BitVec 64))
(declare-const I2 (_ BitVec 64))
(assert
(and
(not
(=
(bvlshr (bvlshr V I1) I2)
(bvlshr V (bvadd I1 I2))
))
(bvule I1 #x0000000000000040)
(bvule I2 #x0000000000000040)
)
)
(check-sat)
(get-model)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 64))
(declare-const B (_ BitVec 64))
(push)
(assert
(and
(bvuge
(concat #x00000000 ((_ extract 31 0) (bvadd A B)))
A)
(>= (+ (bv2int A) (bv2int B)) (^ 2 32))
)
)
(check-sat)
(get-model)
(pop)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 64))
(declare-const B (_ BitVec 64))
(push)
(assert
(and
(bvuge
(concat #x00000000 ((_ extract 31 0) (bvadd A B)))
A)
(>= (bv2int A) (^ 2 32))
)
)
(check-sat)
(get-model)
(pop)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A Int)
(declare-const B Int)
(push)
(assert
(and
(>= A 0)
(< A 255)
(>= B 0)
(< B 255)
(> (+ A B) 15)
(>= (mod (+ A B) 16) A)
)
)
(check-sat)
(get-model)
(pop)
(push)
(assert
(and
(>= A 0)
(< A 255)
(>= B 0)
(< B 255)
(> (+ A B) 255)
(>= (mod (+ A B) 256) A)
)
)
(check-sat)
(get-model)
(pop)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 8))
(declare-const B (_ BitVec 8))
(declare-const a Int)
(declare-const b Int)
(assert
(not
(=
(bv2int (bvadd A B))
(+ (bv2int A) (bv2int B))
))
)
(assert
(and (<= (bv2int A) 15) (>= (bv2int A) 0))
)
(assert
(and (<= (bv2int B) 15) (>= (bv2int B) 0))
)
(check-sat)
(get-model)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 8))
(declare-const B (_ BitVec 8))
(declare-const a Int)
(declare-const b Int)
(assert
(not
(=
(bv2int (bvadd A B))
(+ (bv2int A) (bv2int B))
))
)
(assert
(and (>= (+ (bv2int A) (bv2int B)) 0) (<= (+ (bv2int A) (bv2int B)) 255))
)
(check-sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 8))
(declare-const B (_ BitVec 8))
(declare-const C (_ BitVec 8))
(declare-const a Int)
(declare-const b Int)
(assert
(not
(=
(bvadd (bvadd A B) C)
(bvadd A (bvadd B C))
))
)
(check-sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 8))
(declare-const B (_ BitVec 8))
(assert
(not
(=
(bv2int (bvsub A B))
(ite
(>= (bv2int A) (bv2int B))
(- (bv2int A) (bv2int B))
(+ 256 (- (bv2int A) (bv2int B)))
)
)))
(check-sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 8))
(declare-const B (_ BitVec 8))
(assert
(not
(=
(bvadd (bvnot A) #x01)
( (_ int2bv 8) (* -1 (bv2int A)))
)))
(check-sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 8))
(declare-const B (_ BitVec 8))
(declare-const x (_ BitVec 1))
(declare-const y (_ BitVec 1))
(assert
(not
(=
((_ extract 7 0 ) (bvadd (concat x A) (concat y B)))
(bvadd A B)
)))
(check-sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (_ BitVec 8))
(declare-const B (_ BitVec 8))
(push)
(assert
(not
(=
((_ extract 3 0) (bvadd A B) )
(bvadd ((_ extract 3 0) A) ((_ extract 3 0) B))
)))
(check-sat)
(pop)
(push)
(assert
(not
(=
((_ extract 3 1) (bvadd A B) )
(bvadd ((_ extract 3 1) A) ((_ extract 3 1) B))
)))
(check-sat)
(pop)