(set-option :produce-models true) (set-option :pull-nested-quantifiers true) (set-option :mbqi true) (declare-const x (_ BitVec 23)) (declare-const y (_ BitVec 23)) (declare-const xs (_ BitVec 23)) (declare-fun T ((_ BitVec 23) (_ BitVec 23) ) bool) ; -------------- Transition Relation: ----------------- (assert (forall ((x (_ BitVec 23)) (y (_ BitVec 23)) )(= (T x y) (and (or (and (= (bvand (bvlshr x (_ bv0 23)) (_ bv1 23)) (_ bv0 23)) (or (= (bvand (bvlshr y (_ bv0 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv0 23)) (_ bv1 23)) (_ bv1 23)))) (and (= (bvand (bvlshr x (_ bv0 23)) (_ bv1 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv0 23)) (_ bv1 23)) (_ bv1 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv0 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv0 23)) (_ bv1 23)) (_ bv1 23)))) (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv0 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv0 23)) (_ bv1 23)) (_ bv1 23))) (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv1 23)) (or (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv2 23)))) (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv2 23)) (or (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv3 23)))) (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv3 23)) (or (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv4 23)))) (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (or (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23)))) (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv5 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23)))) (= (bvand (bvlshr x (_ bv4 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv4 23)) (_ bv1 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23))) (= (bvand (bvlshr x (_ bv4 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv4 23)) (_ bv1 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv4 23)) (_ bv1 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv4 23)) (_ bv1 23)) (_ bv1 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23)))) (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23))) (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (or (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23)))) (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (or (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23)))) (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (or (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23)))) (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23)))) (= (bvand (bvlshr x (_ bv8 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv8 23)) (_ bv3 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23))) (= (bvand (bvlshr x (_ bv8 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv8 23)) (_ bv3 23)) (_ bv1 23))) (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23)))) (= (bvand (bvlshr x (_ bv8 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv8 23)) (_ bv3 23)) (_ bv1 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23))) (= (bvand (bvlshr x (_ bv8 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv8 23)) (_ bv3 23)) (_ bv2 23))) (and (= (bvand (bvlshr x (_ bv8 23)) (_ bv3 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv8 23)) (_ bv3 23)) (_ bv2 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23)))) (= (bvand (bvlshr x (_ bv10 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv10 23)) (_ bv3 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23))) (= (bvand (bvlshr x (_ bv10 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv10 23)) (_ bv3 23)) (_ bv1 23))) (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23)))) (= (bvand (bvlshr x (_ bv10 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv10 23)) (_ bv3 23)) (_ bv1 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23))) (= (bvand (bvlshr x (_ bv10 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv10 23)) (_ bv3 23)) (_ bv2 23))) (and (= (bvand (bvlshr x (_ bv10 23)) (_ bv3 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv10 23)) (_ bv3 23)) (_ bv2 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23)))) (= (bvand (bvlshr x (_ bv12 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv12 23)) (_ bv3 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv1 23)) (_ bv7 23)) (_ bv4 23)) (= (bvand (bvlshr y (_ bv1 23)) (_ bv7 23)) (_ bv5 23))) (= (bvand (bvlshr x (_ bv12 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv12 23)) (_ bv3 23)) (_ bv1 23))) (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23)))) (= (bvand (bvlshr x (_ bv12 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv12 23)) (_ bv3 23)) (_ bv1 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23))) (= (bvand (bvlshr x (_ bv12 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv12 23)) (_ bv3 23)) (_ bv2 23))) (and (= (bvand (bvlshr x (_ bv12 23)) (_ bv3 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv12 23)) (_ bv3 23)) (_ bv2 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23)))) (= (bvand (bvlshr x (_ bv14 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv14 23)) (_ bv3 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23))) (= (bvand (bvlshr x (_ bv14 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv14 23)) (_ bv3 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv14 23)) (_ bv3 23)) (_ bv1 23)) (or (= (bvand (bvlshr y (_ bv14 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv14 23)) (_ bv3 23)) (_ bv2 23)))) (and (= (bvand (bvlshr x (_ bv14 23)) (_ bv3 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv14 23)) (_ bv3 23)) (_ bv2 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23)))) (= (bvand (bvlshr x (_ bv16 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv16 23)) (_ bv1 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv2 23))) (= (bvand (bvlshr x (_ bv16 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv16 23)) (_ bv1 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv16 23)) (_ bv1 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv16 23)) (_ bv1 23)) (_ bv1 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23)))) (= (bvand (bvlshr x (_ bv17 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv17 23)) (_ bv3 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23))) (= (bvand (bvlshr x (_ bv17 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv17 23)) (_ bv3 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv17 23)) (_ bv3 23)) (_ bv1 23)) (or (= (bvand (bvlshr y (_ bv17 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv17 23)) (_ bv3 23)) (_ bv2 23)))) (and (= (bvand (bvlshr x (_ bv17 23)) (_ bv3 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv17 23)) (_ bv3 23)) (_ bv2 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23)))) (= (bvand (bvlshr x (_ bv19 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv19 23)) (_ bv1 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv3 23))) (= (bvand (bvlshr x (_ bv19 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv19 23)) (_ bv1 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv19 23)) (_ bv1 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv19 23)) (_ bv1 23)) (_ bv1 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23)))) (= (bvand (bvlshr x (_ bv20 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv20 23)) (_ bv3 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23))) (= (bvand (bvlshr x (_ bv20 23)) (_ bv3 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv20 23)) (_ bv3 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv20 23)) (_ bv3 23)) (_ bv1 23)) (or (= (bvand (bvlshr y (_ bv20 23)) (_ bv3 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv20 23)) (_ bv3 23)) (_ bv2 23)))) (and (= (bvand (bvlshr x (_ bv20 23)) (_ bv3 23)) (_ bv2 23)) (= (bvand (bvlshr y (_ bv20 23)) (_ bv3 23)) (_ bv2 23)))) (or (and (not (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23)))) (= (bvand (bvlshr x (_ bv22 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv22 23)) (_ bv1 23)) (_ bv0 23))) (and (and (= (bvand (bvlshr x (_ bv5 23)) (_ bv7 23)) (_ bv3 23)) (= (bvand (bvlshr y (_ bv5 23)) (_ bv7 23)) (_ bv4 23))) (= (bvand (bvlshr x (_ bv22 23)) (_ bv1 23)) (_ bv0 23)) (= (bvand (bvlshr y (_ bv22 23)) (_ bv1 23)) (_ bv1 23))) (and (= (bvand (bvlshr x (_ bv22 23)) (_ bv1 23)) (_ bv1 23)) (= (bvand (bvlshr y (_ bv22 23)) (_ bv1 23)) (_ bv1 23)))))))) ; ------------------ END ------------------------------ (echo "Simulating model (any path):") (declare-const p0 (_ BitVec 23)) (assert (= p0 (_ bv0 23))) (declare-const p1 (_ BitVec 23)) (assert (T p0 p1)) (declare-const p2 (_ BitVec 23)) (assert (T p1 p2)) (declare-const p3 (_ BitVec 23)) (assert (T p2 p3)) (declare-const p4 (_ BitVec 23)) (assert (T p3 p4)) (declare-const p5 (_ BitVec 23)) (assert (T p4 p5)) (declare-const p6 (_ BitVec 23)) (assert (T p5 p6)) (declare-const p7 (_ BitVec 23)) (assert (T p6 p7)) (declare-const p8 (_ BitVec 23)) (assert (T p7 p8)) (declare-const p9 (_ BitVec 23)) (assert (T p8 p9)) (check-sat) (eval p0) (eval p1) (eval p2) (eval p3) (eval p4) (eval p5) (eval p6) (eval p7) (eval p8) (eval p9) (echo "Simulating model (any simple path):") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))))) ; --------------- END (Loop free)------------------ (check-sat) (eval p0) (eval p1) (eval p2) (eval p3) (eval p4) (eval p5) (eval p6) (eval p7) (eval p8) (eval p9) (get-info :all-statistics)