My Z3 proof snippets

allProofs.z3

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;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)