(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
(declare-const xs (_ BitVec 4))
; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\toy3.cnet--------
(declare-fun T ((_ BitVec 4) (_ BitVec 4) ) bool)
; -------------- Transition Relation: -----------------
(assert (forall ((x (_ BitVec 4)) (y (_ BitVec 4))
  )(= (T x y)
     (and (= (= ((_ extract 0 0) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 0 0) x) (_ bv1 1)))))
                  (not (= ((_ extract 2 2) x) (_ bv1 1)))))
          (= (= ((_ extract 1 1) y) (_ bv1 1))
             (and (or (and (= ((_ extract 0 0) x) (_ bv1 1))))
                  (not (= ((_ extract 3 3) x) (_ bv1 1)))))
          (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1)))
          (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1)))))))
; ------------------ END ------------------------------
(push)
(declare-const p10 (_ BitVec 4))
(declare-const p11 (_ BitVec 4))
(declare-const p12 (_ BitVec 4))
(declare-const p13 (_ BitVec 4))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11) (T p11 p12) (T p12 p13)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 4))
(declare-const p21 (_ BitVec 4))
(declare-const p22 (_ BitVec 4))
(declare-const p23 (_ BitVec 4))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21) (T p21 p22) (T p22 p23)))
; --------------- END (Path)------------------
(assert (= ((_ extract 1 0) p10) ((_ extract 1 0) p20)))
(assert (= ((_ extract 3 2) p10) (_ bv0 2)))
(assert (= ((_ extract 3 2) p20) (_ bv1 2)))
(assert (or (and (T p13 p13) (not (T p23 p23))) (and (not (T p13 p13)) (T p23 p23))))
(echo "Does gene 0 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 4))
(declare-const p11 (_ BitVec 4))
(declare-const p12 (_ BitVec 4))
(declare-const p13 (_ BitVec 4))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11) (T p11 p12) (T p12 p13)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 4))
(declare-const p21 (_ BitVec 4))
(declare-const p22 (_ BitVec 4))
(declare-const p23 (_ BitVec 4))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21) (T p21 p22) (T p22 p23)))
; --------------- END (Path)------------------
(assert (= ((_ extract 1 0) p10) ((_ extract 1 0) p20)))
(assert (= ((_ extract 3 2) p10) (_ bv0 2)))
(assert (= ((_ extract 3 2) p20) (_ bv2 2)))
(assert (or (and (T p13 p13) (not (T p23 p23))) (and (not (T p13 p13)) (T p23 p23))))
(echo "Does gene 1 affect the stability of the system?")
(check-sat)
(pop)
(get-info :all-statistics)