(set-option :produce-models true) (set-option :pull-nested-quantifiers true) (set-option :mbqi true) (declare-const x (_ BitVec 46)) (declare-const y (_ BitVec 46)) (declare-const xs (_ BitVec 46)) ; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\thelper.cnet-------- (declare-fun T ((_ BitVec 46) (_ BitVec 46) ) bool) ; -------------- Transition Relation: ----------------- (assert (forall ((x (_ BitVec 46)) (y (_ BitVec 46)) )(= (T x y) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (and (or false) (not (= ((_ extract 23 23) x) (_ bv1 1))))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (and (or (and (= ((_ extract 0 0) x) (_ bv1 1)))) (not (= ((_ extract 24 24) x) (_ bv1 1))))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (and (or false) (not (= ((_ extract 25 25) x) (_ bv1 1))))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (and (or (and (= ((_ extract 2 2) x) (_ bv1 1)))) (not (= ((_ extract 26 26) x) (_ bv1 1))))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (and (or false) (not (= ((_ extract 27 27) x) (_ bv1 1))))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (and (or (and (= ((_ extract 4 4) x) (_ bv1 1)) (not (= ((_ extract 18 18) x) (_ bv1 1))))) (not (= ((_ extract 28 28) x) (_ bv1 1))))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (and (or (and (= ((_ extract 5 5) x) (_ bv1 1)))) (not (= ((_ extract 29 29) x) (_ bv1 1))))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (and (or (and (= ((_ extract 15 15) x) (_ bv1 1))) (and (= ((_ extract 11 11) x) (_ bv1 1)))) (not (= ((_ extract 30 30) x) (_ bv1 1))))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (and (or false) (not (= ((_ extract 31 31) x) (_ bv1 1))))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (and (or (and (= ((_ extract 8 8) x) (_ bv1 1)) (not (= ((_ extract 18 18) x) (_ bv1 1))))) (not (= ((_ extract 32 32) x) (_ bv1 1))))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (and (or (and (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 19 19) x) (_ bv1 1))))) (not (= ((_ extract 33 33) x) (_ bv1 1))))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (and (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))))) (not (= ((_ extract 34 34) x) (_ bv1 1))))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (and (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))))) (not (= ((_ extract 35 35) x) (_ bv1 1))))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (and (or (and (= ((_ extract 12 12) x) (_ bv1 1)))) (not (= ((_ extract 36 36) x) (_ bv1 1))))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (and (or (and (= ((_ extract 13 13) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))))) (not (= ((_ extract 37 37) x) (_ bv1 1))))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (and (or (and (= ((_ extract 14 14) x) (_ bv1 1))) (and (= ((_ extract 3 3) x) (_ bv1 1)))) (not (= ((_ extract 38 38) x) (_ bv1 1))))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (and (or (and (= ((_ extract 19 19) x) (_ bv1 1)) (not (= ((_ extract 15 15) x) (_ bv1 1))))) (not (= ((_ extract 39 39) x) (_ bv1 1))))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (and (or (and (= ((_ extract 16 16) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))))) (not (= ((_ extract 40 40) x) (_ bv1 1))))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (and (or (and (= ((_ extract 17 17) x) (_ bv1 1)))) (not (= ((_ extract 41 41) x) (_ bv1 1))))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (and (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))))) (not (= ((_ extract 42 42) x) (_ bv1 1))))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (and (or (and (= ((_ extract 19 19) x) (_ bv1 1)))) (not (= ((_ extract 43 43) x) (_ bv1 1))))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (and (or (and (= ((_ extract 20 20) x) (_ bv1 1)))) (not (= ((_ extract 44 44) x) (_ bv1 1))))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (and (or (and (= ((_ extract 21 21) x) (_ bv1 1)))) (not (= ((_ extract 45 45) x) (_ bv1 1))))) (= (= ((_ extract 23 23) y) (_ bv1 1)) (= ((_ extract 23 23) x) (_ bv1 1))) (= (= ((_ extract 24 24) y) (_ bv1 1)) (= ((_ extract 24 24) x) (_ bv1 1))) (= (= ((_ extract 25 25) y) (_ bv1 1)) (= ((_ extract 25 25) x) (_ bv1 1))) (= (= ((_ extract 26 26) y) (_ bv1 1)) (= ((_ extract 26 26) x) (_ bv1 1))) (= (= ((_ extract 27 27) y) (_ bv1 1)) (= ((_ extract 27 27) x) (_ bv1 1))) (= (= ((_ extract 28 28) y) (_ bv1 1)) (= ((_ extract 28 28) x) (_ bv1 1))) (= (= ((_ extract 29 29) y) (_ bv1 1)) (= ((_ extract 29 29) x) (_ bv1 1))) (= (= ((_ extract 30 30) y) (_ bv1 1)) (= ((_ extract 30 30) x) (_ bv1 1))) (= (= ((_ extract 31 31) y) (_ bv1 1)) (= ((_ extract 31 31) x) (_ bv1 1))) (= (= ((_ extract 32 32) y) (_ bv1 1)) (= ((_ extract 32 32) x) (_ bv1 1))) (= (= ((_ extract 33 33) y) (_ bv1 1)) (= ((_ extract 33 33) x) (_ bv1 1))) (= (= ((_ extract 34 34) y) (_ bv1 1)) (= ((_ extract 34 34) x) (_ bv1 1))) (= (= ((_ extract 35 35) y) (_ bv1 1)) (= ((_ extract 35 35) x) (_ bv1 1))) (= (= ((_ extract 36 36) y) (_ bv1 1)) (= ((_ extract 36 36) x) (_ bv1 1))) (= (= ((_ extract 37 37) y) (_ bv1 1)) (= ((_ extract 37 37) x) (_ bv1 1))) (= (= ((_ extract 38 38) y) (_ bv1 1)) (= ((_ extract 38 38) x) (_ bv1 1))) (= (= ((_ extract 39 39) y) (_ bv1 1)) (= ((_ extract 39 39) x) (_ bv1 1))) (= (= ((_ extract 40 40) y) (_ bv1 1)) (= ((_ extract 40 40) x) (_ bv1 1))) (= (= ((_ extract 41 41) y) (_ bv1 1)) (= ((_ extract 41 41) x) (_ bv1 1))) (= (= ((_ extract 42 42) y) (_ bv1 1)) (= ((_ extract 42 42) x) (_ bv1 1))) (= (= ((_ extract 43 43) y) (_ bv1 1)) (= ((_ extract 43 43) x) (_ bv1 1))) (= (= ((_ extract 44 44) y) (_ bv1 1)) (= ((_ extract 44 44) x) (_ bv1 1))) (= (= ((_ extract 45 45) y) (_ bv1 1)) (= ((_ extract 45 45) x) (_ bv1 1))))))) ; ------------------ END ------------------------------ (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv1 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 0 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv2 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 1 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv4 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 2 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv8 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 3 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv16 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 4 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv32 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 5 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv64 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 6 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv128 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 7 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv256 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 8 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv512 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 9 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv1024 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 10 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv2048 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 11 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv4096 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 12 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv8192 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 13 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv16384 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 14 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv32768 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 15 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv65536 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 16 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv131072 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 17 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv262144 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 18 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv524288 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 19 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv1048576 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 20 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv2097152 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 21 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 46)) (declare-const p11 (_ BitVec 46)) (declare-const p12 (_ BitVec 46)) (declare-const p13 (_ BitVec 46)) (declare-const p14 (_ BitVec 46)) (declare-const p15 (_ BitVec 46)) (declare-const p16 (_ BitVec 46)) (declare-const p17 (_ BitVec 46)) (declare-const p18 (_ BitVec 46)) (declare-const p19 (_ BitVec 46)) (declare-const p110 (_ BitVec 46)) (declare-const p111 (_ BitVec 46)) (declare-const p112 (_ BitVec 46)) (declare-const p113 (_ BitVec 46)) (declare-const p114 (_ BitVec 46)) (declare-const p115 (_ BitVec 46)) (declare-const p116 (_ BitVec 46)) (declare-const p117 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16) (T p16 p17) (T p17 p18) (T p18 p19) (T p19 p110) (T p110 p111) (T p111 p112) (T p112 p113) (T p113 p114) (T p114 p115) (T p115 p116) (T p116 p117))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 46)) (declare-const p21 (_ BitVec 46)) (declare-const p22 (_ BitVec 46)) (declare-const p23 (_ BitVec 46)) (declare-const p24 (_ BitVec 46)) (declare-const p25 (_ BitVec 46)) (declare-const p26 (_ BitVec 46)) (declare-const p27 (_ BitVec 46)) (declare-const p28 (_ BitVec 46)) (declare-const p29 (_ BitVec 46)) (declare-const p210 (_ BitVec 46)) (declare-const p211 (_ BitVec 46)) (declare-const p212 (_ BitVec 46)) (declare-const p213 (_ BitVec 46)) (declare-const p214 (_ BitVec 46)) (declare-const p215 (_ BitVec 46)) (declare-const p216 (_ BitVec 46)) (declare-const p217 (_ BitVec 46)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26) (T p26 p27) (T p27 p28) (T p28 p29) (T p29 p210) (T p210 p211) (T p211 p212) (T p212 p213) (T p213 p214) (T p214 p215) (T p215 p216) (T p216 p217))) ; --------------- END (Path)------------------ (assert (= ((_ extract 22 0) p10) ((_ extract 22 0) p20))) (assert (= ((_ extract 45 23) p10) (_ bv0 23))) (assert (= ((_ extract 45 23) p20) (_ bv4194304 23))) (assert (or (and (T p117 p117) (not (T p217 p217))) (and (not (T p117 p117)) (T p217 p217)))) (echo "Does gene 22 affect the stability of the system?") (check-sat) (pop) (get-info :all-statistics)