Skip to content

Instantly share code, notes, and snippets.

@leonardoalt

leonardoalt/sum_sat.smt2

Created August 12, 2021 11:54
Show Gist options
  • Save leonardoalt/b60b83a6946bc7cc2b72e0ab6dd8c561 to your computer and use it in GitHub Desktop.
Save leonardoalt/b60b83a6946bc7cc2b72e0ab6dd8c561 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sum_sat.smt2
(set-logic HORN)
(declare-fun |interface_0_C_33_0| (Int ) Bool)
(declare-fun |nondet_interface_1_C_33_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_C_33_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_C_33_0 error_0 this_0))))
(declare-fun |summary_3_function_f__32_33_0| (Int Int Int Int Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int))
(=> (and (and (nondet_interface_1_C_33_0 error_0 this_0) true) (and (= error_0 0) (summary_3_function_f__32_33_0 error_1 this_0 x_2_0 y_4_0 x_2_1 y_4_1))) (nondet_interface_1_C_33_0 error_1 this_0))))
(declare-fun |block_4_function_f__32_33_0| (Int Int Int Int Int Int Int ) Bool)
(declare-fun |block_5_f_31_33_0| (Int Int Int Int Int Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int))
(block_4_function_f__32_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_1)))
(assert
(forall ( (error_0 Int) (error_1 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int))
(=> (and (and (block_4_function_f__32_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_1) (and (and (and (and true (= error_0 0)) true) (and (and true (= x_2_1 x_2_0)) (= y_4_1 y_4_0))) true)) true) (block_5_f_31_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_1))))
(declare-fun |block_6_return_function_f__32_33_0| (Int Int Int Int Int Int Int ) Bool)
(declare-fun |block_7_function_f__32_33_0| (Int Int Int Int Int Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (block_5_f_31_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_1) (and (= expr_28_1 (< expr_26_0 expr_27_0)) (and (=> true true) (and (= expr_27_0 1000) (and (=> true (and (>= expr_26_0 0) (<= expr_26_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_0 z_20_2) (and (= z_20_2 expr_23_1) (and (=> true (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (+ expr_21_0 expr_22_0)) (and (=> true (and (>= expr_22_0 0) (<= expr_22_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_22_0 y_4_1) (and (=> true (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_2_1) (and (=> true expr_16_1) (and (= expr_16_1 (< expr_14_0 expr_15_0)) (and (=> true true) (and (= expr_15_0 100) (and (=> true (and (>= expr_14_0 0) (<= expr_14_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_0 y_4_1) (and (=> true expr_10_1) (and (= expr_10_1 (< expr_8_0 expr_9_0)) (and (=> true true) (and (= expr_9_0 100) (and (=> true (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_2_1) (and (and (>= y_4_1 0) (<= y_4_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_2_1 0) (<= x_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= z_20_1 0) true)))))))))))))))))))))))))))) (and (not expr_28_1) (= error_1 1))) (block_7_function_f__32_33_0 error_1 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_2))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (block_7_function_f__32_33_0 error_1 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_2) (summary_3_function_f__32_33_0 error_1 this_0 x_2_0 y_4_0 x_2_1 y_4_1))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (block_5_f_31_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_1) (and (= error_1 error_0) (and (= expr_28_1 (< expr_26_0 expr_27_0)) (and (=> true true) (and (= expr_27_0 1000) (and (=> true (and (>= expr_26_0 0) (<= expr_26_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_0 z_20_2) (and (= z_20_2 expr_23_1) (and (=> true (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (+ expr_21_0 expr_22_0)) (and (=> true (and (>= expr_22_0 0) (<= expr_22_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_22_0 y_4_1) (and (=> true (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_2_1) (and (=> true expr_16_1) (and (= expr_16_1 (< expr_14_0 expr_15_0)) (and (=> true true) (and (= expr_15_0 100) (and (=> true (and (>= expr_14_0 0) (<= expr_14_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_0 y_4_1) (and (=> true expr_10_1) (and (= expr_10_1 (< expr_8_0 expr_9_0)) (and (=> true true) (and (= expr_9_0 100) (and (=> true (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_2_1) (and (and (>= y_4_1 0) (<= y_4_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_2_1 0) (<= x_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= z_20_1 0) true))))))))))))))))))))))))))))) true) (block_6_return_function_f__32_33_0 error_1 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_2))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (block_6_return_function_f__32_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1 z_20_1) true) true) (summary_3_function_f__32_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (interface_0_C_33_0 this_0) true) (and (and (and true true) (summary_3_function_f__32_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1)) (= error_0 0))) (interface_0_C_33_0 this_0))))
(declare-fun |contract_initializer_8_C_33_0| (Int Int ) Bool)
(declare-fun |contract_initializer_entry_9_C_33_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and true (= error_0 0)) true) (contract_initializer_entry_9_C_33_0 error_0 this_0))))
(declare-fun |contract_initializer_after_init_10_C_33_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (contract_initializer_entry_9_C_33_0 error_0 this_0) true) true) (contract_initializer_after_init_10_C_33_0 error_0 this_0))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (contract_initializer_after_init_10_C_33_0 error_0 this_0) true) true) (contract_initializer_8_C_33_0 error_0 this_0))))
(declare-fun |implicit_constructor_entry_11_C_33_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (and true (= error_0 0)) true) true) (implicit_constructor_entry_11_C_33_0 error_0 this_0))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (implicit_constructor_entry_11_C_33_0 error_0 this_0) (and (contract_initializer_8_C_33_0 error_1 this_0) true)) (> error_1 0)) (summary_constructor_2_C_33_0 error_1 this_0))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (implicit_constructor_entry_11_C_33_0 error_0 this_0) (and (= error_1 0) (and (contract_initializer_8_C_33_0 error_1 this_0) true))) true) (summary_constructor_2_C_33_0 error_1 this_0))))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_4_0 Int) (y_4_1 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (summary_constructor_2_C_33_0 error_0 this_0) true) (and (and true true) (= error_0 0))) (interface_0_C_33_0 this_0))))
(declare-fun |error_target_2_0| () Bool)
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (x_2_2 Int) (y_4_0 Int) (y_4_1 Int) (y_4_2 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 Int))
(=> (and (and (interface_0_C_33_0 this_0) true) (and (and (and true true) (summary_3_function_f__32_33_0 error_0 this_0 x_2_0 y_4_0 x_2_1 y_4_1)) (= error_0 1))) error_target_2_0)))
(assert
(forall ( (error_0 Int) (error_1 Int) (expr_10_1 Bool) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Bool) (expr_21_0 Int) (expr_22_0 Int) (expr_23_1 Int) (expr_26_0 Int) (expr_27_0 Int) (expr_28_1 Bool) (expr_8_0 Int) (expr_9_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (x_2_2 Int) (y_4_0 Int) (y_4_1 Int) (y_4_2 Int) (z_20_0 Int) (z_20_1 Int) (z_20_2 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