Small bounded model checking demo example in Z3

gen.rkt

#lang racket

;; CIS700, Fall 2023 -- Kris Micinski
;; 
;; Demo of SMT (SMTLIB) to perform bounded-model checking for an example
;; program.
;; 
;;  // input x, a bit vector of length N
;;  i = 0;
;;  r = 0;
;;  while(i < N) {
;;    if (x & 1<<i) { r += 1<<i; }
;;    i++;
;;  }
;;  assert( r == x );
;; 
;; This program generates SMTLIB output. Run its output using Z3/CVC5/...

(define c (make-hash))
(define preamble "(set-logic QF_BV)\n(declare-const x (_ BitVec 4))\n")

(define (gimme x)
  (define v (hash-ref c x 0))
  (hash-set! c x (add1 v))
  (let ([name (format "~a_~a" x v)])
    (set! preamble (string-append preamble 
                                  (format "(declare-const ~a (_ BitVec 4))\n" name)))
    (string->symbol name)))

(define output-port (open-output-string))
(parameterize ([current-output-port output-port])
  (define r (gimme 'r))
  (define i (gimme 'i))
  (define N (gimme 'N))
  (pretty-display `(assert (= ,N (_ bv4 4))))
  (pretty-display `(assert (= ,i (_ bv0 4))))
  (pretty-display `(assert (= ,r (_ bv0 4))))


  (for ([iteration (range 32)])
    (let ([r_1 (gimme 'r)]
          [r_2 (gimme 'r)]
          [i_1 (gimme 'i)]
          [i_2 (gimme 'i)])
      (pretty-display
       `(assert (= ,r_1 (bvadd ,r (bvshl ,(string->symbol "#x1") ,i)))))
      (pretty-display
       `(assert (= ,r_2 (ite (and (bvult ,i ,N)
                                  (not (= (_ bv0 4) (bvand x (bvshl ,(string->symbol "#x1") ,i)))))
                             ,r_1
                             ,r))))
      (pretty-display
       `(assert (= ,i_1 (bvadd ,i (_ bv1 4)))))
      (pretty-display `(assert (= ,i_2 (ite (bvult ,i ,N) ,i_1 ,i))))
      (set! r r_2)

      (set! i i_2)))

  (pretty-display `(assert (not (= x ,r))))
  (pretty-display '(check-sat))
  (pretty-display '(get-model)))

(display (string-append preamble (get-output-string output-port))) 

shift32.smt

(set-logic QF_BV)
(declare-const x (_ BitVec 4))
(declare-const r_0 (_ BitVec 4))
(declare-const i_0 (_ BitVec 4))
(declare-const N_0 (_ BitVec 4))
(declare-const r_1 (_ BitVec 4))
(declare-const r_2 (_ BitVec 4))
(declare-const i_1 (_ BitVec 4))
(declare-const i_2 (_ BitVec 4))
(declare-const r_3 (_ BitVec 4))
(declare-const r_4 (_ BitVec 4))
(declare-const i_3 (_ BitVec 4))
(declare-const i_4 (_ BitVec 4))
(declare-const r_5 (_ BitVec 4))
(declare-const r_6 (_ BitVec 4))
(declare-const i_5 (_ BitVec 4))
(declare-const i_6 (_ BitVec 4))
(declare-const r_7 (_ BitVec 4))
(declare-const r_8 (_ BitVec 4))
(declare-const i_7 (_ BitVec 4))
(declare-const i_8 (_ BitVec 4))
(declare-const r_9 (_ BitVec 4))
(declare-const r_10 (_ BitVec 4))
(declare-const i_9 (_ BitVec 4))
(declare-const i_10 (_ BitVec 4))
(declare-const r_11 (_ BitVec 4))
(declare-const r_12 (_ BitVec 4))
(declare-const i_11 (_ BitVec 4))
(declare-const i_12 (_ BitVec 4))
(declare-const r_13 (_ BitVec 4))
(declare-const r_14 (_ BitVec 4))
(declare-const i_13 (_ BitVec 4))
(declare-const i_14 (_ BitVec 4))
(declare-const r_15 (_ BitVec 4))
(declare-const r_16 (_ BitVec 4))
(declare-const i_15 (_ BitVec 4))
(declare-const i_16 (_ BitVec 4))
(declare-const r_17 (_ BitVec 4))
(declare-const r_18 (_ BitVec 4))
(declare-const i_17 (_ BitVec 4))
(declare-const i_18 (_ BitVec 4))
(declare-const r_19 (_ BitVec 4))
(declare-const r_20 (_ BitVec 4))
(declare-const i_19 (_ BitVec 4))
(declare-const i_20 (_ BitVec 4))
(declare-const r_21 (_ BitVec 4))
(declare-const r_22 (_ BitVec 4))
(declare-const i_21 (_ BitVec 4))
(declare-const i_22 (_ BitVec 4))
(declare-const r_23 (_ BitVec 4))
(declare-const r_24 (_ BitVec 4))
(declare-const i_23 (_ BitVec 4))
(declare-const i_24 (_ BitVec 4))
(declare-const r_25 (_ BitVec 4))
(declare-const r_26 (_ BitVec 4))
(declare-const i_25 (_ BitVec 4))
(declare-const i_26 (_ BitVec 4))
(declare-const r_27 (_ BitVec 4))
(declare-const r_28 (_ BitVec 4))
(declare-const i_27 (_ BitVec 4))
(declare-const i_28 (_ BitVec 4))
(declare-const r_29 (_ BitVec 4))
(declare-const r_30 (_ BitVec 4))
(declare-const i_29 (_ BitVec 4))
(declare-const i_30 (_ BitVec 4))
(declare-const r_31 (_ BitVec 4))
(declare-const r_32 (_ BitVec 4))
(declare-const i_31 (_ BitVec 4))
(declare-const i_32 (_ BitVec 4))
(declare-const r_33 (_ BitVec 4))
(declare-const r_34 (_ BitVec 4))
(declare-const i_33 (_ BitVec 4))
(declare-const i_34 (_ BitVec 4))
(declare-const r_35 (_ BitVec 4))
(declare-const r_36 (_ BitVec 4))
(declare-const i_35 (_ BitVec 4))
(declare-const i_36 (_ BitVec 4))
(declare-const r_37 (_ BitVec 4))
(declare-const r_38 (_ BitVec 4))
(declare-const i_37 (_ BitVec 4))
(declare-const i_38 (_ BitVec 4))
(declare-const r_39 (_ BitVec 4))
(declare-const r_40 (_ BitVec 4))
(declare-const i_39 (_ BitVec 4))
(declare-const i_40 (_ BitVec 4))
(declare-const r_41 (_ BitVec 4))
(declare-const r_42 (_ BitVec 4))
(declare-const i_41 (_ BitVec 4))
(declare-const i_42 (_ BitVec 4))
(declare-const r_43 (_ BitVec 4))
(declare-const r_44 (_ BitVec 4))
(declare-const i_43 (_ BitVec 4))
(declare-const i_44 (_ BitVec 4))
(declare-const r_45 (_ BitVec 4))
(declare-const r_46 (_ BitVec 4))
(declare-const i_45 (_ BitVec 4))
(declare-const i_46 (_ BitVec 4))
(declare-const r_47 (_ BitVec 4))
(declare-const r_48 (_ BitVec 4))
(declare-const i_47 (_ BitVec 4))
(declare-const i_48 (_ BitVec 4))
(declare-const r_49 (_ BitVec 4))
(declare-const r_50 (_ BitVec 4))
(declare-const i_49 (_ BitVec 4))
(declare-const i_50 (_ BitVec 4))
(declare-const r_51 (_ BitVec 4))
(declare-const r_52 (_ BitVec 4))
(declare-const i_51 (_ BitVec 4))
(declare-const i_52 (_ BitVec 4))
(declare-const r_53 (_ BitVec 4))
(declare-const r_54 (_ BitVec 4))
(declare-const i_53 (_ BitVec 4))
(declare-const i_54 (_ BitVec 4))
(declare-const r_55 (_ BitVec 4))
(declare-const r_56 (_ BitVec 4))
(declare-const i_55 (_ BitVec 4))
(declare-const i_56 (_ BitVec 4))
(declare-const r_57 (_ BitVec 4))
(declare-const r_58 (_ BitVec 4))
(declare-const i_57 (_ BitVec 4))
(declare-const i_58 (_ BitVec 4))
(declare-const r_59 (_ BitVec 4))
(declare-const r_60 (_ BitVec 4))
(declare-const i_59 (_ BitVec 4))
(declare-const i_60 (_ BitVec 4))
(declare-const r_61 (_ BitVec 4))
(declare-const r_62 (_ BitVec 4))
(declare-const i_61 (_ BitVec 4))
(declare-const i_62 (_ BitVec 4))
(declare-const r_63 (_ BitVec 4))
(declare-const r_64 (_ BitVec 4))
(declare-const i_63 (_ BitVec 4))
(declare-const i_64 (_ BitVec 4))
(assert (= N_0 (_ bv4 4)))
(assert (= i_0 (_ bv0 4)))
(assert (= r_0 (_ bv0 4)))
(assert (= r_1 (bvadd r_0 (bvshl #x1 i_0))))
(assert
 (=
  r_2
  (ite
   (and (bvult i_0 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_0)))))
   r_1
   r_0)))
(assert (= i_1 (bvadd i_0 (_ bv1 4))))
(assert (= i_2 (ite (bvult i_0 N_0) i_1 i_0)))
(assert (= r_3 (bvadd r_2 (bvshl #x1 i_2))))
(assert
 (=
  r_4
  (ite
   (and (bvult i_2 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_2)))))
   r_3
   r_2)))
(assert (= i_3 (bvadd i_2 (_ bv1 4))))
(assert (= i_4 (ite (bvult i_2 N_0) i_3 i_2)))
(assert (= r_5 (bvadd r_4 (bvshl #x1 i_4))))
(assert
 (=
  r_6
  (ite
   (and (bvult i_4 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_4)))))
   r_5
   r_4)))
(assert (= i_5 (bvadd i_4 (_ bv1 4))))
(assert (= i_6 (ite (bvult i_4 N_0) i_5 i_4)))
(assert (= r_7 (bvadd r_6 (bvshl #x1 i_6))))
(assert
 (=
  r_8
  (ite
   (and (bvult i_6 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_6)))))
   r_7
   r_6)))
(assert (= i_7 (bvadd i_6 (_ bv1 4))))
(assert (= i_8 (ite (bvult i_6 N_0) i_7 i_6)))
(assert (= r_9 (bvadd r_8 (bvshl #x1 i_8))))
(assert
 (=
  r_10
  (ite
   (and (bvult i_8 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_8)))))
   r_9
   r_8)))
(assert (= i_9 (bvadd i_8 (_ bv1 4))))
(assert (= i_10 (ite (bvult i_8 N_0) i_9 i_8)))
(assert (= r_11 (bvadd r_10 (bvshl #x1 i_10))))
(assert
 (=
  r_12
  (ite
   (and (bvult i_10 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_10)))))
   r_11
   r_10)))
(assert (= i_11 (bvadd i_10 (_ bv1 4))))
(assert (= i_12 (ite (bvult i_10 N_0) i_11 i_10)))
(assert (= r_13 (bvadd r_12 (bvshl #x1 i_12))))
(assert
 (=
  r_14
  (ite
   (and (bvult i_12 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_12)))))
   r_13
   r_12)))
(assert (= i_13 (bvadd i_12 (_ bv1 4))))
(assert (= i_14 (ite (bvult i_12 N_0) i_13 i_12)))
(assert (= r_15 (bvadd r_14 (bvshl #x1 i_14))))
(assert
 (=
  r_16
  (ite
   (and (bvult i_14 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_14)))))
   r_15
   r_14)))
(assert (= i_15 (bvadd i_14 (_ bv1 4))))
(assert (= i_16 (ite (bvult i_14 N_0) i_15 i_14)))
(assert (= r_17 (bvadd r_16 (bvshl #x1 i_16))))
(assert
 (=
  r_18
  (ite
   (and (bvult i_16 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_16)))))
   r_17
   r_16)))
(assert (= i_17 (bvadd i_16 (_ bv1 4))))
(assert (= i_18 (ite (bvult i_16 N_0) i_17 i_16)))
(assert (= r_19 (bvadd r_18 (bvshl #x1 i_18))))
(assert
 (=
  r_20
  (ite
   (and (bvult i_18 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_18)))))
   r_19
   r_18)))
(assert (= i_19 (bvadd i_18 (_ bv1 4))))
(assert (= i_20 (ite (bvult i_18 N_0) i_19 i_18)))
(assert (= r_21 (bvadd r_20 (bvshl #x1 i_20))))
(assert
 (=
  r_22
  (ite
   (and (bvult i_20 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_20)))))
   r_21
   r_20)))
(assert (= i_21 (bvadd i_20 (_ bv1 4))))
(assert (= i_22 (ite (bvult i_20 N_0) i_21 i_20)))
(assert (= r_23 (bvadd r_22 (bvshl #x1 i_22))))
(assert
 (=
  r_24
  (ite
   (and (bvult i_22 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_22)))))
   r_23
   r_22)))
(assert (= i_23 (bvadd i_22 (_ bv1 4))))
(assert (= i_24 (ite (bvult i_22 N_0) i_23 i_22)))
(assert (= r_25 (bvadd r_24 (bvshl #x1 i_24))))
(assert
 (=
  r_26
  (ite
   (and (bvult i_24 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_24)))))
   r_25
   r_24)))
(assert (= i_25 (bvadd i_24 (_ bv1 4))))
(assert (= i_26 (ite (bvult i_24 N_0) i_25 i_24)))
(assert (= r_27 (bvadd r_26 (bvshl #x1 i_26))))
(assert
 (=
  r_28
  (ite
   (and (bvult i_26 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_26)))))
   r_27
   r_26)))
(assert (= i_27 (bvadd i_26 (_ bv1 4))))
(assert (= i_28 (ite (bvult i_26 N_0) i_27 i_26)))
(assert (= r_29 (bvadd r_28 (bvshl #x1 i_28))))
(assert
 (=
  r_30
  (ite
   (and (bvult i_28 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_28)))))
   r_29
   r_28)))
(assert (= i_29 (bvadd i_28 (_ bv1 4))))
(assert (= i_30 (ite (bvult i_28 N_0) i_29 i_28)))
(assert (= r_31 (bvadd r_30 (bvshl #x1 i_30))))
(assert
 (=
  r_32
  (ite
   (and (bvult i_30 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_30)))))
   r_31
   r_30)))
(assert (= i_31 (bvadd i_30 (_ bv1 4))))
(assert (= i_32 (ite (bvult i_30 N_0) i_31 i_30)))
(assert (= r_33 (bvadd r_32 (bvshl #x1 i_32))))
(assert
 (=
  r_34
  (ite
   (and (bvult i_32 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_32)))))
   r_33
   r_32)))
(assert (= i_33 (bvadd i_32 (_ bv1 4))))
(assert (= i_34 (ite (bvult i_32 N_0) i_33 i_32)))
(assert (= r_35 (bvadd r_34 (bvshl #x1 i_34))))
(assert
 (=
  r_36
  (ite
   (and (bvult i_34 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_34)))))
   r_35
   r_34)))
(assert (= i_35 (bvadd i_34 (_ bv1 4))))
(assert (= i_36 (ite (bvult i_34 N_0) i_35 i_34)))
(assert (= r_37 (bvadd r_36 (bvshl #x1 i_36))))
(assert
 (=
  r_38
  (ite
   (and (bvult i_36 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_36)))))
   r_37
   r_36)))
(assert (= i_37 (bvadd i_36 (_ bv1 4))))
(assert (= i_38 (ite (bvult i_36 N_0) i_37 i_36)))
(assert (= r_39 (bvadd r_38 (bvshl #x1 i_38))))
(assert
 (=
  r_40
  (ite
   (and (bvult i_38 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_38)))))
   r_39
   r_38)))
(assert (= i_39 (bvadd i_38 (_ bv1 4))))
(assert (= i_40 (ite (bvult i_38 N_0) i_39 i_38)))
(assert (= r_41 (bvadd r_40 (bvshl #x1 i_40))))
(assert
 (=
  r_42
  (ite
   (and (bvult i_40 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_40)))))
   r_41
   r_40)))
(assert (= i_41 (bvadd i_40 (_ bv1 4))))
(assert (= i_42 (ite (bvult i_40 N_0) i_41 i_40)))
(assert (= r_43 (bvadd r_42 (bvshl #x1 i_42))))
(assert
 (=
  r_44
  (ite
   (and (bvult i_42 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_42)))))
   r_43
   r_42)))
(assert (= i_43 (bvadd i_42 (_ bv1 4))))
(assert (= i_44 (ite (bvult i_42 N_0) i_43 i_42)))
(assert (= r_45 (bvadd r_44 (bvshl #x1 i_44))))
(assert
 (=
  r_46
  (ite
   (and (bvult i_44 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_44)))))
   r_45
   r_44)))
(assert (= i_45 (bvadd i_44 (_ bv1 4))))
(assert (= i_46 (ite (bvult i_44 N_0) i_45 i_44)))
(assert (= r_47 (bvadd r_46 (bvshl #x1 i_46))))
(assert
 (=
  r_48
  (ite
   (and (bvult i_46 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_46)))))
   r_47
   r_46)))
(assert (= i_47 (bvadd i_46 (_ bv1 4))))
(assert (= i_48 (ite (bvult i_46 N_0) i_47 i_46)))
(assert (= r_49 (bvadd r_48 (bvshl #x1 i_48))))
(assert
 (=
  r_50
  (ite
   (and (bvult i_48 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_48)))))
   r_49
   r_48)))
(assert (= i_49 (bvadd i_48 (_ bv1 4))))
(assert (= i_50 (ite (bvult i_48 N_0) i_49 i_48)))
(assert (= r_51 (bvadd r_50 (bvshl #x1 i_50))))
(assert
 (=
  r_52
  (ite
   (and (bvult i_50 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_50)))))
   r_51
   r_50)))
(assert (= i_51 (bvadd i_50 (_ bv1 4))))
(assert (= i_52 (ite (bvult i_50 N_0) i_51 i_50)))
(assert (= r_53 (bvadd r_52 (bvshl #x1 i_52))))
(assert
 (=
  r_54
  (ite
   (and (bvult i_52 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_52)))))
   r_53
   r_52)))
(assert (= i_53 (bvadd i_52 (_ bv1 4))))
(assert (= i_54 (ite (bvult i_52 N_0) i_53 i_52)))
(assert (= r_55 (bvadd r_54 (bvshl #x1 i_54))))
(assert
 (=
  r_56
  (ite
   (and (bvult i_54 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_54)))))
   r_55
   r_54)))
(assert (= i_55 (bvadd i_54 (_ bv1 4))))
(assert (= i_56 (ite (bvult i_54 N_0) i_55 i_54)))
(assert (= r_57 (bvadd r_56 (bvshl #x1 i_56))))
(assert
 (=
  r_58
  (ite
   (and (bvult i_56 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_56)))))
   r_57
   r_56)))
(assert (= i_57 (bvadd i_56 (_ bv1 4))))
(assert (= i_58 (ite (bvult i_56 N_0) i_57 i_56)))
(assert (= r_59 (bvadd r_58 (bvshl #x1 i_58))))
(assert
 (=
  r_60
  (ite
   (and (bvult i_58 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_58)))))
   r_59
   r_58)))
(assert (= i_59 (bvadd i_58 (_ bv1 4))))
(assert (= i_60 (ite (bvult i_58 N_0) i_59 i_58)))
(assert (= r_61 (bvadd r_60 (bvshl #x1 i_60))))
(assert
 (=
  r_62
  (ite
   (and (bvult i_60 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_60)))))
   r_61
   r_60)))
(assert (= i_61 (bvadd i_60 (_ bv1 4))))
(assert (= i_62 (ite (bvult i_60 N_0) i_61 i_60)))
(assert (= r_63 (bvadd r_62 (bvshl #x1 i_62))))
(assert
 (=
  r_64
  (ite
   (and (bvult i_62 N_0) (not (= (_ bv0 4) (bvand x (bvshl #x1 i_62)))))
   r_63
   r_62)))
(assert (= i_63 (bvadd i_62 (_ bv1 4))))
(assert (= i_64 (ite (bvult i_62 N_0) i_63 i_62)))
(assert (not (= x r_64)))
(check-sat)
(get-model)