(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)
(declare-const x (_ BitVec 3))
(declare-const y (_ BitVec 3))
(declare-const xs (_ BitVec 3))
; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\toy2.cnet--------
(declare-fun T ((_ BitVec 3) (_ BitVec 3) ) bool)
; -------------- Transition Relation: -----------------
(assert (forall ((x (_ BitVec 3)) (y (_ BitVec 3))
  )(= (T x y)
     (and (= (= ((_ extract 0 0) y) (_ bv1 1))
             (or (and (= ((_ extract 0 0) x) (_ bv1 1))
                      (not (= ((_ extract 1 1) x) (_ bv1 1)))
                      (not (= ((_ extract 2 2) x) (_ bv1 1))))
                 (and (not (= ((_ extract 0 0) x) (_ bv1 1)))
                      (= ((_ extract 1 1) x) (_ bv1 1))
                      (not (= ((_ extract 2 2) x) (_ bv1 1))))
                 (and (= ((_ extract 0 0) x) (_ bv1 1))
                      (= ((_ extract 1 1) x) (_ bv1 1))
                      (not (= ((_ extract 2 2) x) (_ bv1 1))))))
          (= (= ((_ extract 1 1) y) (_ bv1 1))
             (or (and (= ((_ extract 0 0) x) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1)))))
          (= (= ((_ extract 2 2) y) (_ bv1 1))
             (or (and (= ((_ extract 0 0) x) (_ bv1 1))
                      (= ((_ extract 1 1) x) (_ bv1 1))
                      (= ((_ extract 2 2) x) (_ bv1 1)))
                 (and (= ((_ extract 0 0) x) (_ bv1 1))
                      (= ((_ extract 1 1) x) (_ bv1 1))
                      (not (= ((_ extract 2 2) x) (_ bv1 1))))
                 (and (not (= ((_ extract 0 0) x) (_ bv1 1)))
                      (= ((_ extract 1 1) x) (_ bv1 1))
                      (not (= ((_ extract 2 2) x) (_ bv1 1))))
                 (and (= ((_ extract 0 0) x) (_ bv1 1))
                      (not (= ((_ extract 1 1) x) (_ bv1 1)))
                      (not (= ((_ extract 2 2) x) (_ bv1 1))))
                 (and (not (= ((_ extract 0 0) x) (_ bv1 1)))
                      (not (= ((_ extract 1 1) x) (_ bv1 1)))
                      (not (= ((_ extract 2 2) x) (_ bv1 1))))))))))
; ------------------ END ------------------------------
(echo "Testing the stability of model toy2")
(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 3))
(declare-const p1 (_ BitVec 3))
(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)
(get-info :all-statistics)