Code Snippets SMT

Short texts SMT 🧑‍💻 Code snippets SMT ✍️ Reading lists SMT 👀

simple_sat.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)) (=> […]

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)) (=> […]

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) […]

mutex_sat.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) […]

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 […]