Created
August 12, 2021 11:54
-
-
Save leonardoalt/4ea67e0b985ee34551383090d21f6231 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (declare-fun |interface_0_I_4_0| (Int ) Bool) | |
| (declare-fun |nondet_interface_1_I_4_0| (Int Int ) Bool) | |
| (declare-fun |summary_constructor_2_I_4_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (error_0 Int) (this_0 Int)) | |
| (=> (= error_0 0) (nondet_interface_1_I_4_0 error_0 this_0)))) | |
| (declare-fun |summary_3_function_ext__3_4_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (error_0 Int) (error_1 Int) (this_0 Int)) | |
| (=> (and (and (nondet_interface_1_I_4_0 error_0 this_0) true) (and (= error_0 0) (summary_3_function_ext__3_4_0 error_1 this_0))) (nondet_interface_1_I_4_0 error_1 this_0)))) | |
| (declare-fun |interface_4_C_62_0| (Int Int Bool ) Bool) | |
| (declare-fun |nondet_interface_5_C_62_0| (Int Int Int Bool Int Bool ) Bool) | |
| (declare-fun |summary_constructor_6_C_62_0| (Int Int Int Bool Int Bool ) Bool) | |
| (assert | |
| (forall ( (error_0 Int) (error_1 Int) (lock_8_0 Bool) (this_0 Int) (x_6_0 Int)) | |
| (=> (= error_1 0) (nondet_interface_5_C_62_0 error_1 this_0 x_6_0 lock_8_0 x_6_0 lock_8_0)))) | |
| (declare-fun |summary_7_function_set__37_62_0| (Int Int Int Bool Int Int Bool Int ) Bool) | |
| (assert | |
| (forall ( (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int)) | |
| (=> (and (and (nondet_interface_5_C_62_0 error_1 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) true) (and (= error_1 0) (summary_7_function_set__37_62_0 error_2 this_0 x_6_1 lock_8_1 _x_27_0 x_6_2 lock_8_2 _x_27_1))) (nondet_interface_5_C_62_0 error_2 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2)))) | |
| (declare-fun |summary_8_function_f__61_62_0| (Int Int Int Bool Int Int Bool Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int)) | |
| (=> (and (and (nondet_interface_5_C_62_0 error_2 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) true) (and (= error_2 0) (summary_8_function_f__61_62_0 error_3 this_0 x_6_1 lock_8_1 _i_40_0 x_6_2 lock_8_2 _i_40_1))) (nondet_interface_5_C_62_0 error_3 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_prev_46_1 Int)) | |
| (=> (and true (= error_0 0)) (summary_3_function_ext__3_4_0 error_0 this_0)))) | |
| (declare-fun |contract_initializer_9_I_4_0| (Int Int ) Bool) | |
| (declare-fun |contract_initializer_entry_10_I_4_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_prev_46_1 Int)) | |
| (=> (and (and true (= error_0 0)) true) (contract_initializer_entry_10_I_4_0 error_0 this_0)))) | |
| (declare-fun |contract_initializer_after_init_11_I_4_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_prev_46_1 Int)) | |
| (=> (and (and (contract_initializer_entry_10_I_4_0 error_0 this_0) true) true) (contract_initializer_after_init_11_I_4_0 error_0 this_0)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_prev_46_1 Int)) | |
| (=> (and (and (contract_initializer_after_init_11_I_4_0 error_0 this_0) true) true) (contract_initializer_9_I_4_0 error_0 this_0)))) | |
| (declare-fun |implicit_constructor_entry_12_I_4_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_prev_46_1 Int)) | |
| (=> (and (and (and true (= error_0 0)) true) true) (implicit_constructor_entry_12_I_4_0 error_0 this_0)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_prev_46_1 Int)) | |
| (=> (and (and (implicit_constructor_entry_12_I_4_0 error_0 this_0) (and (contract_initializer_9_I_4_0 error_1 this_0) true)) (> error_1 0)) (summary_constructor_2_I_4_0 error_1 this_0)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_x_27_0 Int) (_x_27_1 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_prev_46_1 Int)) | |
| (=> (and (and (implicit_constructor_entry_12_I_4_0 error_0 this_0) (and (= error_1 0) (and (contract_initializer_9_I_4_0 error_1 this_0) true))) true) (summary_constructor_2_I_4_0 error_1 this_0)))) | |
| (declare-fun |block_13_function_set__37_62_0| (Int Int Int Bool Int Int Bool Int ) Bool) | |
| (declare-fun |block_14_set_36_62_0| (Int Int Int Bool Int Int Bool Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (block_13_function_set__37_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_13_function_set__37_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1) (and (and (and (and true (= error_0 0)) (and (and true (= x_6_1 x_6_0)) (= lock_8_1 lock_8_0))) (and true (= _x_27_1 _x_27_0))) true)) true) (block_14_set_36_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1)))) | |
| (declare-fun |block_15_return_set_25_62_0| (Int Int Int Bool Int Int Bool Int ) Bool) | |
| (declare-fun |block_16_return_function_set__37_62_0| (Int Int Int Bool Int Int Bool Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_12_1 Bool) (expr_15_0 Bool) (expr_16_0 Bool) (expr_17_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_14_set_36_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1) (and (= x_6_2 expr_34_1) (and (=> true (and (>= expr_34_1 0) (<= expr_34_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_34_1 expr_33_0) (and (=> true (and (>= expr_32_0 0) (<= expr_32_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_32_0 x_6_1) (and (=> true (and (>= expr_33_0 0) (<= expr_33_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_33_0 _x_27_1) (and (= lock_8_2 expr_17_1) (and (= expr_17_1 expr_16_0) (and (= expr_15_0 lock_8_1) (and (= expr_16_0 true) (and (=> true expr_12_1) (and (= expr_12_1 (not expr_11_0)) (and (= expr_11_0 lock_8_1) (and (and (>= _x_27_1 0) (<= _x_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))))))))))) true) (block_16_return_function_set__37_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_2 lock_8_2 _x_27_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_12_1 Bool) (expr_15_0 Bool) (expr_16_0 Bool) (expr_17_1 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_16_return_function_set__37_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1) (and (= lock_8_2 expr_22_1) (and (= expr_22_1 expr_21_0) (and (= expr_20_0 lock_8_1) (and (= expr_21_0 false) true))))) true) (block_15_return_set_25_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_2 _x_27_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_12_1 Bool) (expr_15_0 Bool) (expr_16_0 Bool) (expr_17_1 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_15_return_set_25_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1) true) true) (summary_7_function_set__37_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_12_1 Bool) (expr_15_0 Bool) (expr_16_0 Bool) (expr_17_1 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (interface_4_C_62_0 this_0 x_6_0 lock_8_0) true) (and (and (and true true) (summary_7_function_set__37_62_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_1 lock_8_1 _x_27_1)) (= error_0 0))) (interface_4_C_62_0 this_0 x_6_1 lock_8_1)))) | |
| (declare-fun |block_17_function_f__61_62_0| (Int Int Int Bool Int Int Bool Int Int ) Bool) | |
| (declare-fun |block_18_f_60_62_0| (Int Int Int Bool Int Int Bool Int Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_12_1 Bool) (expr_15_0 Bool) (expr_16_0 Bool) (expr_17_1 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (block_17_function_f__61_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_12_1 Bool) (expr_15_0 Bool) (expr_16_0 Bool) (expr_17_1 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_17_function_f__61_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1) (and (and (and (and true (= error_0 0)) (and (and true (= x_6_1 x_6_0)) (= lock_8_1 lock_8_0))) (and true (= _i_40_1 _i_40_0))) true)) true) (block_18_f_60_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1)))) | |
| (declare-fun |block_19_return_f_25_62_0| (Int Int Int Bool Int Int Bool Int Int ) Bool) | |
| (declare-fun |block_20_return_function_f__61_62_0| (Int Int Int Bool Int Int Bool Int Int ) Bool) | |
| (declare-fun |nondet_call_21_0| (Int Int Int Bool Int Bool ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (nondet_interface_5_C_62_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (nondet_call_21_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_18_f_60_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1) (and (nondet_call_21_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (and (=> true true) (and (= expr_49_0 _i_40_1) (and (= x_prev_46_2 expr_47_0) (and (=> true (and (>= expr_47_0 0) (<= expr_47_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_47_0 x_6_1) (and (= lock_8_2 expr_17_3) (and (= expr_17_3 expr_16_1) (and (= expr_15_1 lock_8_1) (and (= expr_16_1 true) (and (=> true expr_12_3) (and (= expr_12_3 (not expr_11_1)) (and (= expr_11_1 lock_8_1) (and (and (>= _i_40_1 0) (<= _i_40_1 1461501637330902918203684832716283019655932542975)) (and (= x_prev_46_1 0) true)))))))))))))))) (> error_1 0)) (summary_8_function_f__61_62_0 error_1 this_0 x_6_0 lock_8_0 _i_40_0 x_6_2 lock_8_3 _i_40_1)))) | |
| (declare-fun |block_22_function_f__61_62_0| (Int Int Int Bool Int Int Bool Int Int ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_18_f_60_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1) (and (= expr_57_1 (= expr_55_0 expr_56_0)) (and (=> true (and (>= expr_56_0 0) (<= expr_56_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_56_0 x_prev_46_2) (and (=> true (and (>= expr_55_0 0) (<= expr_55_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_55_0 x_6_2) (and (= error_1 0) (and (nondet_call_21_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (and (=> true true) (and (= expr_49_0 _i_40_1) (and (= x_prev_46_2 expr_47_0) (and (=> true (and (>= expr_47_0 0) (<= expr_47_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_47_0 x_6_1) (and (= lock_8_2 expr_17_3) (and (= expr_17_3 expr_16_1) (and (= expr_15_1 lock_8_1) (and (= expr_16_1 true) (and (=> true expr_12_3) (and (= expr_12_3 (not expr_11_1)) (and (= expr_11_1 lock_8_1) (and (and (>= _i_40_1 0) (<= _i_40_1 1461501637330902918203684832716283019655932542975)) (and (= x_prev_46_1 0) true)))))))))))))))))))))) (and (not expr_57_1) (= error_2 1))) (block_22_function_f__61_62_0 error_2 this_0 x_6_0 lock_8_0 _i_40_0 x_6_2 lock_8_3 _i_40_1 x_prev_46_2)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (block_22_function_f__61_62_0 error_2 this_0 x_6_0 lock_8_0 _i_40_0 x_6_2 lock_8_3 _i_40_1 x_prev_46_2) (summary_8_function_f__61_62_0 error_2 this_0 x_6_0 lock_8_0 _i_40_0 x_6_2 lock_8_3 _i_40_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_21_0 Bool) (expr_22_1 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_18_f_60_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1) (and (= error_2 error_1) (and (= expr_57_1 (= expr_55_0 expr_56_0)) (and (=> true (and (>= expr_56_0 0) (<= expr_56_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_56_0 x_prev_46_2) (and (=> true (and (>= expr_55_0 0) (<= expr_55_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_55_0 x_6_2) (and (= error_1 0) (and (nondet_call_21_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (and (=> true true) (and (= expr_49_0 _i_40_1) (and (= x_prev_46_2 expr_47_0) (and (=> true (and (>= expr_47_0 0) (<= expr_47_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_47_0 x_6_1) (and (= lock_8_2 expr_17_3) (and (= expr_17_3 expr_16_1) (and (= expr_15_1 lock_8_1) (and (= expr_16_1 true) (and (=> true expr_12_3) (and (= expr_12_3 (not expr_11_1)) (and (= expr_11_1 lock_8_1) (and (and (>= _i_40_1 0) (<= _i_40_1 1461501637330902918203684832716283019655932542975)) (and (= x_prev_46_1 0) true))))))))))))))))))))))) true) (block_20_return_function_f__61_62_0 error_2 this_0 x_6_0 lock_8_0 _i_40_0 x_6_2 lock_8_3 _i_40_1 x_prev_46_2)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_20_return_function_f__61_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1) (and (= lock_8_2 expr_22_3) (and (= expr_22_3 expr_21_1) (and (= expr_20_1 lock_8_1) (and (= expr_21_1 false) true))))) true) (block_19_return_f_25_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_2 _i_40_1 x_prev_46_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (block_19_return_f_25_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1 x_prev_46_1) true) true) (summary_8_function_f__61_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (interface_4_C_62_0 this_0 x_6_0 lock_8_0) true) (and (and (and true true) (summary_8_function_f__61_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1)) (= error_0 0))) (interface_4_C_62_0 this_0 x_6_1 lock_8_1)))) | |
| (declare-fun |contract_initializer_23_C_62_0| (Int Int Int Bool Int Bool ) Bool) | |
| (declare-fun |contract_initializer_entry_24_C_62_0| (Int Int Int Bool Int Bool ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and true (= error_0 0)) (and (and true (= x_6_1 x_6_0)) (= lock_8_1 lock_8_0))) (contract_initializer_entry_24_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1)))) | |
| (declare-fun |contract_initializer_after_init_25_C_62_0| (Int Int Int Bool Int Bool ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (contract_initializer_entry_24_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) true) true) (contract_initializer_after_init_25_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (contract_initializer_after_init_25_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) true) true) (contract_initializer_23_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1)))) | |
| (declare-fun |implicit_constructor_entry_26_C_62_0| (Int Int Int Bool Int Bool ) Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (and true (= error_0 0)) (and (and true (= x_6_1 x_6_0)) (= lock_8_1 lock_8_0))) (and (and true (= x_6_1 0)) (= lock_8_1 false))) (implicit_constructor_entry_26_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (implicit_constructor_entry_26_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) (and (contract_initializer_23_C_62_0 error_1 this_0 x_6_1 lock_8_1 x_6_2 lock_8_2) true)) (> error_1 0)) (summary_constructor_6_C_62_0 error_1 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (implicit_constructor_entry_26_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) (and (= error_1 0) (and (contract_initializer_23_C_62_0 error_1 this_0 x_6_1 lock_8_1 x_6_2 lock_8_2) true))) true) (summary_constructor_6_C_62_0 error_1 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2)))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (summary_constructor_6_C_62_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) true) (and (and true true) (= error_0 0))) (interface_4_C_62_0 this_0 x_6_1 lock_8_1)))) | |
| (declare-fun |error_target_2_0| () Bool) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> (and (and (interface_4_C_62_0 this_0 x_6_0 lock_8_0) true) (and (and (and true true) (summary_8_function_f__61_62_0 error_0 this_0 x_6_0 lock_8_0 _i_40_0 x_6_1 lock_8_1 _i_40_1)) (= error_0 1))) error_target_2_0))) | |
| (assert | |
| (forall ( (_i_40_0 Int) (_i_40_1 Int) (_i_40_2 Int) (_i_40_3 Int) (_x_27_0 Int) (_x_27_1 Int) (_x_27_2 Int) (_x_27_3 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_11_0 Bool) (expr_11_1 Bool) (expr_12_1 Bool) (expr_12_2 Bool) (expr_12_3 Bool) (expr_13_1 |tuple()|) (expr_15_0 Bool) (expr_15_1 Bool) (expr_16_0 Bool) (expr_16_1 Bool) (expr_17_1 Bool) (expr_17_2 Bool) (expr_17_3 Bool) (expr_20_0 Bool) (expr_20_1 Bool) (expr_21_0 Bool) (expr_21_1 Bool) (expr_22_1 Bool) (expr_22_2 Bool) (expr_22_3 Bool) (expr_32_0 Int) (expr_33_0 Int) (expr_34_1 Int) (expr_47_0 Int) (expr_49_0 Int) (expr_52_1 |tuple()|) (expr_55_0 Int) (expr_56_0 Int) (expr_57_1 Bool) (lock_8_0 Bool) (lock_8_1 Bool) (lock_8_2 Bool) (lock_8_3 Bool) (this_0 Int) (x_6_0 Int) (x_6_1 Int) (x_6_2 Int) (x_6_3 Int) (x_prev_46_0 Int) (x_prev_46_1 Int) (x_prev_46_2 Int) (x_prev_46_3 Int)) | |
| (=> error_target_2_0 false))) | |
| (check-sat) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment