Skip to content

Instantly share code, notes, and snippets.

@leonardoalt

leonardoalt/linear_unsat_div_with_slack_vars.smt2

Created August 12, 2021 11:55
Show Gist options
  • Save leonardoalt/77d72c7fb35eaced97ea3dea54eaa90e to your computer and use it in GitHub Desktop.
Save leonardoalt/77d72c7fb35eaced97ea3dea54eaa90e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
linear_unsat_div_with_slack_vars.smt2
(set-logic HORN)
(declare-fun |interface_0_C_19_0| (Int ) Bool)
(declare-fun |nondet_interface_1_C_19_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_C_19_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_C_19_0 error_0 this_0))))
(declare-fun |summary_3_function_f__18_19_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_19_0 error_0 this_0) true) (and (= error_0 0) (summary_3_function_f__18_19_0 error_1 this_0 x_2_0 x_2_1))) (nondet_interface_1_C_19_0 error_1 this_0))))
(declare-fun |block_4_function_f__18_19_0| (Int Int Int Int Int ) Bool)
(declare-fun |block_5_f_17_19_0| (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_6_0 Int) (y_6_1 Int))
(block_4_function_f__18_19_0 error_0 this_0 x_2_0 x_2_1 y_6_1)))
(assert
(forall ( (error_0 Int) (error_1 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int))
(=> (and (and (block_4_function_f__18_19_0 error_0 this_0 x_2_0 x_2_1 y_6_1) (and (and (and (and true (= error_0 0)) true) (and true (= x_2_1 x_2_0))) true)) true) (block_5_f_17_19_0 error_0 this_0 x_2_0 x_2_1 y_6_1))))
(declare-fun |block_6_return_function_f__18_19_0| (Int Int Int Int Int ) Bool)
(declare-fun |block_7_function_f__18_19_0| (Int Int Int Int Int ) Bool)
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (block_5_f_17_19_0 error_0 this_0 x_2_0 x_2_1 y_6_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (=> true (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_2_1) (and (=> true (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 y_6_2) (and (= y_6_2 expr_9_1) (and (=> true (and (>= expr_9_1 0) (<= expr_9_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_1 (ite (= expr_8_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_8_0 0) (< r_div_mod_0_0 expr_8_0))) (and (= (+ (* d_div_mod_0_0 expr_8_0) r_div_mod_0_0) expr_7_0) (and (=> true true) (and (= expr_8_0 2) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_2_1) (and (and (>= x_2_1 0) (<= x_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= y_6_1 0) true))))))))))))))))) (and (not expr_14_1) (= error_1 1))) (block_7_function_f__18_19_0 error_1 this_0 x_2_0 x_2_1 y_6_2))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (block_7_function_f__18_19_0 error_1 this_0 x_2_0 x_2_1 y_6_2) (summary_3_function_f__18_19_0 error_1 this_0 x_2_0 x_2_1))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (block_5_f_17_19_0 error_0 this_0 x_2_0 x_2_1 y_6_1) (and (= error_1 error_0) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (=> true (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_2_1) (and (=> true (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 y_6_2) (and (= y_6_2 expr_9_1) (and (=> true (and (>= expr_9_1 0) (<= expr_9_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_1 (ite (= expr_8_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_8_0 0) (< r_div_mod_0_0 expr_8_0))) (and (= (+ (* d_div_mod_0_0 expr_8_0) r_div_mod_0_0) expr_7_0) (and (=> true true) (and (= expr_8_0 2) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_2_1) (and (and (>= x_2_1 0) (<= x_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= y_6_1 0) true)))))))))))))))))) true) (block_6_return_function_f__18_19_0 error_1 this_0 x_2_0 x_2_1 y_6_2))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (block_6_return_function_f__18_19_0 error_0 this_0 x_2_0 x_2_1 y_6_1) true) true) (summary_3_function_f__18_19_0 error_0 this_0 x_2_0 x_2_1))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (interface_0_C_19_0 this_0) true) (and (and (and true true) (summary_3_function_f__18_19_0 error_0 this_0 x_2_0 x_2_1)) (= error_0 0))) (interface_0_C_19_0 this_0))))
(declare-fun |contract_initializer_8_C_19_0| (Int Int ) Bool)
(declare-fun |contract_initializer_entry_9_C_19_0| (Int Int ) Bool)
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and true (= error_0 0)) true) (contract_initializer_entry_9_C_19_0 error_0 this_0))))
(declare-fun |contract_initializer_after_init_10_C_19_0| (Int Int ) Bool)
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (contract_initializer_entry_9_C_19_0 error_0 this_0) true) true) (contract_initializer_after_init_10_C_19_0 error_0 this_0))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (contract_initializer_after_init_10_C_19_0 error_0 this_0) true) true) (contract_initializer_8_C_19_0 error_0 this_0))))
(declare-fun |implicit_constructor_entry_11_C_19_0| (Int Int ) Bool)
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (and true (= error_0 0)) true) true) (implicit_constructor_entry_11_C_19_0 error_0 this_0))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (implicit_constructor_entry_11_C_19_0 error_0 this_0) (and (contract_initializer_8_C_19_0 error_1 this_0) true)) (> error_1 0)) (summary_constructor_2_C_19_0 error_1 this_0))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (implicit_constructor_entry_11_C_19_0 error_0 this_0) (and (= error_1 0) (and (contract_initializer_8_C_19_0 error_1 this_0) true))) true) (summary_constructor_2_C_19_0 error_1 this_0))))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (summary_constructor_2_C_19_0 error_0 this_0) true) (and (and true true) (= error_0 0))) (interface_0_C_19_0 this_0))))
(declare-fun |error_target_2_0| () Bool)
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (x_2_2 Int) (y_6_0 Int) (y_6_1 Int) (y_6_2 Int))
(=> (and (and (interface_0_C_19_0 this_0) true) (and (and (and true true) (summary_3_function_f__18_19_0 error_0 this_0 x_2_0 x_2_1)) (= error_0 1))) error_target_2_0)))
(assert
(forall ( (d_div_mod_0_0 Int) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_13_0 Int) (expr_14_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Int) (r_div_mod_0_0 Int) (this_0 Int) (x_2_0 Int) (x_2_1 Int) (x_2_2 Int) (y_6_0 Int) (y_6_1 Int) (y_6_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