diff options
Diffstat (limited to 'test/regress/regress0/uflia/microwave21.ec.minimized.smt2')
| -rw-r--r-- | test/regress/regress0/uflia/microwave21.ec.minimized.smt2 | 444 |
1 files changed, 0 insertions, 444 deletions
diff --git a/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 b/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 deleted file mode 100644 index b37db9a1e..000000000 --- a/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 +++ /dev/null @@ -1,444 +0,0 @@ -; initialize_defs -; PROPERTY DEFGEN -(set-logic QF_UFNIA) -(set-info :status unsat) -(declare-fun _base () Int) -(declare-fun _n () Int) -(assert (>= _n 0)) - -; maxdepth = 1 -(declare-fun ___z2z___ (Int) Bool) - ; KP_START ; INPUT,STATE(1,)/102 -(declare-fun ___z3z___ (Int) Bool) - ; KP_CLEAR ; INPUT,STATE(1,)/103 -(declare-fun ___z4z___ (Int) Bool) - ; KP_0 ; INPUT,STATE(1,)/104 -(declare-fun ___z5z___ (Int) Bool) - ; KP_1 ; INPUT,STATE(1,)/105 -(declare-fun ___z6z___ (Int) Bool) - ; KP_2 ; INPUT,STATE(1,)/106 -(declare-fun ___z7z___ (Int) Bool) - ; KP_3 ; INPUT,STATE(1,)/107 -(declare-fun ___z8z___ (Int) Bool) - ; KP_4 ; INPUT,STATE(1,)/108 -(declare-fun ___z9z___ (Int) Bool) - ; KP_5 ; INPUT,STATE(1,)/109 -(declare-fun ___z10z___ (Int) Bool) - ; KP_6 ; INPUT,STATE(1,)/110 -(declare-fun ___z11z___ (Int) Bool) - ; KP_7 ; INPUT,STATE(1,)/111 -(declare-fun ___z12z___ (Int) Bool) - ; KP_8 ; INPUT,STATE(1,)/112 -(declare-fun ___z13z___ (Int) Bool) - ; KP_9 ; INPUT,STATE(1,)/113 -(declare-fun ___z14z___ (Int) Bool) - ; DOOR_CLOSED ; INPUT/114 -(declare-fun ___z15z___ (Int) Bool) - ; OK ; OUTPUT/115 -(declare-fun ___z19z___ (Int) Bool) - ; V20_START_PRESSED ; LOCAL/119 -(declare-fun ___z20z___ (Int) Bool) - ; V21_CLEAR_PRESSED ; LOCAL/120 -(declare-fun ___z21z___ (Int) Int) - ; V25_STEPS_TO_COOK ; LOCAL,STATE(1,)/121 -(declare-fun ___z22z___ (Int) Bool) - ; V26_rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock ; LOCAL,STATE(1,)/122 -(declare-fun ___z23z___ (Int) Bool) - ; V37_rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step ; LOCAL,STATE(1,)/123 -(declare-fun ___z24z___ (Int) Int) - ; V38_microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY ; LOCAL,STATE(1,)/124 -(declare-fun ___z25z___ (Int) Int) - ; V39_microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY ; LOCAL,STATE(1,)/125 -(declare-fun ___z26z___ (Int) Int) - ; V40_microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY ; LOCAL,STATE(1,)/126 -(declare-fun ___z33z___ (Int) Int) - ; V47_chart_microwave_mode_logic_start ; LOCAL/133 -(declare-fun ___z34z___ (Int) Int) - ; V48_chart_microwave_mode_logic_clear_off ; LOCAL/134 -(declare-fun ___z35z___ (Int) Int) - ; V49_chart_microwave_mode_logic_door_closed ; LOCAL/135 -(declare-fun ___z36z___ (Int) Bool) - ; V51_rlt_eval_microwave_mode_logic_ON_rlt_fired_1 ; LOCAL/136 -(declare-fun ___z37z___ (Int) Int) - ; V52_rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root ; LOCAL/137 -(declare-fun ___z38z___ (Int) Int) - ; V53_rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root ; LOCAL/138 -(declare-fun ___z39z___ (Int) Bool) - ; V54_rlt_eval_microwave_mode_logic_ON_rlt_fired_2 ; LOCAL/139 -(declare-fun ___z40z___ (Int) Bool) - ; V55_rlt_eval_microwave_mode_logic_ON_rlt_complete_1 ; LOCAL/140 -(declare-fun ___z41z___ (Int) Int) - ; V56_rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root ; LOCAL/141 -(declare-fun ___z42z___ (Int) Int) - ; V57_rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode ; LOCAL/142 -(declare-fun ___z43z___ (Int) Int) - ; V58_rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root ; LOCAL/143 -(declare-fun ___z44z___ (Int) Int) - ; V59_rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode ; LOCAL/144 -(declare-fun ___z45z___ (Int) Bool) - ; V60_rlt_eval_microwave_mode_logic_ON_rlt_fired_4 ; LOCAL/145 -(declare-fun ___z46z___ (Int) Bool) - ; V61_rlt_eval_microwave_mode_logic_ON_rlt_complete_2 ; LOCAL/146 -(declare-fun ___z47z___ (Int) Int) - ; V62_rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root ; LOCAL/147 -(declare-fun ___z48z___ (Int) Int) - ; V63_rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining ; LOCAL/148 -(declare-fun ___z49z___ (Int) Int) - ; V64_rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root ; LOCAL/149 -(declare-fun ___z50z___ (Int) Bool) - ; V65_rlt_eval_microwave_mode_logic_ON_rlt_fired_5 ; LOCAL/150 -(declare-fun ___z51z___ (Int) Int) - ; V66_rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode ; LOCAL/151 -(declare-fun ___z52z___ (Int) Int) - ; V67_rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root ; LOCAL/152 -(declare-fun ___z53z___ (Int) Int) - ; V68_rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root ; LOCAL/153 -(declare-fun ___z54z___ (Int) Bool) - ; V69_rlt_eval_microwave_mode_logic_ON_rlt_fired_6 ; LOCAL/154 -(declare-fun ___z55z___ (Int) Int) - ; V70_rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root ; LOCAL/155 -(declare-fun ___z56z___ (Int) Int) - ; V71_rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode ; LOCAL/156 -(declare-fun ___z57z___ (Int) Int) - ; V72_rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root ; LOCAL/157 -(declare-fun ___z58z___ (Int) Bool) - ; V73_rlt_enter_microwave_mode_logic_ON_rlt_fired_0 ; LOCAL/158 -(declare-fun ___z59z___ (Int) Bool) - ; V74_rlt_enter_microwave_mode_logic_ON_rlt_fired_1 ; LOCAL/159 -(declare-fun ___z60z___ (Int) Int) - ; V75_rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root ; LOCAL/160 -(declare-fun ___z61z___ (Int) Int) - ; V76_rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode ; LOCAL/161 -(declare-fun ___z62z___ (Int) Bool) - ; V77_rlt_enter_microwave_mode_logic_ON_rlt_fired_2 ; LOCAL/162 -(declare-fun ___z63z___ (Int) Int) - ; V78_rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root ; LOCAL/163 -(declare-fun ___z64z___ (Int) Bool) - ; V79_rlt_eval_microwave_mode_logic_rlt_fired_0 ; LOCAL/164 -(declare-fun ___z65z___ (Int) Int) - ; V80_rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining ; LOCAL/165 -(declare-fun ___z66z___ (Int) Bool) - ; V81_rlt_eval_microwave_mode_logic_rlt_fired_1 ; LOCAL/166 -(declare-fun ___z67z___ (Int) Int) - ; V82_rlt_eval_microwave_mode_logic_rlt_state_2_states___root ; LOCAL/167 -(declare-fun ___z68z___ (Int) Int) - ; V83_rlt_eval_microwave_mode_logic_rlt_state_3_states___root ; LOCAL/168 -(declare-fun ___z69z___ (Int) Int) - ; V84_rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode ; LOCAL/169 -(declare-fun ___z70z___ (Int) Int) - ; V85_rlt_enter_microwave_mode_logic_rlt_state_2_states___root ; LOCAL/170 -(declare-fun ___z71z___ (Int) Bool) - ; V86_chart_microwave_mode_logic_rlt_evtInitStep ; LOCAL,STATE(1,)/171 -(declare-fun ___z72z___ (Int) Int) - ; V87_chart_microwave_mode_logic_begin_state_states___root ; LOCAL/172 -(declare-fun ___z73z___ (Int) Int) - ; V88_chart_microwave_mode_logic_begin_state_outports_mode ; LOCAL/173 -(declare-fun ___z74z___ (Int) Int) - ; V89_chart_microwave_mode_logic_begin_state_outports_steps_remaining ; LOCAL/174 -(declare-fun ___z75z___ (Int) Int) - ; V90_chart_microwave_mode_logic_final_state_states___root ; LOCAL,STATE(1,)/175 -(declare-fun ___z76z___ (Int) Int) - ; V92_chart_microwave_mode_logic_steps_remaining ; LOCAL,STATE(1,)/176 -(declare-fun ___z77z___ (Int) Int) - ; V93_microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT ; LOCAL/177 -(declare-fun ___z80z___ (Int) Int) - ; V96_microwave_microwave_mode_logic_mode ; LOCAL,STATE(1,)/180 - - -; Generic definitions: -(define-fun DEF__172 ((_M Int)) Bool(= (___z72z___ _M) (ite (= _M _base) 0 (___z75z___ (- _M 1))))) -(define-fun DEF__173 ((_M Int)) Bool(= (___z73z___ _M) (ite (= _M _base) 0 (___z80z___ (- _M 1))))) -(define-fun DEF__174 ((_M Int)) Bool(= (___z74z___ _M) (ite (= _M _base) 0 (___z76z___ (- _M 1))))) -(define-fun DEF__175 ((_M Int)) Bool(= (___z75z___ _M) (ite (= (___z71z___ _M) true) (___z70z___ _M) (ite (= (and (not (___z66z___ _M)) (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3))) true) (ite (= (___z54z___ _M) true) (ite (= (not (= (___z55z___ _M) 3)) true) 3 (___z55z___ _M)) (___z55z___ _M)) (___z68z___ _M))))) -(define-fun DEF__133 ((_M Int)) Bool(= (___z33z___ _M) (ite (= (= (___z19z___ _M) false) true) 0 1))) -(define-fun DEF__176 ((_M Int)) Bool(= (___z76z___ _M) (ite (= (___z71z___ _M) true) (___z74z___ _M) (ite (= (and (not (___z66z___ _M)) (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3))) true) (ite (= (___z50z___ _M) true) (- (___z48z___ _M) 1) (___z48z___ _M)) (___z65z___ _M))))) -(define-fun DEF__134 ((_M Int)) Bool(= (___z34z___ _M) (ite (= (= (___z20z___ _M) false) true) 0 1))) -(define-fun DEF__177 ((_M Int)) Bool(= (___z77z___ _M) (div (div (___z76z___ _M) 1) 60))) -(define-fun DEF__135 ((_M Int)) Bool(= (___z35z___ _M) (ite (= (= (___z14z___ _M) false) true) 0 1))) -(define-fun DEF__136 ((_M Int)) Bool(= (___z36z___ _M) (and (and (= (___z68z___ _M) 2) (<= (___z65z___ _M) 0)) (= (___z68z___ _M) 2)))) -(define-fun DEF__180 ((_M Int)) Bool(= (___z80z___ _M) (ite (= (___z71z___ _M) true) (ite (= (not (= (___z72z___ _M) 4)) true) 1 (___z73z___ _M)) (ite (= (and (not (___z66z___ _M)) (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3))) true) (ite (= (___z54z___ _M) true) (ite (= (not (= (___z55z___ _M) 3)) true) 3 (___z56z___ _M)) (___z56z___ _M)) (___z69z___ _M))))) -(define-fun DEF__137 ((_M Int)) Bool(= (___z37z___ _M) (ite (= (___z36z___ _M) true) (ite (= (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3)) true) 0 (___z68z___ _M)) (___z68z___ _M)))) -(define-fun DEF__138 ((_M Int)) Bool(= (___z38z___ _M) (ite (= (___z36z___ _M) true) (ite (= (not (= (___z37z___ _M) 4)) true) 4 (___z37z___ _M)) (___z37z___ _M)))) -(define-fun DEF__139 ((_M Int)) Bool(= (___z39z___ _M) (and (= (___z38z___ _M) 3) (and (and (ite (= (not (= (___z33z___ _M) 0)) true) true false) (ite (= (not (= (___z35z___ _M) 0)) true) true false)) (not (___z36z___ _M)))))) -(define-fun DEF__140 ((_M Int)) Bool(= (___z40z___ _M) (or (___z39z___ _M) (___z36z___ _M)))) -(define-fun DEF__141 ((_M Int)) Bool(= (___z41z___ _M) (ite (= (___z39z___ _M) true) (ite (= (___z38z___ _M) 3) 1 (___z38z___ _M)) (___z38z___ _M)))) -(define-fun DEF__142 ((_M Int)) Bool(= (___z42z___ _M) (ite (= (___z36z___ _M) true) (ite (= (not (= (___z37z___ _M) 4)) true) 1 (___z69z___ _M)) (___z69z___ _M)))) -(define-fun DEF__143 ((_M Int)) Bool(= (___z43z___ _M) (ite (= (___z39z___ _M) true) (ite (= (not (= (___z41z___ _M) 2)) true) 2 (___z41z___ _M)) (___z41z___ _M)))) -(define-fun DEF__144 ((_M Int)) Bool(= (___z44z___ _M) (ite (= (___z39z___ _M) true) (ite (= (not (= (___z41z___ _M) 2)) true) 2 (___z42z___ _M)) (___z42z___ _M)))) -(define-fun DEF__145 ((_M Int)) Bool(= (___z45z___ _M) (and (and (= (___z43z___ _M) 3) (and (ite (= (not (= (___z34z___ _M) 0)) true) true false) (not (___z40z___ _M)))) (and (= (___z43z___ _M) 3) (not (___z40z___ _M)))))) -(define-fun DEF__146 ((_M Int)) Bool(= (___z46z___ _M) (or (___z45z___ _M) (___z40z___ _M)))) -(define-fun DEF__147 ((_M Int)) Bool(= (___z47z___ _M) (ite (= (___z45z___ _M) true) (ite (= (and (>= (___z43z___ _M) 1) (<= (___z43z___ _M) 3)) true) 0 (___z43z___ _M)) (___z43z___ _M)))) -(define-fun DEF__148 ((_M Int)) Bool(= (___z48z___ _M) (ite (= (___z45z___ _M) true) 0 (___z65z___ _M)))) -(define-fun DEF__149 ((_M Int)) Bool(= (___z49z___ _M) (ite (= (___z45z___ _M) true) (ite (= (not (= (___z47z___ _M) 4)) true) 4 (___z47z___ _M)) (___z47z___ _M)))) -(define-fun DEF__150 ((_M Int)) Bool(= (___z50z___ _M) (and (= (___z49z___ _M) 2) (and (> (___z48z___ _M) 0) (not (___z46z___ _M)))))) -(define-fun DEF__151 ((_M Int)) Bool(= (___z51z___ _M) (ite (= (___z45z___ _M) true) (ite (= (not (= (___z47z___ _M) 4)) true) 1 (___z44z___ _M)) (___z44z___ _M)))) -(define-fun DEF__152 ((_M Int)) Bool(= (___z52z___ _M) (ite (= (___z50z___ _M) true) (ite (= (___z49z___ _M) 2) 1 (___z49z___ _M)) (___z49z___ _M)))) -(define-fun DEF__153 ((_M Int)) Bool(= (___z53z___ _M) (ite (= (___z50z___ _M) true) (ite (= (not (= (___z52z___ _M) 2)) true) 2 (___z52z___ _M)) (___z52z___ _M)))) -(define-fun DEF__154 ((_M Int)) Bool(= (___z54z___ _M) (and (= (___z53z___ _M) 2) (and (or (ite (= (not (= (___z34z___ _M) 0)) true) true false) (not (ite (= (not (= (___z35z___ _M) 0)) true) true false))) (not (or (___z50z___ _M) (___z46z___ _M))))))) -(define-fun DEF__155 ((_M Int)) Bool(= (___z55z___ _M) (ite (= (___z54z___ _M) true) (ite (= (___z53z___ _M) 2) 1 (___z53z___ _M)) (___z53z___ _M)))) -(define-fun DEF__156 ((_M Int)) Bool(= (___z56z___ _M) (ite (= (___z50z___ _M) true) (ite (= (not (= (___z52z___ _M) 2)) true) 2 (___z51z___ _M)) (___z51z___ _M)))) -(define-fun DEF__157 ((_M Int)) Bool(= (___z57z___ _M) (ite (= (not (and (>= (___z67z___ _M) 1) (<= (___z67z___ _M) 3))) true) 1 (___z67z___ _M)))) -(define-fun DEF__115 ((_M Int)) Bool(= (___z15z___ _M) (ite (= _M _base) (or (not (and (___z22z___ _M) (not (___z3z___ _M)))) (or (not (or (or (or (or (or (or (or (or (or (___z5z___ _M) (___z6z___ _M)) (___z7z___ _M)) (___z8z___ _M)) (___z9z___ _M)) (___z10z___ _M)) (___z11z___ _M)) (___z12z___ _M)) (___z13z___ _M)) (___z4z___ _M))) (= (___z77z___ _M) (div (div (___z21z___ _M) 1) 60)))) (or (not (and (___z22z___ _M) (not (___z3z___ _M)))) (or (not (or (or (or (or (or (or (or (or (or (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) (and (___z6z___ _M) (not (___z6z___ (- _M 1))))) (and (___z7z___ _M) (not (___z7z___ (- _M 1))))) (and (___z8z___ _M) (not (___z8z___ (- _M 1))))) (and (___z9z___ _M) (not (___z9z___ (- _M 1))))) (and (___z10z___ _M) (not (___z10z___ (- _M 1))))) (and (___z11z___ _M) (not (___z11z___ (- _M 1))))) (and (___z12z___ _M) (not (___z12z___ (- _M 1))))) (and (___z13z___ _M) (not (___z13z___ (- _M 1))))) (and (___z4z___ _M) (not (___z4z___ (- _M 1)))))) (= (___z77z___ _M) (div (div (___z21z___ _M) 1) 60))))))) -(define-fun DEF__158 ((_M Int)) Bool(= (___z58z___ _M) (and (not (and (>= (___z67z___ _M) 1) (<= (___z67z___ _M) 3))) (and (>= (___z57z___ _M) 1) (<= (___z57z___ _M) 3))))) -(define-fun DEF__159 ((_M Int)) Bool(= (___z59z___ _M) (and (___z58z___ _M) (and (and (>= (___z57z___ _M) 1) (<= (___z57z___ _M) 3)) (ite (= (not (= (___z35z___ _M) 0)) true) true false))))) -(define-fun DEF__160 ((_M Int)) Bool(= (___z60z___ _M) (ite (= (___z59z___ _M) true) (ite (= (not (= (___z57z___ _M) 2)) true) 2 (___z57z___ _M)) (___z57z___ _M)))) -(define-fun DEF__161 ((_M Int)) Bool(= (___z61z___ _M) (ite (= (___z59z___ _M) true) (ite (= (not (= (___z57z___ _M) 2)) true) 2 (___z73z___ _M)) (___z73z___ _M)))) -(define-fun DEF__119 ((_M Int)) Bool(= (___z19z___ _M) (ite (= _M _base) (___z2z___ _M) (and (___z2z___ _M) (not (___z2z___ (- _M 1))))))) -(define-fun DEF__162 ((_M Int)) Bool(= (___z62z___ _M) (and (___z58z___ _M) (and (and (>= (___z60z___ _M) 1) (<= (___z60z___ _M) 3)) (not (___z59z___ _M)))))) -(define-fun DEF__120 ((_M Int)) Bool(= (___z20z___ _M) (ite (= _M _base) (___z3z___ _M) (and (___z3z___ _M) (not (___z3z___ (- _M 1))))))) -(define-fun DEF__163 ((_M Int)) Bool(= (___z63z___ _M) (ite (= (___z62z___ _M) true) (ite (= (not (= (___z60z___ _M) 3)) true) 3 (___z60z___ _M)) (___z60z___ _M)))) -(define-fun DEF__121 ((_M Int)) Bool(= (___z21z___ _M) (ite (= _M _base) (ite (= (and (___z23z___ _M) (not (___z22z___ _M))) true) 0 (* (+ (+ (* (___z26z___ _M) 1) (* (___z25z___ _M) 10)) (* (___z24z___ _M) 60)) 1)) (ite (= (and (___z23z___ _M) (not (___z22z___ _M))) true) 0 (ite (= (___z22z___ _M) true) (* (+ (+ (* (___z26z___ _M) 1) (* (___z25z___ _M) 10)) (* (___z24z___ _M) 60)) 1) (___z21z___ (- _M 1))))))) -(define-fun DEF__164 ((_M Int)) Bool(= (___z64z___ _M) (= (___z72z___ _M) 4))) -(define-fun DEF__122 ((_M Int)) Bool(= (___z22z___ _M) (ite (= _M _base) true (ite (= 1 (___z80z___ (- _M 1))) true false)))) -(define-fun DEF__165 ((_M Int)) Bool(= (___z65z___ _M) (ite (= (___z64z___ _M) true) (___z21z___ _M) (___z74z___ _M)))) -(define-fun DEF__123 ((_M Int)) Bool(= (___z23z___ _M) (ite (= _M _base) true (ite (= (not (___z22z___ _M)) true) true (ite (= (___z22z___ (- _M 1)) true) false (___z23z___ (- _M 1))))))) -(define-fun DEF__166 ((_M Int)) Bool(= (___z66z___ _M) (and (___z64z___ _M) (and (= (___z72z___ _M) 4) (and (ite (= (not (= (___z33z___ _M) 0)) true) true false) (ite (= (not (= (ite (= (= (> (___z21z___ _M) 0) false) true) 0 1) 0)) true) true false)))))) -(define-fun DEF__124 ((_M Int)) Bool(= (___z24z___ _M) (ite (= _M _base) 0 (ite (= (___z22z___ _M) true) (ite (= (___z23z___ _M) true) 0 (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) 9) true false) true) (___z25z___ (- _M 1)) (___z24z___ (- _M 1))))) (___z24z___ (- _M 1)))))) -(define-fun DEF__167 ((_M Int)) Bool(= (___z67z___ _M) (ite (= (___z66z___ _M) true) (ite (= (___z72z___ _M) 4) 0 (___z72z___ _M)) (___z72z___ _M)))) -(define-fun DEF__125 ((_M Int)) Bool(= (___z25z___ _M) (ite (= _M _base) 0 (ite (= (___z22z___ _M) true) (ite (= (___z23z___ _M) true) 0 (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) 9) true false) true) (___z26z___ (- _M 1)) (___z25z___ (- _M 1))))) (___z25z___ (- _M 1)))))) -(define-fun DEF__168 ((_M Int)) Bool(= (___z68z___ _M) (ite (= (___z66z___ _M) true) (___z63z___ _M) (___z67z___ _M)))) -(define-fun DEF__126 ((_M Int)) Bool(= (___z26z___ _M) (ite (= _M _base) (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 9) true false) true) (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 0)) (ite (= (___z22z___ _M) true) (ite (= (___z23z___ _M) true) (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 9) true false) true) (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 0)) (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) 9) true false) true) (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) (___z26z___ (- _M 1))))) (___z26z___ (- _M 1)))))) -(define-fun DEF__169 ((_M Int)) Bool(= (___z69z___ _M) (ite (= (___z66z___ _M) true) (ite (= (___z62z___ _M) true) (ite (= (not (= (___z60z___ _M) 3)) true) 3 (___z61z___ _M)) (___z61z___ _M)) (___z73z___ _M)))) -(define-fun DEF__170 ((_M Int)) Bool(= (___z70z___ _M) (ite (= (not (= (___z72z___ _M) 4)) true) 4 (___z72z___ _M)))) -(define-fun DEF__171 ((_M Int)) Bool(= (___z71z___ _M) (ite (= _M _base) true (ite (= true true) false (___z71z___ (- _M 1)))))) -; Transition: -(define-fun trans ((_M Int)) Bool (and (DEF__171 _M) (DEF__170 _M) (DEF__169 _M) (DEF__126 _M) (DEF__168 _M) (DEF__125 _M) (DEF__167 _M) (DEF__124 _M) (DEF__166 _M) (DEF__123 _M) (DEF__165 _M) (DEF__122 _M) (DEF__164 _M) (DEF__121 _M) (DEF__163 _M) (DEF__120 _M) (DEF__162 _M) (DEF__119 _M) (DEF__161 _M) (DEF__160 _M) (DEF__159 _M) (DEF__158 _M) (DEF__115 _M) (DEF__157 _M) (DEF__156 _M) (DEF__155 _M) (DEF__154 _M) (DEF__153 _M) (DEF__152 _M) (DEF__151 _M) (DEF__150 _M) (DEF__149 _M) (DEF__148 _M) (DEF__147 _M) (DEF__146 _M) (DEF__145 _M) (DEF__144 _M) (DEF__143 _M) (DEF__142 _M) (DEF__141 _M) (DEF__140 _M) (DEF__139 _M) (DEF__138 _M) (DEF__137 _M) (DEF__180 _M) (DEF__136 _M) (DEF__135 _M) (DEF__177 _M) (DEF__134 _M) (DEF__176 _M) (DEF__133 _M) (DEF__175 _M) (DEF__174 _M) (DEF__173 _M) (DEF__172 _M) )) - -(define-fun P ((_M Int)) Bool(= (___z15z___ _M) true)) - - - -; BASE DONE - -; Begin induction: -; print_initialization -; def_assert_both1 -; def_assert_both -(assert (DEF__172 0)) -; print_checker_assertion -(assert (DEF__173 0)) -; print_checker_assertion -(assert (DEF__174 0)) -; print_checker_assertion -(assert (DEF__175 0)) -; print_checker_assertion -(assert (DEF__133 0)) -; print_checker_assertion -(assert (DEF__176 0)) -; print_checker_assertion -(assert (DEF__134 0)) -; print_checker_assertion -(assert (DEF__177 0)) -; print_checker_assertion -(assert (DEF__135 0)) -; print_checker_assertion -(assert (DEF__136 0)) -; print_checker_assertion -(assert (DEF__180 0)) -; print_checker_assertion -(assert (DEF__137 0)) -; print_checker_assertion -(assert (DEF__138 0)) -; print_checker_assertion -(assert (DEF__139 0)) -; print_checker_assertion -(assert (DEF__140 0)) -; print_checker_assertion -(assert (DEF__141 0)) -; print_checker_assertion -(assert (DEF__142 0)) -; print_checker_assertion -(assert (DEF__143 0)) -; print_checker_assertion -(assert (DEF__144 0)) -; print_checker_assertion -(assert (DEF__145 0)) -; print_checker_assertion -(assert (DEF__146 0)) -; print_checker_assertion -(assert (DEF__147 0)) -; print_checker_assertion -(assert (DEF__148 0)) -; print_checker_assertion -(assert (DEF__149 0)) -; print_checker_assertion -(assert (DEF__150 0)) -; print_checker_assertion -(assert (DEF__151 0)) -; print_checker_assertion -(assert (DEF__152 0)) -; print_checker_assertion -(assert (DEF__153 0)) -; print_checker_assertion -(assert (DEF__154 0)) -; print_checker_assertion -(assert (DEF__155 0)) -; print_checker_assertion -(assert (DEF__156 0)) -; print_checker_assertion -(assert (DEF__157 0)) -; print_checker_assertion -(assert (DEF__115 0)) -; print_checker_assertion -(assert (DEF__158 0)) -; print_checker_assertion -(assert (DEF__159 0)) -; print_checker_assertion -(assert (DEF__160 0)) -; print_checker_assertion -(assert (DEF__161 0)) -; print_checker_assertion -(assert (DEF__119 0)) -; print_checker_assertion -(assert (DEF__162 0)) -; print_checker_assertion -(assert (DEF__120 0)) -; print_checker_assertion -(assert (DEF__163 0)) -; print_checker_assertion -(assert (DEF__121 0)) -; print_checker_assertion -(assert (DEF__164 0)) -; print_checker_assertion -(assert (DEF__122 0)) -; print_checker_assertion -(assert (DEF__165 0)) -; print_checker_assertion -(assert (DEF__123 0)) -; print_checker_assertion -(assert (DEF__166 0)) -; print_checker_assertion -(assert (DEF__124 0)) -; print_checker_assertion -(assert (DEF__167 0)) -; print_checker_assertion -(assert (DEF__125 0)) -; print_checker_assertion -(assert (DEF__168 0)) -; print_checker_assertion -(assert (DEF__126 0)) -; print_checker_assertion -(assert (DEF__169 0)) -; print_checker_assertion -(assert (DEF__170 0)) -; print_checker_assertion -(assert (DEF__171 0)) -; print_checker_assertion -; def_assert_both1 -; def_assert_both -(assert (DEF__172 (- 0 1))) -; print_checker_assertion -(assert (DEF__173 (- 0 1))) -; print_checker_assertion -(assert (DEF__174 (- 0 1))) -; print_checker_assertion -(assert (DEF__175 (- 0 1))) -; print_checker_assertion -(assert (DEF__133 (- 0 1))) -; print_checker_assertion -(assert (DEF__176 (- 0 1))) -; print_checker_assertion -(assert (DEF__134 (- 0 1))) -; print_checker_assertion -(assert (DEF__177 (- 0 1))) -; print_checker_assertion -(assert (DEF__135 (- 0 1))) -; print_checker_assertion -(assert (DEF__136 (- 0 1))) -; print_checker_assertion -(assert (DEF__180 (- 0 1))) -; print_checker_assertion -(assert (DEF__137 (- 0 1))) -; print_checker_assertion -(assert (DEF__138 (- 0 1))) -; print_checker_assertion -(assert (DEF__139 (- 0 1))) -; print_checker_assertion -(assert (DEF__140 (- 0 1))) -; print_checker_assertion -(assert (DEF__141 (- 0 1))) -; print_checker_assertion -(assert (DEF__142 (- 0 1))) -; print_checker_assertion -(assert (DEF__143 (- 0 1))) -; print_checker_assertion -(assert (DEF__144 (- 0 1))) -; print_checker_assertion -(assert (DEF__145 (- 0 1))) -; print_checker_assertion -(assert (DEF__146 (- 0 1))) -; print_checker_assertion -(assert (DEF__147 (- 0 1))) -; print_checker_assertion -(assert (DEF__148 (- 0 1))) -; print_checker_assertion -(assert (DEF__149 (- 0 1))) -; print_checker_assertion -(assert (DEF__150 (- 0 1))) -; print_checker_assertion -(assert (DEF__151 (- 0 1))) -; print_checker_assertion -(assert (DEF__152 (- 0 1))) -; print_checker_assertion -(assert (DEF__153 (- 0 1))) -; print_checker_assertion -(assert (DEF__154 (- 0 1))) -; print_checker_assertion -(assert (DEF__155 (- 0 1))) -; print_checker_assertion -(assert (DEF__156 (- 0 1))) -; print_checker_assertion -(assert (DEF__157 (- 0 1))) -; print_checker_assertion -(assert (DEF__115 (- 0 1))) -; print_checker_assertion -(assert (DEF__158 (- 0 1))) -; print_checker_assertion -(assert (DEF__159 (- 0 1))) -; print_checker_assertion -(assert (DEF__160 (- 0 1))) -; print_checker_assertion -(assert (DEF__161 (- 0 1))) -; print_checker_assertion -(assert (DEF__119 (- 0 1))) -; print_checker_assertion -(assert (DEF__162 (- 0 1))) -; print_checker_assertion -(assert (DEF__120 (- 0 1))) -; print_checker_assertion -(assert (DEF__163 (- 0 1))) -; print_checker_assertion -(assert (DEF__121 (- 0 1))) -; print_checker_assertion -(assert (DEF__164 (- 0 1))) -; print_checker_assertion -(assert (DEF__122 (- 0 1))) -; print_checker_assertion -(assert (DEF__165 (- 0 1))) -; print_checker_assertion -(assert (DEF__123 (- 0 1))) -; print_checker_assertion -(assert (DEF__166 (- 0 1))) -; print_checker_assertion -(assert (DEF__124 (- 0 1))) -; print_checker_assertion -(assert (DEF__167 (- 0 1))) -; print_checker_assertion -(assert (DEF__125 (- 0 1))) -; print_checker_assertion -(assert (DEF__168 (- 0 1))) -; print_checker_assertion -(assert (DEF__126 (- 0 1))) -; print_checker_assertion -(assert (DEF__169 (- 0 1))) -; print_checker_assertion -(assert (DEF__170 (- 0 1))) -; print_checker_assertion -(assert (DEF__171 (- 0 1))) -; print_checker_assertion - -; Checking k=2 base -; not refinement_pass -(assert (not (=> (= _base (- 0 1)) (and (P (- 0 1)) (P 0))))) -(assert true) -(check-sat) |