Bounded Model Checking

bm.rkt

#lang rosette/safe

(output-smt "/tmp/rosette")

(define-symbolic x (bitvector 4))

(define (range x)
  (if (zero? x)
      (list)
      (append (range (sub1 x)) (list x))))

(define (check-bitvector x)
  (let ([N (bv 4 4)]
        [i (box (bv 0 4))]
        [r (box (bv 0 4))])
    (for-each (lambda (_)
                (begin
                  (when (and (bvult (unbox i) N)
                             (not (bveq (bv 0 4)
                                        (bvand x
                                               (bvshl (bv 1 4) (unbox i))))))
                    (set-box! r
                              (bvadd (bvshl (bv 1 4) (unbox i))
                                     (unbox r))))
                  (when (bvult (unbox i) N)
                    (set-box! i (bvadd (bv 1 4) (unbox i))))))
              (range 32))
    (assert (bveq x (unbox r)))))

(define sol (verify (check-bitvector x)))

bm.smt2

(set-option :auto-config true)
(set-option :produce-unsat-cores false)
(set-option :smt.mbqi.max_iterations 10000000)
(set-option :smt.relevancy 2)
(reset)
(set-option :auto-config true)
(set-option :produce-unsat-cores false)
(set-option :smt.mbqi.max_iterations 10000000)
(set-option :smt.relevancy 2)
(declare-fun c0 () (_ BitVec 4))
(define-fun e1 () (_ BitVec 4) (_ bv0 4))
(define-fun e2 () (_ BitVec 4) (bvneg (_ bv8 4)))
(define-fun e3 () (_ BitVec 4) (bvand e2 c0))
(define-fun e4 () Bool (= e1 e3))
(define-fun e5 () (_ BitVec 4) (_ bv4 4))
(define-fun e6 () (_ BitVec 4) (bvand e5 c0))
(define-fun e7 () Bool (= e1 e6))
(define-fun e8 () (_ BitVec 4) (_ bv2 4))
(define-fun e9 () (_ BitVec 4) (bvand e8 c0))
(define-fun e10 () Bool (= e1 e9))
(define-fun e11 () (_ BitVec 4) (_ bv1 4))
(define-fun e12 () (_ BitVec 4) (bvand e11 c0))
(define-fun e13 () Bool (= e1 e12))
(define-fun e14 () (_ BitVec 4) (ite e13 e1 e11))
(define-fun e15 () (_ BitVec 4) (_ bv3 4))
(define-fun e16 () (_ BitVec 4) (ite e13 e8 e15))
(define-fun e17 () (_ BitVec 4) (ite e10 e14 e16))
(define-fun e18 () (_ BitVec 4) (bvadd e5 e17))
(define-fun e19 () (_ BitVec 4) (ite e7 e17 e18))
(define-fun e20 () (_ BitVec 4) (bvadd e2 e19))
(define-fun e21 () (_ BitVec 4) (ite e4 e19 e20))
(define-fun e22 () Bool (= c0 e21))
(define-fun e23 () Bool (not e22))
(assert e23)
(check-sat)
(reset)
(set-option :auto-config true)
(set-option :produce-unsat-cores false)
(set-option :smt.mbqi.max_iterations 10000000)
(set-option :smt.relevancy 2)