mutex_unsat.smt2

(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_60_0| (Int Int Bool ) Bool)
(declare-fun |nondet_interface_5_C_60_0| (Int Int Int Bool Int Bool ) Bool)
(declare-fun |summary_constructor_6_C_60_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_60_0 error_1 this_0 x_6_0 lock_8_0 x_6_0 lock_8_0))))


(declare-fun |summary_7_function_set__35_60_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_60_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__35_60_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_60_0 error_2 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2))))


(declare-fun |summary_8_function_f__59_60_0| (Int Int Int Bool Int Int Bool Int ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_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_60_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__59_60_0 error_3 this_0 x_6_1 lock_8_1 _i_38_0 x_6_2 lock_8_2 _i_38_1))) (nondet_interface_5_C_60_0 error_3 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2))))


(assert
(forall ( (_i_38_0 Int) (_i_38_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_44_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_38_0 Int) (_i_38_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_44_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_38_0 Int) (_i_38_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_44_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_38_0 Int) (_i_38_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_44_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_38_0 Int) (_i_38_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_44_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_38_0 Int) (_i_38_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_44_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_38_0 Int) (_i_38_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_44_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__35_60_0| (Int Int Int Bool Int Int Bool Int ) Bool)
(declare-fun |block_14_set_34_60_0| (Int Int Int Bool Int Int Bool Int ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(block_13_function_set__35_60_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_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_13_function_set__35_60_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_34_60_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_function_set__35_60_0| (Int Int Int Bool Int Int Bool Int ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_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_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_14_set_34_60_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_32_1) (and (=> true (and (>= expr_32_1 0) (<= expr_32_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_32_1 expr_31_0) (and (=> true (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_6_1) (and (=> true (and (>= expr_31_0 0) (<= expr_31_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_0 _x_27_1) (and (and (>= _x_27_1 0) (<= _x_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))))) true) (block_15_return_function_set__35_60_0 error_0 this_0 x_6_0 lock_8_0 _x_27_0 x_6_2 lock_8_1 _x_27_1))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_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_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_15_return_function_set__35_60_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__35_60_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_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_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_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (interface_4_C_60_0 this_0 x_6_0 lock_8_0) true) (and (and (and true true) (summary_7_function_set__35_60_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_60_0 this_0 x_6_1 lock_8_1))))


(declare-fun |block_16_function_f__59_60_0| (Int Int Int Bool Int Int Bool Int Int ) Bool)
(declare-fun |block_17_f_58_60_0| (Int Int Int Bool Int Int Bool Int Int ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(block_16_function_f__59_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_1)))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_16_function_f__59_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_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_38_1 _i_38_0))) true)) true) (block_17_f_58_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_1))))


(declare-fun |block_18_return_f_25_60_0| (Int Int Int Bool Int Int Bool Int Int ) Bool)
(declare-fun |block_19_return_function_f__59_60_0| (Int Int Int Bool Int Int Bool Int Int ) Bool)
(declare-fun |nondet_call_20_0| (Int Int Int Bool Int Bool ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (nondet_interface_5_C_60_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (nondet_call_20_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_17_f_58_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_1) (and (nondet_call_20_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (and (=> true true) (and (= expr_47_0 _i_38_1) (and (= x_prev_44_2 expr_45_0) (and (=> true (and (>= expr_45_0 0) (<= expr_45_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_45_0 x_6_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 (>= _i_38_1 0) (<= _i_38_1 1461501637330902918203684832716283019655932542975)) (and (= x_prev_44_1 0) true)))))))))))))))) (> error_1 0)) (summary_8_function_f__59_60_0 error_1 this_0 x_6_0 lock_8_0 _i_38_0 x_6_2 lock_8_3 _i_38_1))))


(declare-fun |block_21_function_f__59_60_0| (Int Int Int Bool Int Int Bool Int Int ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_17_f_58_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_1) (and (= expr_55_1 (= expr_53_0 expr_54_0)) (and (=> true (and (>= expr_54_0 0) (<= expr_54_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_54_0 x_prev_44_2) (and (=> true (and (>= expr_53_0 0) (<= expr_53_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_53_0 x_6_2) (and (= error_1 0) (and (nondet_call_20_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (and (=> true true) (and (= expr_47_0 _i_38_1) (and (= x_prev_44_2 expr_45_0) (and (=> true (and (>= expr_45_0 0) (<= expr_45_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_45_0 x_6_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 (>= _i_38_1 0) (<= _i_38_1 1461501637330902918203684832716283019655932542975)) (and (= x_prev_44_1 0) true)))))))))))))))))))))) (and (not expr_55_1) (= error_2 1))) (block_21_function_f__59_60_0 error_2 this_0 x_6_0 lock_8_0 _i_38_0 x_6_2 lock_8_3 _i_38_1 x_prev_44_2))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (block_21_function_f__59_60_0 error_2 this_0 x_6_0 lock_8_0 _i_38_0 x_6_2 lock_8_3 _i_38_1 x_prev_44_2) (summary_8_function_f__59_60_0 error_2 this_0 x_6_0 lock_8_0 _i_38_0 x_6_2 lock_8_3 _i_38_1))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_17_f_58_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_1) (and (= error_2 error_1) (and (= expr_55_1 (= expr_53_0 expr_54_0)) (and (=> true (and (>= expr_54_0 0) (<= expr_54_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_54_0 x_prev_44_2) (and (=> true (and (>= expr_53_0 0) (<= expr_53_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_53_0 x_6_2) (and (= error_1 0) (and (nondet_call_20_0 error_1 this_0 x_6_1 lock_8_2 x_6_2 lock_8_3) (and (=> true true) (and (= expr_47_0 _i_38_1) (and (= x_prev_44_2 expr_45_0) (and (=> true (and (>= expr_45_0 0) (<= expr_45_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_45_0 x_6_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 (>= _i_38_1 0) (<= _i_38_1 1461501637330902918203684832716283019655932542975)) (and (= x_prev_44_1 0) true))))))))))))))))))))))) true) (block_19_return_function_f__59_60_0 error_2 this_0 x_6_0 lock_8_0 _i_38_0 x_6_2 lock_8_3 _i_38_1 x_prev_44_2))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_19_return_function_f__59_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_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_18_return_f_25_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_2 _i_38_1 x_prev_44_1))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (block_18_return_f_25_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1 x_prev_44_1) true) true) (summary_8_function_f__59_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (interface_4_C_60_0 this_0 x_6_0 lock_8_0) true) (and (and (and true true) (summary_8_function_f__59_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1)) (= error_0 0))) (interface_4_C_60_0 this_0 x_6_1 lock_8_1))))


(declare-fun |contract_initializer_22_C_60_0| (Int Int Int Bool Int Bool ) Bool)
(declare-fun |contract_initializer_entry_23_C_60_0| (Int Int Int Bool Int Bool ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_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_23_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1))))


(declare-fun |contract_initializer_after_init_24_C_60_0| (Int Int Int Bool Int Bool ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (contract_initializer_entry_23_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) true) true) (contract_initializer_after_init_24_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (contract_initializer_after_init_24_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) true) true) (contract_initializer_22_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1))))


(declare-fun |implicit_constructor_entry_25_C_60_0| (Int Int Int Bool Int Bool ) Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_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_25_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (implicit_constructor_entry_25_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) (and (contract_initializer_22_C_60_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_60_0 error_1 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (implicit_constructor_entry_25_C_60_0 error_0 this_0 x_6_0 lock_8_0 x_6_1 lock_8_1) (and (= error_1 0) (and (contract_initializer_22_C_60_0 error_1 this_0 x_6_1 lock_8_1 x_6_2 lock_8_2) true))) true) (summary_constructor_6_C_60_0 error_1 this_0 x_6_0 lock_8_0 x_6_2 lock_8_2))))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (summary_constructor_6_C_60_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_60_0 this_0 x_6_1 lock_8_1))))


(declare-fun |error_target_2_0| () Bool)
(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> (and (and (interface_4_C_60_0 this_0 x_6_0 lock_8_0) true) (and (and (and true true) (summary_8_function_f__59_60_0 error_0 this_0 x_6_0 lock_8_0 _i_38_0 x_6_1 lock_8_1 _i_38_1)) (= error_0 1))) error_target_2_0)))


(assert
(forall ( (_i_38_0 Int) (_i_38_1 Int) (_i_38_2 Int) (_i_38_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_30_0 Int) (expr_31_0 Int) (expr_32_1 Int) (expr_45_0 Int) (expr_47_0 Int) (expr_50_1 |tuple()|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_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_44_0 Int) (x_prev_44_1 Int) (x_prev_44_2 Int) (x_prev_44_3 Int))
(=> error_target_2_0 false)))
(check-sat)