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