simple_unsat.smt2

(set-logic HORN)

(declare-fun |interface_0_C_13_0| (Int ) Bool)
(declare-fun |nondet_interface_1_C_13_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_C_13_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_C_13_0 error_0 this_0))))


(declare-fun |summary_3_function_f__12_13_0| (Int Int Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (nondet_interface_1_C_13_0 error_0 this_0) true) (and (= error_0 0) (summary_3_function_f__12_13_0 error_1 this_0 x_2_0 x_2_1))) (nondet_interface_1_C_13_0 error_1 this_0))))


(declare-fun |block_4_function_f__12_13_0| (Int Int Int Int ) Bool)
(declare-fun |block_5_f_11_13_0| (Int Int Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(block_4_function_f__12_13_0 error_0 this_0 x_2_0 x_2_1)))


(assert
(forall ( (error_0 Int) (error_1 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (block_4_function_f__12_13_0 error_0 this_0 x_2_0 x_2_1) (and (and (and (and true (= error_0 0)) true) (and true (= x_2_1 x_2_0))) true)) true) (block_5_f_11_13_0 error_0 this_0 x_2_0 x_2_1))))


(declare-fun |block_6_return_function_f__12_13_0| (Int Int Int Int ) Bool)
(declare-fun |block_7_function_f__12_13_0| (Int Int Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (block_5_f_11_13_0 error_0 this_0 x_2_0 x_2_1) (and (= expr_8_1 (> expr_6_0 expr_7_0)) (and (=> true true) (and (= expr_7_0 0) (and (=> true (and (>= expr_6_0 0) (<= expr_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_6_0 x_2_1) (and (and (>= x_2_1 0) (<= x_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (not expr_8_1) (= error_1 1))) (block_7_function_f__12_13_0 error_1 this_0 x_2_0 x_2_1))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (block_7_function_f__12_13_0 error_1 this_0 x_2_0 x_2_1) (summary_3_function_f__12_13_0 error_1 this_0 x_2_0 x_2_1))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (block_5_f_11_13_0 error_0 this_0 x_2_0 x_2_1) (and (= error_1 error_0) (and (= expr_8_1 (> expr_6_0 expr_7_0)) (and (=> true true) (and (= expr_7_0 0) (and (=> true (and (>= expr_6_0 0) (<= expr_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_6_0 x_2_1) (and (and (>= x_2_1 0) (<= x_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) true) (block_6_return_function_f__12_13_0 error_1 this_0 x_2_0 x_2_1))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (block_6_return_function_f__12_13_0 error_0 this_0 x_2_0 x_2_1) true) true) (summary_3_function_f__12_13_0 error_0 this_0 x_2_0 x_2_1))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (interface_0_C_13_0 this_0) true) (and (and (and true true) (summary_3_function_f__12_13_0 error_0 this_0 x_2_0 x_2_1)) (= error_0 0))) (interface_0_C_13_0 this_0))))


(declare-fun |contract_initializer_8_C_13_0| (Int Int ) Bool)
(declare-fun |contract_initializer_entry_9_C_13_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and true (= error_0 0)) true) (contract_initializer_entry_9_C_13_0 error_0 this_0))))


(declare-fun |contract_initializer_after_init_10_C_13_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (contract_initializer_entry_9_C_13_0 error_0 this_0) true) true) (contract_initializer_after_init_10_C_13_0 error_0 this_0))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (contract_initializer_after_init_10_C_13_0 error_0 this_0) true) true) (contract_initializer_8_C_13_0 error_0 this_0))))


(declare-fun |implicit_constructor_entry_11_C_13_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (and true (= error_0 0)) true) true) (implicit_constructor_entry_11_C_13_0 error_0 this_0))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (implicit_constructor_entry_11_C_13_0 error_0 this_0) (and (contract_initializer_8_C_13_0 error_1 this_0) true)) (> error_1 0)) (summary_constructor_2_C_13_0 error_1 this_0))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (implicit_constructor_entry_11_C_13_0 error_0 this_0) (and (= error_1 0) (and (contract_initializer_8_C_13_0 error_1 this_0) true))) true) (summary_constructor_2_C_13_0 error_1 this_0))))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int))
(=> (and (and (summary_constructor_2_C_13_0 error_0 this_0) true) (and (and true true) (= error_0 0))) (interface_0_C_13_0 this_0))))


(declare-fun |error_target_2_0| () Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (x_2_2 Int))
(=> (and (and (interface_0_C_13_0 this_0) true) (and (and (and true true) (summary_3_function_f__12_13_0 error_0 this_0 x_2_0 x_2_1)) (= error_0 1))) error_target_2_0)))


(assert
(forall ( (error_0 Int) (error_1 Int) (expr_6_0 Int) (expr_7_0 Int) (expr_8_1 Bool) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (x_2_2 Int))
(=> error_target_2_0 false)))
(check-sat)