(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))
; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\thelper.cnet--------
(declare-fun T ((_ BitVec 23) (_ BitVec 23) ) bool)
; -------------- Transition Relation: -----------------
(assert (forall ((x (_ BitVec 23)) (y (_ BitVec 23))
  )(= (T x y)
     (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (or false))
          (= (= ((_ extract 1 1) y) (_ bv1 1)) (or (and (= ((_ extract 0 0) x) (_ bv1 1)))))
          (= (= ((_ extract 2 2) y) (_ bv1 1)) (or false))
          (= (= ((_ extract 3 3) y) (_ bv1 1)) (or (and (= ((_ extract 2 2) x) (_ bv1 1)))))
          (= (= ((_ extract 4 4) y) (_ bv1 1)) (or false))
          (= (= ((_ extract 5 5) y) (_ bv1 1))
             (or (and (= ((_ extract 4 4) x) (_ bv1 1))
                      (not (= ((_ extract 18 18) x) (_ bv1 1))))))
          (= (= ((_ extract 6 6) y) (_ bv1 1)) (or (and (= ((_ extract 5 5) x) (_ bv1 1)))))
          (= (= ((_ extract 7 7) y) (_ bv1 1))
             (or (and (= ((_ extract 15 15) x) (_ bv1 1)))
                 (and (= ((_ extract 11 11) x) (_ bv1 1)))))
          (= (= ((_ extract 8 8) y) (_ bv1 1)) (or false))
          (= (= ((_ extract 9 9) y) (_ bv1 1))
             (or (and (= ((_ extract 8 8) x) (_ bv1 1))
                      (not (= ((_ extract 18 18) x) (_ bv1 1))))))
          (= (= ((_ extract 10 10) y) (_ bv1 1))
             (or (and (= ((_ extract 9 9) x) (_ bv1 1))
                      (not (= ((_ extract 19 19) x) (_ bv1 1))))))
          (= (= ((_ extract 11 11) y) (_ bv1 1))
             (or (and (= ((_ extract 15 15) x) (_ bv1 1))
                      (not (= ((_ extract 19 19) x) (_ bv1 1))))
                 (and (= ((_ extract 11 11) x) (_ bv1 1))
                      (not (= ((_ extract 19 19) x) (_ bv1 1))))))
          (= (= ((_ extract 12 12) y) (_ bv1 1))
             (or (and (= ((_ extract 11 11) x) (_ bv1 1))
                      (not (= ((_ extract 22 22) x) (_ bv1 1))))
                 (and (= ((_ extract 10 10) x) (_ bv1 1))
                      (not (= ((_ extract 22 22) x) (_ bv1 1))))
                 (and (= ((_ extract 6 6) x) (_ bv1 1))
                      (not (= ((_ extract 22 22) x) (_ bv1 1))))
                 (and (= ((_ extract 1 1) x) (_ bv1 1))
                      (not (= ((_ extract 22 22) x) (_ bv1 1))))))
          (= (= ((_ extract 13 13) y) (_ bv1 1))
             (or (and (= ((_ extract 12 12) x) (_ bv1 1)))))
          (= (= ((_ extract 14 14) y) (_ bv1 1))
             (or (and (= ((_ extract 13 13) x) (_ bv1 1))
                      (not (= ((_ extract 7 7) x) (_ bv1 1))))))
          (= (= ((_ extract 15 15) y) (_ bv1 1))
             (or (and (= ((_ extract 14 14) x) (_ bv1 1)))
                 (and (= ((_ extract 3 3) x) (_ bv1 1)))))
          (= (= ((_ extract 16 16) y) (_ bv1 1))
             (or (and (= ((_ extract 19 19) x) (_ bv1 1))
                      (not (= ((_ extract 15 15) x) (_ bv1 1))))))
          (= (= ((_ extract 17 17) y) (_ bv1 1))
             (or (and (= ((_ extract 16 16) x) (_ bv1 1))
                      (not (= ((_ extract 7 7) x) (_ bv1 1))))))
          (= (= ((_ extract 18 18) y) (_ bv1 1))
             (or (and (= ((_ extract 17 17) x) (_ bv1 1)))))
          (= (= ((_ extract 19 19) y) (_ bv1 1))
             (or (and (= ((_ extract 19 19) x) (_ bv1 1))
                      (not (= ((_ extract 11 11) x) (_ bv1 1))))
                 (and (= ((_ extract 18 18) x) (_ bv1 1))
                      (not (= ((_ extract 11 11) x) (_ bv1 1))))))
          (= (= ((_ extract 20 20) y) (_ bv1 1))
             (or (and (= ((_ extract 19 19) x) (_ bv1 1)))))
          (= (= ((_ extract 21 21) y) (_ bv1 1))
             (or (and (= ((_ extract 20 20) x) (_ bv1 1)))))
          (= (= ((_ extract 22 22) y) (_ bv1 1))
             (or (and (= ((_ extract 21 21) x) (_ bv1 1)))))))))
; ------------------ END ------------------------------
(echo "Testing the stability of model thelper")
(echo "-----------------------------------------------------------")
(echo "Is the system non-deterministic?")
(push)
(assert (and (T x y) (T x xs) (not (= y xs))))
(check-sat)
(pop)
(declare-const p0 (_ BitVec 23))
(declare-const p1 (_ BitVec 23))
(assert (T p0 p1))
(echo "Is oscillation possible (k=1)?")
(push)
(assert (not (T p1 p1)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=1)?")
(push)
(assert (T p1 p1))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=1)?")
; ---------- Loop Free: ---------------
(assert (and (and (not (= p1 p0)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p2 (_ BitVec 23))
(assert (T p1 p2))
(echo "Is oscillation possible (k=2)?")
(push)
(assert (not (T p2 p2)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=2)?")
(push)
(assert (T p2 p2))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=2)?")
; ---------- Loop Free: ---------------
(assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p3 (_ BitVec 23))
(assert (T p2 p3))
(echo "Is oscillation possible (k=3)?")
(push)
(assert (not (T p3 p3)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=3)?")
(push)
(assert (T p3 p3))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=3)?")
; ---------- 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)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p4 (_ BitVec 23))
(assert (T p3 p4))
(echo "Is oscillation possible (k=4)?")
(push)
(assert (not (T p4 p4)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=4)?")
(push)
(assert (T p4 p4))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=4)?")
; ---------- 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)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p5 (_ BitVec 23))
(assert (T p4 p5))
(echo "Is oscillation possible (k=5)?")
(push)
(assert (not (T p5 p5)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=5)?")
(push)
(assert (T p5 p5))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=5)?")
; ---------- 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)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p6 (_ BitVec 23))
(assert (T p5 p6))
(echo "Is oscillation possible (k=6)?")
(push)
(assert (not (T p6 p6)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=6)?")
(push)
(assert (T p6 p6))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=6)?")
; ---------- 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)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p7 (_ BitVec 23))
(assert (T p6 p7))
(echo "Is oscillation possible (k=7)?")
(push)
(assert (not (T p7 p7)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=7)?")
(push)
(assert (T p7 p7))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=7)?")
; ---------- 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)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p8 (_ BitVec 23))
(assert (T p7 p8))
(echo "Is oscillation possible (k=8)?")
(push)
(assert (not (T p8 p8)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=8)?")
(push)
(assert (T p8 p8))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=8)?")
; ---------- 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)))))
; --------------- END (Loop free)------------------
(check-sat)
(pop)
(declare-const p9 (_ BitVec 23))
(assert (T p8 p9))
(echo "Is oscillation possible (k=9)?")
(push)
(assert (not (T p9 p9)))
(check-sat)
(pop)
(echo "Is stabilization possible (k=9)?")
(push)
(assert (T p9 p9))
(check-sat)
(pop)
(push)
(echo "Can a simple path be generated (k=9)?")
; ---------- 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)
(pop)
(declare-const p10 (_ BitVec 23))
(assert (T p9 p10))
(echo "Is oscillation possible (k=10)?")
(push)
(assert (not (T p10 p10)))
(check-sat)
(pop)
(get-info :all-statistics)