SMT-LIB · hansjoergschurr · Apr 14, 2025 · Mar 18, 2025 · Mar 18, 2025 · Mar 19, 2025
diff --git a/...QF_NIA/20250318-BohanLi/From_AProVE_2014__DivMinus.jar-obl-11__p28570_edge_closing_0.smt2 b/...QF_NIA/20250318-BohanLi/From_AProVE_2014__DivMinus.jar-obl-11__p28570_edge_closing_0.smt2
diff --git a/..._NIA/20250318-BohanLi/From_AProVE_2014__LessLeaves.jar-obl-10__p10014_edge_closing_0.smt2 b/..._NIA/20250318-BohanLi/From_AProVE_2014__LessLeaves.jar-obl-10__p10014_edge_closing_0.smt2
diff --git a/..._NIA/20250318-BohanLi/From_AProVE_2014__MainDelete.jar-obl-10__p10519_edge_closing_0.smt2 b/..._NIA/20250318-BohanLi/From_AProVE_2014__MainDelete.jar-obl-10__p10519_edge_closing_0.smt2
diff --git a/...emental/QF_NIA/20250318-BohanLi/From_AProVE_2014__Matrix.jar-obl-16__p10788_safety_0.smt2 b/...emental/QF_NIA/20250318-BohanLi/From_AProVE_2014__Matrix.jar-obl-16__p10788_safety_0.smt2
diff --git a/...l/QF_NIA/20250318-BohanLi/From_AProVE_2014__Matrix.jar-obl-16__p10803_terminationG_0.smt2 b/...l/QF_NIA/20250318-BohanLi/From_AProVE_2014__Matrix.jar-obl-16__p10803_terminationG_0.smt2
diff --git a/...l/QF_NIA/20250318-BohanLi/From_AProVE_2014__Matrix.jar-obl-16__p10849_edge_closing_0.smt2 b/...l/QF_NIA/20250318-BohanLi/From_AProVE_2014__Matrix.jar-obl-16__p10849_edge_closing_0.smt2
diff --git a/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12127_terminationG_0.smt2 b/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12127_terminationG_0.smt2
diff --git a/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12189_terminationG_0.smt2 b/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12189_terminationG_0.smt2
diff --git a/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12209_terminationG_0.smt2 b/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12209_terminationG_0.smt2
diff --git a/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12240_terminationG_0.smt2 b/...F_NIA/20250318-BohanLi/From_AProVE_2014__SortCount.jar-obl-10__p12240_terminationG_0.smt2
diff --git a/...20250318-BohanLi/From_AProVE_2014__TaylorSeriesRec.jar-obl-13__p12566_terminationG_0.smt2 b/...20250318-BohanLi/From_AProVE_2014__TaylorSeriesRec.jar-obl-13__p12566_terminationG_0.smt2
diff --git a/...hanLi/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31684_terminationG_0.smt2 b/...hanLi/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31684_terminationG_0.smt2
diff --git a/...hanLi/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31846_edge_closing_0.smt2 b/...hanLi/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31846_edge_closing_0.smt2
diff --git a/.../From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3364_edge_closing_0.smt2 b/.../From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3364_edge_closing_0.smt2
diff --git a/...50318-BohanLi/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7615_edge_closing_0.smt2 b/...50318-BohanLi/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7615_edge_closing_0.smt2
diff --git a/...50318-BohanLi/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7616_edge_closing_0.smt2 b/...50318-BohanLi/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7616_edge_closing_0.smt2
diff --git a/...hanLi/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__p9812_terminationG_0.smt2 b/...hanLi/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__p9812_terminationG_0.smt2
diff --git a/...tal/QF_NIA/20250318-BohanLi/From_T2__apchild-accepted-fail.t2__p15978_terminationG_0.smt2 b/...tal/QF_NIA/20250318-BohanLi/From_T2__apchild-accepted-fail.t2__p15978_terminationG_0.smt2
diff --git a/...tal/QF_NIA/20250318-BohanLi/From_T2__apchild-accepted-fail.t2__p15979_terminationG_0.smt2 b/...tal/QF_NIA/20250318-BohanLi/From_T2__apchild-accepted-fail.t2__p15979_terminationG_0.smt2
diff --git a/..._NIA/20250318-BohanLi/From_T2__apchild-accepted-fail.t2_fixed__p15779_terminationG_0.smt2 b/..._NIA/20250318-BohanLi/From_T2__apchild-accepted-fail.t2_fixed__p15779_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__apchild-live.t2__p16681_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__apchild-live.t2__p16681_terminationG_0.smt2
diff --git a/...mental/QF_NIA/20250318-BohanLi/From_T2__apchild-live.t2_fixed__p16560_terminationG_0.smt2 b/...mental/QF_NIA/20250318-BohanLi/From_T2__apchild-live.t2_fixed__p16560_terminationG_0.smt2
diff --git a/...ental/QF_NIA/20250318-BohanLi/From_T2__apchildlive-succeed.t2__p16430_terminationG_0.smt2 b/...ental/QF_NIA/20250318-BohanLi/From_T2__apchildlive-succeed.t2__p16430_terminationG_0.smt2
diff --git a/...ental/QF_NIA/20250318-BohanLi/From_T2__apchildlive-succeed.t2__p16456_edge_closing_0.smt2 b/...ental/QF_NIA/20250318-BohanLi/From_T2__apchildlive-succeed.t2__p16456_edge_closing_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__brp_withassume.t2__p17422_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__brp_withassume.t2__p17422_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__db2.t2_fixed__p18730_edge_closing_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__db2.t2_fixed__p18730_edge_closing_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__db3.t2__p18774_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__db3.t2__p18774_terminationG_0.smt2
diff --git a/..._NIA/20250318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.fixed.t2__p32592_terminationG_0.smt2 b/..._NIA/20250318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.fixed.t2__p32592_terminationG_0.smt2
diff --git a/..._NIA/20250318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.fixed.t2__p32601_terminationG_0.smt2 b/..._NIA/20250318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.fixed.t2__p32601_terminationG_0.smt2
diff --git a/..._NIA/20250318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.fixed.t2__p32602_terminationG_0.smt2 b/..._NIA/20250318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.fixed.t2__p32602_terminationG_0.smt2
diff --git a/...318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed.t2__p32671_terminationG_0.smt2 b/...318-BohanLi/From_T2__fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed.t2__p32671_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1.t2__p849_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1.t2__p849_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1.t2_fixed__p697_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1.t2_fixed__p697_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p626_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p626_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p639_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p639_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p659_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p659_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p673_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__fun1b.t2__p673_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__fun9.t2__p1233_edge_closing_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__fun9.t2__p1233_edge_closing_0.smt2
diff --git a/...al/QF_NIA/20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__p1654_edge_closing_0.smt2 b/...al/QF_NIA/20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__p1654_edge_closing_0.smt2
diff --git a/...al/QF_NIA/20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__p1655_edge_closing_0.smt2 b/...al/QF_NIA/20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__p1655_edge_closing_0.smt2
diff --git a/...20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__p1697_terminationG_0.smt2 b/...20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__p1697_terminationG_0.smt2
diff --git a/...20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__p1699_terminationG_0.smt2 b/...20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__p1699_terminationG_0.smt2
diff --git a/...20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__p1718_edge_closing_0.smt2 b/...20250318-BohanLi/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__p1718_edge_closing_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__hqr.t2__p1774_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__hqr.t2__p1774_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__hqr.t2_fixed__p1737_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__hqr.t2_fixed__p1737_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2051_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2051_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2127_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2127_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2150_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2150_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2278_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__janne_complex.t2__p2278_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__matmul.t2__p2658_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__matmul.t2__p2658_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3070_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3070_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3101_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3101_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3112_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3112_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3117_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3117_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3231_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3231_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3328_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__mc91test.t2__p3328_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__p_armc.t2__p6946_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__p_armc.t2__p6946_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__polyrank4.t2__p7528_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__polyrank4.t2__p7528_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__polyrank4.t2__p7536_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__polyrank4.t2__p7536_terminationG_0.smt2
diff --git a/...F_NIA/20250318-BohanLi/From_T2__rlft3.c.i.rlft3.pl.t2.fixed.t2__p8947_edge_closing_0.smt2 b/...F_NIA/20250318-BohanLi/From_T2__rlft3.c.i.rlft3.pl.t2.fixed.t2__p8947_edge_closing_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__sas2.t2__p21297_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__sas2.t2__p21297_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__sas2.t2__p21302_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__sas2.t2__p21302_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-3-new.t2__p21878_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-3-new.t2__p21878_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22519_safety_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22519_safety_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22620_safety_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22620_safety_0.smt2
diff --git a/...emental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22688_terminationG_0.smt2 b/...emental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22688_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22712_safety_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__slayer-4-filtered.t2__p22712_safety_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__sudoku.t2__p24877_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__sudoku.t2__p24877_terminationG_0.smt2
diff --git a/...IA/20250318-BohanLi/From_T2__svdcmp.c.i.svdcmp.pl.t2.fixed.t2__p24885_terminationG_0.smt2 b/...IA/20250318-BohanLi/From_T2__svdcmp.c.i.svdcmp.pl.t2.fixed.t2__p24885_terminationG_0.smt2
diff --git a/...IA/20250318-BohanLi/From_T2__svdcmp.c.i.svdcmp.pl.t2.fixed.t2__p24886_terminationG_0.smt2 b/...IA/20250318-BohanLi/From_T2__svdcmp.c.i.svdcmp.pl.t2.fixed.t2__p24886_terminationG_0.smt2
diff --git a/...8-BohanLi/From_T2__svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed.t2__p24940_edge_closing_0.smt2 b/...8-BohanLi/From_T2__svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed.t2__p24940_edge_closing_0.smt2
diff --git a/...50318-BohanLi/From_T2__tqli.c.i.tqli.pl.t2.nor.t2.rlgfixed.t2__p25079_terminationG_0.smt2 b/...50318-BohanLi/From_T2__tqli.c.i.tqli.pl.t2.nor.t2.rlgfixed.t2__p25079_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__tqli.t2__p25217_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__tqli.t2__p25217_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__tqli.t2_fixed__p25128_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__tqli.t2_fixed__p25128_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__weakness.t2__p25655_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__weakness.t2__p25655_terminationG_0.smt2
diff --git a/incremental/QF_NIA/20250318-BohanLi/From_T2__zeroconf.t2__p25775_terminationG_0.smt2 b/incremental/QF_NIA/20250318-BohanLi/From_T2__zeroconf.t2__p25775_terminationG_0.smt2
diff --git a/...BohanLi/Stroeder_15__4NestedWith3Variables_true-termination.c__p20247_terminationG_0.smt2 b/...BohanLi/Stroeder_15__4NestedWith3Variables_true-termination.c__p20247_terminationG_0.smt2
diff --git a/...r_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21912_terminationG_0.smt2 b/...r_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21912_terminationG_0.smt2
diff --git a/...r_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21979_terminationG_0.smt2 b/...r_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21979_terminationG_0.smt2
diff --git a/...er_15__ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c__p22124_terminationG_0.smt2 b/...er_15__ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c__p22124_terminationG_0.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0000.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0000.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0003.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0003.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0010.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0010.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0011.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0011.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0012.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0012.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0013.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0013.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0016.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0016.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0019.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0019.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0021.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0021.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0022.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0022.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0023.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0023.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0028.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0028.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0030.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0030.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0031.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0031.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0032.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0032.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0034.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0034.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0035.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0035.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0036.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0036.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0037.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0037.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0039.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0039.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0054.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0054.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0057.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0057.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0062.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0062.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0066.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0066.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0069.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0069.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0072.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0072.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0080.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0080.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0090.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0090.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0103.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0103.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0104.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0104.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0108.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0108.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0109.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0109.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0111.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0111.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0112.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0112.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0113.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0113.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0114.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0114.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0116.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0116.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0117.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0117.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0125.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0125.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0132.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0132.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0136.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0136.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0146.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0146.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0147.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0147.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0150.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0150.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0153.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0153.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0158.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0158.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0160.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0160.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0162.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0162.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0165.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0165.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0166.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0166.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0170.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0170.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0172.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0172.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0179.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0179.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0180.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0180.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0181.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0181.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0182.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0182.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0184.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0184.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0188.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0188.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0190.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0190.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0191.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0191.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0192.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0192.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0198.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0198.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0205.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0205.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0208.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0208.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0212.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0212.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0231.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0231.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0234.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0234.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0240.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0240.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0242.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0242.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0247.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0247.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0249.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0249.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0251.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0251.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0253.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0253.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0261.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0261.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0262.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0262.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0278.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0278.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0280.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0280.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0282.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0282.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0283.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0283.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0285.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0285.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0286.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0286.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0287.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0287.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0288.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0288.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0294.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0294.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0302.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0302.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0309.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0309.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0318.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0318.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0319.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0319.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0321.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0321.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0323.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0323.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0328.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0328.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0330.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0330.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0331.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0331.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0337.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0337.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0338.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0338.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0341.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0341.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0343.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0343.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0350.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0350.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0351.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0351.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0352.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0352.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0354.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0354.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0355.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0355.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0359.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0359.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0360.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0360.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0361.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0361.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0363.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0363.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0369.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0369.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0371.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0371.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0374.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0374.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0382.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0382.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0387.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0387.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0390.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0390.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0394.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0394.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0395.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0395.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0398.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0398.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0399.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0399.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0403.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0403.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0406.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0406.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0407.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0407.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0408.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0408.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0412.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0412.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0413.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0413.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0415.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0415.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0418.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0418.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0419.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0419.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0421.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0421.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0422.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0422.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0423.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0423.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0425.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0425.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0426.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0426.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0433.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0433.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0435.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0435.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0437.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0437.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0444.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0444.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0445.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0445.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0446.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0446.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0447.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0447.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0448.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0448.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0449.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0449.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0456.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0456.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0457.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0457.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0458.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0458.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0459.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0459.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0460.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0460.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0461.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0461.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0495.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0495.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0497.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0497.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0498.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0498.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0499.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0499.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0618.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0618.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0648.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0648.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0649.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0649.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0650.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0650.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0651.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0651.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0652.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0652.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0653.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0653.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0654.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0654.smt2
@@ -0,0 +1,137 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFBV)
+(set-info :source |
+Generated by: Certora
+Generated on: 2024-01-16
+Generator: The Certora Prover
+Application: Web3 security
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun x15 () (_ BitVec 256))
+(declare-fun x71 () (_ BitVec 256))
+(declare-fun x10 () (_ BitVec 256))
+(declare-fun x58 () (_ BitVec 256))
+(declare-fun x3 () (_ BitVec 256))
+(declare-fun x68 () (_ BitVec 256))
+(declare-fun x41 () (_ BitVec 256))
+(declare-fun x42 () (_ BitVec 256))
+(declare-fun x75 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x73 () (_ BitVec 256))
+(declare-fun x9 () (_ BitVec 256))
+(declare-fun x77 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x70 () (_ BitVec 256))
+(declare-fun x84 () (_ BitVec 256))
+(declare-fun x65 () (_ BitVec 256))
+(declare-fun x62 () (_ BitVec 256))
+(declare-fun x61 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x27 () (_ BitVec 256))
+(declare-fun x48 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x11 () (_ BitVec 256))
+(declare-fun x63 () (_ BitVec 256))
+(declare-fun x25 () (_ BitVec 256))
+(declare-fun x74 () (_ BitVec 256))
+(declare-fun x5 () Bool)
+(declare-fun x66 () (_ BitVec 256))
+(declare-fun x21 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x45 ((_ BitVec 256)) Bool)
+(declare-fun x64 () (_ BitVec 256))
+(declare-fun x35 () Bool)
+(declare-fun x7 () (_ BitVec 256))
+(declare-fun x56 () (_ BitVec 256))
+(declare-fun x2 () (_ BitVec 256))
+(declare-fun x4 () Bool)
+(declare-fun x54 () (_ BitVec 256))
+(declare-fun x22 () (_ BitVec 256))
+(declare-fun x47 () (_ BitVec 256))
+(declare-fun x1 () (_ BitVec 256))
+(declare-fun x33 () (_ BitVec 256))
+(declare-fun x23 () (_ BitVec 256))
+(declare-fun x57 () (_ BitVec 256))
+(declare-fun x17 () (_ BitVec 256))
+(declare-fun x14 () Bool)
+(declare-fun x40 () (_ BitVec 256))
+(declare-fun x72 () (_ BitVec 256))
+(declare-fun x24 () (_ BitVec 256))
+(declare-fun x26 () (_ BitVec 256))
+(declare-fun x59 () (_ BitVec 256))
+(declare-fun x83 () (_ BitVec 256))
+(declare-fun x49 () (_ BitVec 256))
+(declare-fun x12 () (_ BitVec 256))
+(declare-fun x34 () (_ BitVec 256))
+(declare-fun x13 ((_ BitVec 256) (_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))
+(declare-fun x79 () (_ BitVec 256))
+(declare-fun x67 () (_ BitVec 256))
+(declare-fun x69 () (_ BitVec 256))
+(declare-fun x51 () (_ BitVec 256))
+(declare-fun x44 () (_ BitVec 256))
+(declare-fun x53 () Bool)
+(declare-fun x18 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x30 () (_ BitVec 256))
+(declare-fun x8 () (_ BitVec 256))
+(declare-fun x50 () Bool)
+(declare-fun x81 () (_ BitVec 256))
+(declare-fun x28 () (_ BitVec 256))
+(declare-fun x43 () (_ BitVec 256))
+(declare-fun x46 () (_ BitVec 256))
+(declare-fun x80 () (_ BitVec 256))
+(declare-fun x37 () (_ BitVec 256))
+(declare-fun x36 () (_ BitVec 256))
+(declare-fun x20 () (_ BitVec 256))
+(declare-fun x19 () (_ BitVec 256))
+(declare-fun x32 () Bool)
+(declare-fun x31 () (_ BitVec 256))
+(declare-fun x82 () (_ BitVec 256))
+(declare-fun x29 () (_ BitVec 256))
+(declare-fun x52 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x76 () (_ BitVec 256))
+(define-fun x78 ((x39 (_ BitVec 256)) (x6 (_ BitVec 256))) Bool (= x39 (bvudiv (bvmul x6 x39) x6)))
+(define-fun x38 ((x39 (_ BitVec 256)) (x6 (_ BitVec 256))) Bool (= x39 (bvsdiv (bvmul x39 x6) x6)))
+(define-fun x16 ((x39 (_ BitVec 256)) (x6 (_ BitVec 256))) Bool (= x39 (bvsdiv (bvmul x6 x39) x6)))
+(define-fun x60 ((x55 (_ BitVec 256))) (_ BitVec 256) (ite (= x55 x46) x71 (x77 x55)))
+(assert (=> (bvule x46 (_ bv10000 256)) (= (x18 x46) (_ bv0 256))))
+(assert (= (_ bv64 256) (x21 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (not (x45 (x13 (_ bv64 256) x19 (_ bv2 256)))))
+(assert (x45 (_ bv4294967295 256)))
+(assert (x45 (_ bv115792089237316195423570985008687907853269984665640564039457 256)))
+(assert (=> (bvuge (_ bv10000 256) x23) (= (_ bv0 256) (x18 x23))))
+(assert (bvugt (x13 (_ bv64 256) x31 (_ bv2 256)) (_ bv10000 256)))
+(assert (= (_ bv0 256) (x18 (_ bv57896044618658097711785492504343953926634992332820282019728792003956564819967 256))))
+(assert (= (x18 (_ bv404098525 256)) (_ bv0 256)))
+(assert (= (_ bv0 256) (x18 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256))))
+(assert (= (_ bv0 256) (x18 (_ bv1889567281 256))))
+(assert (= x31 (x75 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (= (_ bv0 256) (x18 (_ bv115792089237316195423570985008687907853269984665640564039457 256))))
+(assert (=> (bvuge (_ bv10000 256) x19) (= (_ bv0 256) (x18 x19))))
+(assert (= (x13 (_ bv64 256) x31 (_ bv2 256)) (x18 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (= (x75 (x13 (_ bv64 256) x19 (_ bv2 256))) x19))
+(assert (= (x18 (x13 (_ bv64 256) x19 (_ bv2 256))) (x13 (_ bv64 256) x19 (_ bv2 256))))
+(assert (= (x18 (_ bv1289409798 256)) (_ bv0 256)))
+(assert (x45 (_ bv649617121 256)))
+(assert (= (x48 (x13 (_ bv64 256) x19 (_ bv2 256))) (_ bv2 256)))
+(assert (=> (bvule x31 (_ bv10000 256)) (= (_ bv0 256) (x18 x31))))
+(assert (= (x18 (_ bv105312291668557186697918027683670432318895095400549111254310977535 256)) (_ bv0 256)))
+(assert (not (x45 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (x45 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)))
+(assert (x45 (_ bv1289409798 256)))
+(assert (= (_ bv64 256) (x21 (x13 (_ bv64 256) x19 (_ bv2 256)))))
+(assert (= (_ bv0 256) (x18 (_ bv1461501637330902918203684832716283019655932542975 256))))
+(assert (not x5))
+(assert (= (x18 (_ bv649617121 256)) (_ bv0 256)))
+(assert (= (x18 (_ bv1000000000000000000 256)) (_ bv0 256)))
+(assert (x45 (_ bv1889567281 256)))
+(assert (x45 (_ bv105312291668557186697918027683670432318895095400549111254310977535 256)))
+(assert (x45 (_ bv1461501637330902918203684832716283019655932542975 256)))
+(assert (x45 (_ bv1000000000000000000 256)))
+(assert (= (x18 (_ bv4294967295 256)) (_ bv0 256)))
+(assert (=> (bvuge (_ bv10000 256) x47) (= (_ bv0 256) (x18 x47))))
+(assert (= true x32))
+(assert (bvult (_ bv10000 256) (x13 (_ bv64 256) x19 (_ bv2 256))))
+(assert (x45 (_ bv404098525 256)))
+(assert (= (_ bv2 256) (x48 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (=> (bvuge (_ bv10000 256) x20) (= (x18 x20) (_ bv0 256))))
+(assert (x45 (_ bv57896044618658097711785492504343953926634992332820282019728792003956564819967 256)))
+(assert (= x5 (=> (and (and (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x47) (bvule (_ bv0 256) x25) (= x33 (_ bv0 256)) (bvuge x9 (_ bv0 256)) (bvule x20 (_ bv1461501637330902918203684832716283019655932542975 256)) (= x50 (bvugt (x61 x23) (_ bv0 256))) (bvule x11 (_ bv57896044618658097711785492504343953926634992332820282019728792003956564819967 256)) (bvuge x47 (_ bv1 256)) (bvuge (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256) x59) (= (bvugt (x61 x20) (_ bv0 256)) x53) (bvuge (_ bv4294967295 256) x73) (not (= x23 x20)) (bvule (_ bv0 256) x70) (= x27 (_ bv4 256)) x4 (not (= x20 x47)) (bvuge x59 (_ bv0 256)) (= x34 (_ bv404098525 256)) (bvule x70 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)) (bvule x23 (_ bv1461501637330902918203684832716283019655932542975 256)) (bvuge x23 (_ bv1 256)) (bvule (_ bv4 256) x11) (bvule (_ bv0 256) x8) (= x30 (x61 x20)) (= (bvult (_ bv0 256) (x61 x47)) x4) (bvuge x7 (_ bv0 256)) (bvule x7 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)) (bvule (_ bv1 256) x20) (bvule (_ bv0 256) x73) (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x67) (= (_ bv36 256) x1) (bvule (_ bv0 256) x12) (bvuge x30 (_ bv1 256)) (bvule x57 (_ bv115792089237316195423570985008687907853269984665640564039457 256)) (bvule (_ bv0 256) x67) x50 (not (= x23 x47)) (bvule x62 (_ bv1461501637330902918203684832716283019655932542975 256)) (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x9) (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x65) (bvule x25 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)) x53 (bvule (_ bv0 256) x65) (bvuge (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256) x8) (bvule (_ bv0 256) x62) (bvule x12 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256))) (and (and (= (_ bv36 256) x80) (= x57 x69) (= x29 (bvudiv x17 (_ bv1000000000000000000 256))) (bvule (_ bv1 256) x15) (= x17 (bvmul x69 (_ bv1000000000000000000 256))) (= (bvudiv x17 x74) x82) (= x69 x29) (= x10 (_ bv1289409798 256)) (= x69 x2) (bvule (_ bv1 256) x74) (bvule x74 (_ bv105312291668557186697918027683670432318895095400549111254310977535 256)) (= x15 (x61 x20))) (and (and (= x28 (x61 x23)) x35 (= x49 (x13 (_ bv64 256) x31 (_ bv2 256))) (= (bvule x82 x58) x35) (= x31 x84) (= (_ bv1889567281 256) x63) (= x20 x31) (bvule (_ bv1 256) x28) (= (x52 x49) x58)) (and (and (= (x61 x20) x66) (= (_ bv404098525 256) x56) (bvuge x66 (_ bv1 256)) (= (x60 x23) x83) (= x68 (_ bv4 256)) (= x24 (_ bv649617121 256)) (= x81 (_ bv36 256)) (= x71 x79) (= x71 (x77 x46)) (= x37 x83) (= (x61 x23) x40) (bvuge x40 (_ bv1 256)) (= x46 x9)) (and (and (= x64 x36) (= x72 (bvudiv x76 x74)) (bvule (_ bv1 256) x54) (= x42 (_ bv36 256)) (= (bvmul (_ bv1000000000000000000 256) x64) x76) (= x64 x26) (= (x61 x20) x54) (= x57 x64) (= x36 (bvudiv x76 (_ bv1000000000000000000 256))) (= x22 (_ bv1289409798 256))) (and (bvuge x44 (_ bv1 256)) (= x19 x43) (= x20 x19) (= x3 (x52 x41)) (= (x61 x23) x44) (= (x13 (_ bv64 256) x19 (_ bv2 256)) x41) (= x14 (bvuge x3 x72)) (= x51 (_ bv1889567281 256)))))))) x14)))
+(check-sat)
+(exit)