SMT-LIBv2 formula with classical and Flanagan & Saxe style weakest preconditions

new_wp_z3.smt

(set-logic QF_UFBV)

; This push is essential for our problem:
; It forces Z3 to use the "solver 2", which is used in our application
(push)

(declare-fun register-call () (_ BitVec 8))
(declare-fun register-b () (_ BitVec 8))
(declare-fun register-a () (_ BitVec 8))
(declare-fun register-conv () (_ BitVec 8))
(declare-fun pred () Bool)
(declare-fun register-b-0-0-1 () (_ BitVec 8))
(declare-fun register-a-0-0-1 () (_ BitVec 8))
(declare-fun register-conv-0-0-1 () (_ BitVec 8))
(assert (let ((a!1 (bvsle ((_ extract 7 0)
                    (bvsrem ((_ sign_extend 24) register-a)
                            ((_ sign_extend 24) register-b)))
                  register-call))
      (a!2 ((_ sign_extend 24)
             ((_ extract 7 0)
               (bvsrem ((_ sign_extend 24) register-a)
                       ((_ sign_extend 24) register-b)))))
      (a!4 (= ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-a)
                        ((_ sign_extend 24) register-b)))
              #x00)))
(let ((a!3 (= ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-conv) a!2))
              #x00)))
  (=> pred (or a!1 (not a!3) a!4 (bvsle register-call #x00))))))
(assert (let ((a!1 (= ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-a)
                        ((_ sign_extend 24) register-b)))
              #x00))
      (a!2 (= register-b-0-0-1
              ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-a)
                        ((_ sign_extend 24) register-b)))))
      (a!3 (= register-conv-0-0-1
              ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-conv)
                        ((_ sign_extend 24) register-b-0-0-1)))))
      (a!4 ((_ sign_extend 24)
             ((_ extract 7 0)
               (bvsrem ((_ sign_extend 24) register-a-0-0-1)
                       ((_ sign_extend 24) register-b-0-0-1))))))
(let ((a!5 (bvsle ((_ extract 7 0)
                    (bvsrem ((_ sign_extend 24) register-conv-0-0-1)
                            a!4))
                  register-call))
      (a!6 (= ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-conv-0-0-1) a!4))
              #x00)))
(let ((a!7 (or (not pred)
               (not (and (not a!1)
                         a!2
                         (= register-a-0-0-1
                            register-conv)
                         a!3))
               a!5
               a!6
               (bvsle register-call #x00))))
  (not a!7)))))

(check-sat)

old_wp_z3.smt

(set-logic QF_UFBV)

; This push is essential for our problem:
; It forces Z3 to use the "solver 2", which is used in our application
(push)

(declare-fun register-call () (_ BitVec 8))
(declare-fun register-b () (_ BitVec 8))
(declare-fun register-a () (_ BitVec 8))
(declare-fun register-conv () (_ BitVec 8))
(declare-fun pred () Bool)
(assert (let ((a!1 (bvsle ((_ extract 7 0)
                    (bvsrem ((_ sign_extend 24) register-a)
                            ((_ sign_extend 24) register-b)))
                  register-call))
      (a!2 ((_ sign_extend 24)
             ((_ extract 7 0)
               (bvsrem ((_ sign_extend 24) register-a)
                       ((_ sign_extend 24) register-b)))))
      (a!4 (= ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-a)
                        ((_ sign_extend 24) register-b)))
              #x00)))
(let ((a!3 (= ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-conv) a!2))
              #x00)))
  (=> pred (or a!1 (not a!3) a!4 (bvsle register-call #x00))))))
(assert (let ((a!1 (= ((_ extract 7 0)
                (bvsrem ((_ sign_extend 24) register-a)
                        ((_ sign_extend 24) register-b)))
              #x00))
      (a!2 ((_ sign_extend 24)
             ((_ extract 7 0)
               (bvsrem ((_ sign_extend 24) register-a)
                       ((_ sign_extend 24) register-b))))))
(let ((a!3 ((_ sign_extend 24)
             ((_ extract 7 0)
               (bvsrem ((_ sign_extend 24) register-conv) a!2)))))
(let ((a!4 (or (not pred)
               a!1
               (bvsle ((_ extract 7 0) (bvsrem a!3 a!3)) register-call)
               (= ((_ extract 7 0) (bvsrem a!3 a!3)) #x00)
               (bvsle register-call #x00))))
  (not a!4)))))

(check-sat)