From 67553256b965c096caa6389fc49cee96619dc65c Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 2 Nov 2023 15:40:13 +0100 Subject: [PATCH] Fixed problem with CHC parsing tests --- .../mit/theta/xcfa/cli/XcfaCliParseTest.kt | 4 - .../chc-LIA-nonlin-Arrays-nonrecADT_000.smt2 | 5209 ----------------- .../theta/xcfa/passes/ProcedurePassManager.kt | 1 + 3 files changed, 1 insertion(+), 5213 deletions(-) delete mode 100644 subprojects/xcfa/xcfa-cli/src/test/resources/chc/chc-LIA-nonlin-Arrays-nonrecADT_000.smt2 diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliParseTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliParseTest.kt index 741b263fe6..4cb12efd10 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliParseTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliParseTest.kt @@ -20,7 +20,6 @@ import hu.bme.mit.theta.xcfa.cli.XcfaCli.Companion.main import org.junit.jupiter.params.ParameterizedTest import org.junit.jupiter.params.provider.Arguments import org.junit.jupiter.params.provider.MethodSource -import java.util.* import java.util.stream.Stream import kotlin.io.path.createTempDirectory @@ -95,19 +94,16 @@ class XcfaCliParseTest { Arguments.of("/chc/chc-LIA-Arrays_000.smt2", ChcFrontend.ChcTransformation.PORTFOLIO), Arguments.of("/chc/chc-LIA-Lin-Arrays_000.smt2", ChcFrontend.ChcTransformation.PORTFOLIO), Arguments.of("/chc/chc-LIA-Lin_000.smt2", ChcFrontend.ChcTransformation.PORTFOLIO), - Arguments.of("/chc/chc-LIA-nonlin-Arrays-nonrecADT_000.smt2", ChcFrontend.ChcTransformation.PORTFOLIO), Arguments.of("/chc/chc-LIA_000.smt2", ChcFrontend.ChcTransformation.PORTFOLIO), // Arguments.of("/chc/chc-LIA-Arrays_000.smt2", ChcFrontend.ChcTransformation.FORWARD), // nonlin Arguments.of("/chc/chc-LIA-Lin-Arrays_000.smt2", ChcFrontend.ChcTransformation.FORWARD), Arguments.of("/chc/chc-LIA-Lin_000.smt2", ChcFrontend.ChcTransformation.FORWARD), - Arguments.of("/chc/chc-LIA-nonlin-Arrays-nonrecADT_000.smt2", ChcFrontend.ChcTransformation.FORWARD), // Arguments.of("/chc/chc-LIA_000.smt2", ChcFrontend.ChcTransformation.FORWARD), // nonlin Arguments.of("/chc/chc-LIA-Arrays_000.smt2", ChcFrontend.ChcTransformation.BACKWARD), Arguments.of("/chc/chc-LIA-Lin-Arrays_000.smt2", ChcFrontend.ChcTransformation.BACKWARD), Arguments.of("/chc/chc-LIA-Lin_000.smt2", ChcFrontend.ChcTransformation.BACKWARD), - Arguments.of("/chc/chc-LIA-nonlin-Arrays-nonrecADT_000.smt2", ChcFrontend.ChcTransformation.BACKWARD), Arguments.of("/chc/chc-LIA_000.smt2", ChcFrontend.ChcTransformation.BACKWARD), ) } diff --git a/subprojects/xcfa/xcfa-cli/src/test/resources/chc/chc-LIA-nonlin-Arrays-nonrecADT_000.smt2 b/subprojects/xcfa/xcfa-cli/src/test/resources/chc/chc-LIA-nonlin-Arrays-nonrecADT_000.smt2 deleted file mode 100644 index ed5bfd9131..0000000000 --- a/subprojects/xcfa/xcfa-cli/src/test/resources/chc/chc-LIA-nonlin-Arrays-nonrecADT_000.smt2 +++ /dev/null @@ -1,5209 +0,0 @@ -; ./prepared/solidity/./unit_tests/operators/delete_multid_array.sol_16_000.smt2 -(set-logic HORN) - -(declare-datatypes ((abi_type 0)) (((abi_type )))) -(declare-datatypes ((uint_array_tuple 0)) (((uint_array_tuple (uint_array_tuple_accessor_array (Array Int Int)) (uint_array_tuple_accessor_length Int))))) -(declare-datatypes ((uint_array_tuple_array_tuple 0)) (((uint_array_tuple_array_tuple (uint_array_tuple_array_tuple_accessor_array (Array Int uint_array_tuple)) (uint_array_tuple_array_tuple_accessor_length Int))))) -(declare-datatypes ((bytes_tuple 0)) (((bytes_tuple (bytes_tuple_accessor_array (Array Int Int)) (bytes_tuple_accessor_length Int))))) -(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int)))))) -(declare-datatypes ((tx_type 0)) (((tx_type (block.basefee Int) (block.chainid Int) (block.coinbase Int) (block.difficulty Int) (block.gaslimit Int) (block.number Int) (block.timestamp Int) (blockhash (Array Int Int)) (msg.data bytes_tuple) (msg.sender Int) (msg.sig Int) (msg.value Int) (tx.gasprice Int) (tx.origin Int))))) -(declare-datatypes ((ecrecover_input_type 0)) (((ecrecover_input_type (hash Int) (v Int) (r Int) (s Int))))) -(declare-datatypes ((crypto_type 0)) (((crypto_type (ecrecover (Array ecrecover_input_type Int)) (keccak256 (Array bytes_tuple Int)) (ripemd160 (Array bytes_tuple Int)) (sha256 (Array bytes_tuple Int)))))) - -(declare-fun |block_39_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_60_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_11_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |contract_initializer_entry_88_C_335_0| ( Int Int abi_type crypto_type tx_type state_type state_type uint_array_tuple uint_array_tuple_array_tuple uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |summary_19_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_17_function_setA__300_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_70_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_31_return_function_f__58_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_42_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_41_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_56_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_65_return_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_74_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |summary_6_function_q__27_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_37_return_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_73_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_85_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_34_function_f__58_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |summary_9_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_82_return_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_8_function_f__58_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_36_g_101_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |error_target_45_0| ( ) Bool) -(declare-fun |summary_15_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_24_function_p__16_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_44_h_149_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_20_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_75_function_setA__300_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_43_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_14_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_86_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_constructor_2_C_335_0| ( Int Int abi_type crypto_type tx_type state_type state_type uint_array_tuple uint_array_tuple_array_tuple uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_38_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_48_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_77_return_function_setA__300_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_54_i_204_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_71_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_22_p_15_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_21_function_p__16_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |contract_initializer_after_init_89_C_335_0| ( Int Int abi_type crypto_type tx_type state_type state_type uint_array_tuple uint_array_tuple_array_tuple uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_79_function_setA__300_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |summary_7_function_f__58_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_49_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_27_return_function_q__27_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_58_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_16_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_76_setA_299_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_46_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_51_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_13_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |implicit_constructor_entry_90_C_335_0| ( Int Int abi_type crypto_type tx_type state_type state_type uint_array_tuple uint_array_tuple_array_tuple uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_28_function_q__27_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |interface_0_C_335_0| ( Int abi_type crypto_type state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_72_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_29_function_f__58_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_23_return_function_p__16_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_80_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_68_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_25_function_q__27_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_30_f_57_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |summary_3_function_p__16_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_40_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_4_function_p__16_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_83_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |contract_initializer_87_C_335_0| ( Int Int abi_type crypto_type tx_type state_type state_type uint_array_tuple uint_array_tuple_array_tuple uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_35_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |summary_12_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_69_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |summary_5_function_q__27_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |summary_10_function_g__102_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_57_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_63_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_53_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_66_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_47_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_50_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_33_function_f__58_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |summary_18_function_setA__300_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_52_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_67_function_j__279_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_59_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_61_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_26_q_26_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple state_type uint_array_tuple uint_array_tuple_array_tuple ) Bool) -(declare-fun |block_55_return_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_32_function_f__58_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_81_setB_333_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_78_function_setA__300_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int ) Bool) -(declare-fun |block_64_j_278_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int Int ) Bool) -(declare-fun |block_84_function_setB__334_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_62_function_i__205_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) -(declare-fun |block_45_return_function_h__150_335_0| ( Int Int abi_type crypto_type tx_type state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int state_type uint_array_tuple uint_array_tuple_array_tuple Int Int Int ) Bool) - -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - true - ) - (block_21_function_p__16_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (block_21_function_p__16_335_0 G J C F K H A D I B E) - (and (= B A) (= I H) (= G 0) (= E D)) - ) - (block_22_p_15_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G crypto_type) (H Int) (I uint_array_tuple) (J uint_array_tuple) (K Int) (L state_type) (M state_type) (N Int) (O tx_type) ) - (=> - (and - (block_22_p_15_335_0 H N D G O L A E M B F) - (and (= I B) - (= C J) - (= (uint_array_tuple_accessor_length J) - (+ 1 (uint_array_tuple_accessor_length I))) - (= K 0) - (>= (uint_array_tuple_accessor_length I) 0) - (>= K 0) - (not (<= 115792089237316195423570985008687907853269984665640564039457584007913129639933 - (uint_array_tuple_accessor_length I))) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= (uint_array_tuple_accessor_array J) - (store (uint_array_tuple_accessor_array I) - (uint_array_tuple_accessor_length I) - 0))) - ) - (block_23_return_function_p__16_335_0 H N D G O L A E M C F) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (block_23_return_function_p__16_335_0 G J C F K H A D I B E) - true - ) - (summary_3_function_p__16_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - true - ) - (block_24_function_p__16_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) ) - (=> - (and - (block_24_function_p__16_335_0 I P D H Q L A E M B F) - (summary_3_function_p__16_335_0 J P D H Q N B F O C G) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 106)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 136)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 232)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 154)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= N (state_type a!1)) - (= M L) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 2598930538) - (= I 0) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_4_function_p__16_335_0 J P D H Q L A E O C G) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (summary_4_function_p__16_335_0 G J C F K H A D I B E) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (summary_6_function_q__27_335_0 G J C F K H A D I B E) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (summary_8_function_f__58_335_0 G J C F K H A D N L I B E O M) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (summary_10_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (summary_12_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (summary_14_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (summary_16_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (summary_18_function_setA__300_335_0 G J C F K H A D L N I B E M O) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (summary_20_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - (interface_0_C_335_0 J C F H A D) - (= G 0) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (summary_constructor_2_C_335_0 G J C F K H I A D B E) - (and (= G 0) - (>= (tx.origin K) 0) - (>= (tx.gasprice K) 0) - (>= (msg.value K) 0) - (>= (msg.sender K) 0) - (>= (block.timestamp K) 0) - (>= (block.number K) 0) - (>= (block.gaslimit K) 0) - (>= (block.difficulty K) 0) - (>= (block.coinbase K) 0) - (>= (block.chainid K) 0) - (>= (block.basefee K) 0) - (<= (tx.origin K) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender K) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase K) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= (msg.value K) 0)) - ) - (interface_0_C_335_0 J C F I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - true - ) - (block_25_function_q__27_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (block_25_function_q__27_335_0 G J C F K H A D I B E) - (and (= B A) (= I H) (= G 0) (= E D)) - ) - (block_26_q_26_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J uint_array_tuple_array_tuple) (K uint_array_tuple_array_tuple) (L uint_array_tuple_array_tuple) (M uint_array_tuple) (N uint_array_tuple) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) ) - (=> - (and - (block_26_q_26_335_0 I R C H S P A D Q B E) - (let ((a!1 (= (uint_array_tuple_array_tuple_accessor_array K) - (store (uint_array_tuple_array_tuple_accessor_array J) - (uint_array_tuple_array_tuple_accessor_length J) - (uint_array_tuple ((as const (Array Int Int)) 0) 0)))) - (a!2 (= (uint_array_tuple_array_tuple_accessor_array L) - (store (uint_array_tuple_array_tuple_accessor_array K) - (+ (- 1) (uint_array_tuple_array_tuple_accessor_length K)) - N)))) - (and a!1 - (= (uint_array_tuple_accessor_array N) - (store (uint_array_tuple_accessor_array M) - (uint_array_tuple_accessor_length M) - 0)) - (= F K) - (= G L) - (= J E) - (= M (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= (uint_array_tuple_array_tuple_accessor_length L) - (uint_array_tuple_array_tuple_accessor_length K)) - (= (uint_array_tuple_array_tuple_accessor_length K) - (+ 1 (uint_array_tuple_array_tuple_accessor_length J))) - (= (uint_array_tuple_accessor_length N) - (+ 1 (uint_array_tuple_accessor_length M))) - (= O 0) - (>= (uint_array_tuple_array_tuple_accessor_length J) 0) - (>= (uint_array_tuple_accessor_length M) 0) - (>= O 0) - (not (<= 115792089237316195423570985008687907853269984665640564039457584007913129639933 - (uint_array_tuple_array_tuple_accessor_length J))) - (not (<= 115792089237316195423570985008687907853269984665640564039457584007913129639933 - (uint_array_tuple_accessor_length M))) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!2)) - ) - (block_27_return_function_q__27_335_0 I R C H S P A D Q B G) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (block_27_return_function_q__27_335_0 G J C F K H A D I B E) - true - ) - (summary_5_function_q__27_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - true - ) - (block_28_function_q__27_335_0 G J C F K H A D I B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) ) - (=> - (and - (block_28_function_q__27_335_0 I P D H Q L A E M B F) - (summary_5_function_q__27_335_0 J P D H Q N B F O C G) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 130)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 178)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 58)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 253)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= N (state_type a!1)) - (= M L) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 4248482434) - (= I 0) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_6_function_q__27_335_0 J P D H Q L A E O C G) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - true - ) - (block_29_function_f__58_335_0 G J C F K H A D N L I B E O M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (block_29_function_f__58_335_0 G J C F K H A D N L I B E O M) - (and (= B A) (= I H) (= G 0) (= O N) (= M L) (= E D)) - ) - (block_30_f_57_335_0 G J C F K H A D N L I B E O M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J uint_array_tuple) (K Int) (L Bool) (M uint_array_tuple) (N Int) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) (T Int) (U Int) (V Int) (W Int) ) - (=> - (and - (block_30_f_57_335_0 G R C F S P A D V T Q B E W U) - (and (= M B) - (= J B) - (= K (uint_array_tuple_accessor_length J)) - (= O U) - (= I W) - (= H 2) - (= N W) - (>= K 0) - (>= O 0) - (>= I 0) - (>= W 0) - (>= U 0) - (>= N 0) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 N)) (>= N (uint_array_tuple_accessor_length M))) - (= L true) - (not (= (<= K I) L))) - ) - (block_32_function_f__58_335_0 H R C F S P A D V T Q B E W U) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (block_32_function_f__58_335_0 G J C F K H A D N L I B E O M) - true - ) - (summary_7_function_f__58_335_0 G J C F K H A D N L I B E O M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (block_33_function_f__58_335_0 G J C F K H A D N L I B E O M) - true - ) - (summary_7_function_f__58_335_0 G J C F K H A D N L I B E O M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (block_31_return_function_f__58_335_0 G J C F K H A D N L I B E O M) - true - ) - (summary_7_function_f__58_335_0 G J C F K H A D N L I B E O M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D uint_array_tuple) (E abi_type) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M uint_array_tuple) (N Int) (O Bool) (P uint_array_tuple) (Q uint_array_tuple) (R uint_array_tuple) (S Int) (T Int) (U Int) (V Int) (W Int) (X uint_array_tuple) (Y uint_array_tuple) (Z Int) (A1 Int) (B1 Bool) (C1 state_type) (D1 state_type) (E1 Int) (F1 tx_type) (G1 Int) (H1 Int) (I1 Int) (J1 Int) ) - (=> - (and - (block_30_f_57_335_0 I E1 E H F1 C1 A F I1 G1 D1 B G J1 H1) - (let ((a!1 (= C - (uint_array_tuple (store (uint_array_tuple_accessor_array Q) S W) - (uint_array_tuple_accessor_length Q))))) - (and (= B1 (= Z A1)) - (= M B) - (= Y D) - a!1 - (= D (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= R C) - (= Q B) - (= P B) - (= X C) - (= J I) - (= W V) - (= L J1) - (= K 3) - (= V H1) - (= S J1) - (= N (uint_array_tuple_accessor_length M)) - (= U (select (uint_array_tuple_accessor_array Q) S)) - (= T (select (uint_array_tuple_accessor_array B) S)) - (= A1 0) - (= Z (uint_array_tuple_accessor_length Y)) - (>= W 0) - (>= L 0) - (>= V 0) - (>= S 0) - (>= N 0) - (>= U 0) - (>= T 0) - (>= J1 0) - (>= H1 0) - (>= Z 0) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= O true) - (not B1) - (not (= (<= N L) O)))) - ) - (block_33_function_f__58_335_0 K E1 E H F1 C1 A F I1 G1 D1 D G J1 H1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D uint_array_tuple) (E abi_type) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M uint_array_tuple) (N Int) (O Bool) (P uint_array_tuple) (Q uint_array_tuple) (R uint_array_tuple) (S Int) (T Int) (U Int) (V Int) (W Int) (X uint_array_tuple) (Y uint_array_tuple) (Z Int) (A1 Int) (B1 Bool) (C1 state_type) (D1 state_type) (E1 Int) (F1 tx_type) (G1 Int) (H1 Int) (I1 Int) (J1 Int) ) - (=> - (and - (block_30_f_57_335_0 I E1 E H F1 C1 A F I1 G1 D1 B G J1 H1) - (let ((a!1 (= C - (uint_array_tuple (store (uint_array_tuple_accessor_array Q) S W) - (uint_array_tuple_accessor_length Q))))) - (and (= B1 (= Z A1)) - (= M B) - (= Y D) - a!1 - (= D (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= R C) - (= Q B) - (= P B) - (= X C) - (= J I) - (= W V) - (= L J1) - (= K J) - (= V H1) - (= S J1) - (= N (uint_array_tuple_accessor_length M)) - (= U (select (uint_array_tuple_accessor_array Q) S)) - (= T (select (uint_array_tuple_accessor_array B) S)) - (= A1 0) - (= Z (uint_array_tuple_accessor_length Y)) - (>= W 0) - (>= L 0) - (>= V 0) - (>= S 0) - (>= N 0) - (>= U 0) - (>= T 0) - (>= J1 0) - (>= H1 0) - (>= Z 0) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= O true) - (not (= (<= N L) O)))) - ) - (block_31_return_function_f__58_335_0 K E1 E H F1 C1 A F I1 G1 D1 D G J1 H1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - true - ) - (block_34_function_f__58_335_0 G J C F K H A D N L I B E O M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) ) - (=> - (and - (block_34_function_f__58_335_0 I P D H Q L A E U R M B F V S) - (summary_7_function_f__58_335_0 J P D H Q N B F V S O C G W T) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 46)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 170)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 209)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 19)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= M L) - (= N (state_type a!1)) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 332507694) - (= S R) - (= I 0) - (= V U) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_8_function_f__58_335_0 J P D H Q L A E U R O C G W T) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_35_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_35_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - (and (= B A) (= I H) (= M L) (= Q P) (= O N) (= G 0) (= E D)) - ) - (block_36_g_101_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J uint_array_tuple_array_tuple) (K Int) (L Bool) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) ) - (=> - (and - (block_36_g_101_335_0 G R C F S P A D V X T Q B E W Y U) - (and (= J E) - (= N E) - (= M Y) - (= K (uint_array_tuple_array_tuple_accessor_length J)) - (= H 5) - (= I W) - (= O W) - (>= M 0) - (>= U 0) - (>= K 0) - (>= I 0) - (>= Y 0) - (>= W 0) - (>= O 0) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 O)) (>= O (uint_array_tuple_array_tuple_accessor_length N))) - (= L true) - (not (= (<= K I) L))) - ) - (block_38_function_g__102_335_0 H R C F S P A D V X T Q B E W Y U) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_38_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_9_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_39_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_9_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_40_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_9_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_41_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_9_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_37_return_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_9_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K uint_array_tuple_array_tuple) (L Int) (M Bool) (N Int) (O uint_array_tuple_array_tuple) (P Int) (Q uint_array_tuple) (R Int) (S Bool) (T uint_array_tuple_array_tuple) (U Int) (V Int) (W state_type) (X state_type) (Y Int) (Z tx_type) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) ) - (=> - (and - (block_36_g_101_335_0 G Y C F Z W A D C1 E1 A1 X B E D1 F1 B1) - (and (not (= (<= R N) S)) - (= T E) - (= O E) - (= K E) - (= Q (select (uint_array_tuple_array_tuple_accessor_array E) P)) - (= L (uint_array_tuple_array_tuple_accessor_length K)) - (= H G) - (= N F1) - (= I 6) - (= R (uint_array_tuple_accessor_length Q)) - (= J D1) - (= U D1) - (= P D1) - (= V B1) - (>= (uint_array_tuple_accessor_length Q) 0) - (>= L 0) - (>= B1 0) - (>= N 0) - (>= R 0) - (>= J 0) - (>= U 0) - (>= P 0) - (>= F1 0) - (>= D1 0) - (>= V 0) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 U)) (>= U (uint_array_tuple_array_tuple_accessor_length T))) - (= M true) - (= S true) - (not (= (<= L J) M))) - ) - (block_39_function_g__102_335_0 I Y C F Z W A D C1 E1 A1 X B E D1 F1 B1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K Int) (L uint_array_tuple_array_tuple) (M Int) (N Bool) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R uint_array_tuple) (S Int) (T Bool) (U uint_array_tuple_array_tuple) (V Int) (W Int) (X uint_array_tuple) (Y Int) (Z state_type) (A1 state_type) (B1 Int) (C1 tx_type) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) ) - (=> - (and - (block_36_g_101_335_0 G B1 C F C1 Z A D F1 H1 D1 A1 B E G1 I1 E1) - (and (not (= (<= S O) T)) - (= P E) - (= L E) - (= U E) - (= X (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= R (select (uint_array_tuple_array_tuple_accessor_array E) Q)) - (= I H) - (= W I1) - (= V G1) - (= O I1) - (= K G1) - (= J 7) - (= Q G1) - (= H G) - (= M (uint_array_tuple_array_tuple_accessor_length L)) - (= S (uint_array_tuple_accessor_length R)) - (= Y E1) - (>= (uint_array_tuple_accessor_length X) 0) - (>= (uint_array_tuple_accessor_length R) 0) - (>= W 0) - (>= V 0) - (>= O 0) - (>= E1 0) - (>= K 0) - (>= Q 0) - (>= M 0) - (>= S 0) - (>= I1 0) - (>= G1 0) - (>= Y 0) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 W)) (>= W (uint_array_tuple_accessor_length X))) - (= T true) - (= N true) - (not (= (<= M K) N))) - ) - (block_40_function_g__102_335_0 J B1 C F C1 Z A D F1 H1 D1 A1 B E G1 I1 E1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O uint_array_tuple_array_tuple) (P Int) (Q Bool) (R Int) (S uint_array_tuple_array_tuple) (T Int) (U uint_array_tuple) (V Int) (W Bool) (X uint_array_tuple_array_tuple) (Y uint_array_tuple_array_tuple) (Z uint_array_tuple_array_tuple) (A1 Int) (B1 Int) (C1 uint_array_tuple) (D1 uint_array_tuple) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 uint_array_tuple_array_tuple) (J1 uint_array_tuple_array_tuple) (K1 Int) (L1 Int) (M1 Bool) (N1 state_type) (O1 state_type) (P1 Int) (Q1 tx_type) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) ) - (=> - (and - (block_36_g_101_335_0 I P1 C H Q1 N1 A D T1 V1 R1 O1 B E U1 W1 S1) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array Y) - A1 - (uint_array_tuple (store (uint_array_tuple_accessor_array C1) - B1 - H1) - (uint_array_tuple_accessor_length C1)))) - (a!2 (uint_array_tuple_array_tuple - ((as const (Array Int uint_array_tuple)) - (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - 0))) - (and (not (= (<= V R) W)) - (= M1 (= K1 L1)) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length Y))) - (= G a!2) - (= O E) - (= X E) - (= Y E) - (= J1 G) - (= S E) - (= Z F) - (= I1 F) - (= U (select (uint_array_tuple_array_tuple_accessor_array E) T)) - (= D1 (select (uint_array_tuple_array_tuple_accessor_array Y) A1)) - (= C1 (select (uint_array_tuple_array_tuple_accessor_array E) A1)) - (= K J) - (= L K) - (= K1 (uint_array_tuple_array_tuple_accessor_length J1)) - (= T U1) - (= P (uint_array_tuple_array_tuple_accessor_length O)) - (= J I) - (= R W1) - (= N U1) - (= M 8) - (= E1 (select (uint_array_tuple_accessor_array C1) B1)) - (= V (uint_array_tuple_accessor_length U)) - (= F1 (select (uint_array_tuple_accessor_array C1) B1)) - (= B1 W1) - (= A1 U1) - (= L1 0) - (= H1 G1) - (= G1 S1) - (>= (uint_array_tuple_accessor_length U) 0) - (>= (uint_array_tuple_accessor_length C1) 0) - (>= K1 0) - (>= T 0) - (>= P 0) - (>= S1 0) - (>= R 0) - (>= N 0) - (>= E1 0) - (>= V 0) - (>= F1 0) - (>= B1 0) - (>= A1 0) - (>= H1 0) - (>= G1 0) - (>= W1 0) - (>= U1 0) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= Q true) - (= W true) - (not M1) - (not (= (<= P N) Q)))) - ) - (block_41_function_g__102_335_0 M P1 C H Q1 N1 A D T1 V1 R1 O1 B G U1 W1 S1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O uint_array_tuple_array_tuple) (P Int) (Q Bool) (R Int) (S uint_array_tuple_array_tuple) (T Int) (U uint_array_tuple) (V Int) (W Bool) (X uint_array_tuple_array_tuple) (Y uint_array_tuple_array_tuple) (Z uint_array_tuple_array_tuple) (A1 Int) (B1 Int) (C1 uint_array_tuple) (D1 uint_array_tuple) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 uint_array_tuple_array_tuple) (J1 uint_array_tuple_array_tuple) (K1 Int) (L1 Int) (M1 Bool) (N1 state_type) (O1 state_type) (P1 Int) (Q1 tx_type) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) ) - (=> - (and - (block_36_g_101_335_0 I P1 C H Q1 N1 A D T1 V1 R1 O1 B E U1 W1 S1) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array Y) - A1 - (uint_array_tuple (store (uint_array_tuple_accessor_array C1) - B1 - H1) - (uint_array_tuple_accessor_length C1)))) - (a!2 (uint_array_tuple_array_tuple - ((as const (Array Int uint_array_tuple)) - (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - 0))) - (and (not (= (<= V R) W)) - (= M1 (= K1 L1)) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length Y))) - (= G a!2) - (= O E) - (= X E) - (= Y E) - (= J1 G) - (= S E) - (= Z F) - (= I1 F) - (= U (select (uint_array_tuple_array_tuple_accessor_array E) T)) - (= D1 (select (uint_array_tuple_array_tuple_accessor_array Y) A1)) - (= C1 (select (uint_array_tuple_array_tuple_accessor_array E) A1)) - (= K J) - (= L K) - (= K1 (uint_array_tuple_array_tuple_accessor_length J1)) - (= T U1) - (= P (uint_array_tuple_array_tuple_accessor_length O)) - (= J I) - (= R W1) - (= N U1) - (= M L) - (= E1 (select (uint_array_tuple_accessor_array C1) B1)) - (= V (uint_array_tuple_accessor_length U)) - (= F1 (select (uint_array_tuple_accessor_array C1) B1)) - (= B1 W1) - (= A1 U1) - (= L1 0) - (= H1 G1) - (= G1 S1) - (>= (uint_array_tuple_accessor_length U) 0) - (>= (uint_array_tuple_accessor_length C1) 0) - (>= K1 0) - (>= T 0) - (>= P 0) - (>= S1 0) - (>= R 0) - (>= N 0) - (>= E1 0) - (>= V 0) - (>= F1 0) - (>= B1 0) - (>= A1 0) - (>= H1 0) - (>= G1 0) - (>= W1 0) - (>= U1 0) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= Q true) - (= W true) - (not (= (<= P N) Q)))) - ) - (block_37_return_function_g__102_335_0 - M - P1 - C - H - Q1 - N1 - A - D - T1 - V1 - R1 - O1 - B - G - U1 - W1 - S1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_42_function_g__102_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) ) - (=> - (and - (block_42_function_g__102_335_0 I P D H Q L A E U X R M B F V Y S) - (summary_9_function_g__102_335_0 J P D H Q N B F V Y S O C G W Z T) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 209)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 87)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 17)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 25)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= N (state_type a!1)) - (= M L) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 420566993) - (= V U) - (= I 0) - (= S R) - (= Y X) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_10_function_g__102_335_0 J P D H Q L A E U X R O C G W Z T) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_43_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_43_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - (and (= B A) (= I H) (= M L) (= Q P) (= O N) (= G 0) (= E D)) - ) - (block_44_h_149_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J uint_array_tuple_array_tuple) (K Int) (L Bool) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) ) - (=> - (and - (block_44_h_149_335_0 G R C F S P A D V X T Q B E W Y U) - (and (= J E) - (= N E) - (= M Y) - (= K (uint_array_tuple_array_tuple_accessor_length J)) - (= H 10) - (= I W) - (= O W) - (>= M 0) - (>= U 0) - (>= K 0) - (>= I 0) - (>= Y 0) - (>= W 0) - (>= O 0) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 O)) (>= O (uint_array_tuple_array_tuple_accessor_length N))) - (= L true) - (not (= (<= K I) L))) - ) - (block_46_function_h__150_335_0 H R C F S P A D V X T Q B E W Y U) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_46_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_11_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_47_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_11_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_48_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_11_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_49_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_11_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_50_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_11_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_51_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_11_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_45_return_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_11_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K uint_array_tuple_array_tuple) (L Int) (M Bool) (N Int) (O uint_array_tuple_array_tuple) (P Int) (Q uint_array_tuple) (R Int) (S Bool) (T uint_array_tuple_array_tuple) (U Int) (V Int) (W state_type) (X state_type) (Y Int) (Z tx_type) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) ) - (=> - (and - (block_44_h_149_335_0 G Y C F Z W A D C1 E1 A1 X B E D1 F1 B1) - (and (not (= (<= R N) S)) - (= T E) - (= O E) - (= K E) - (= Q (select (uint_array_tuple_array_tuple_accessor_array E) P)) - (= L (uint_array_tuple_array_tuple_accessor_length K)) - (= H G) - (= N F1) - (= I 11) - (= R (uint_array_tuple_accessor_length Q)) - (= J D1) - (= U D1) - (= P D1) - (= V B1) - (>= (uint_array_tuple_accessor_length Q) 0) - (>= L 0) - (>= B1 0) - (>= N 0) - (>= R 0) - (>= J 0) - (>= U 0) - (>= P 0) - (>= F1 0) - (>= D1 0) - (>= V 0) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 U)) (>= U (uint_array_tuple_array_tuple_accessor_length T))) - (= M true) - (= S true) - (not (= (<= L J) M))) - ) - (block_47_function_h__150_335_0 I Y C F Z W A D C1 E1 A1 X B E D1 F1 B1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K Int) (L uint_array_tuple_array_tuple) (M Int) (N Bool) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R uint_array_tuple) (S Int) (T Bool) (U uint_array_tuple_array_tuple) (V Int) (W Int) (X uint_array_tuple) (Y Int) (Z state_type) (A1 state_type) (B1 Int) (C1 tx_type) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) ) - (=> - (and - (block_44_h_149_335_0 G B1 C F C1 Z A D F1 H1 D1 A1 B E G1 I1 E1) - (and (not (= (<= S O) T)) - (= P E) - (= L E) - (= U E) - (= X (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= R (select (uint_array_tuple_array_tuple_accessor_array E) Q)) - (= I H) - (= W I1) - (= V G1) - (= O I1) - (= K G1) - (= J 12) - (= Q G1) - (= H G) - (= M (uint_array_tuple_array_tuple_accessor_length L)) - (= S (uint_array_tuple_accessor_length R)) - (= Y E1) - (>= (uint_array_tuple_accessor_length X) 0) - (>= (uint_array_tuple_accessor_length R) 0) - (>= W 0) - (>= V 0) - (>= O 0) - (>= E1 0) - (>= K 0) - (>= Q 0) - (>= M 0) - (>= S 0) - (>= I1 0) - (>= G1 0) - (>= Y 0) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 W)) (>= W (uint_array_tuple_accessor_length X))) - (= T true) - (= N true) - (not (= (<= M K) N))) - ) - (block_48_function_h__150_335_0 J B1 C F C1 Z A D F1 H1 D1 A1 B E G1 I1 E1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G crypto_type) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P Bool) (Q Int) (R uint_array_tuple_array_tuple) (S Int) (T uint_array_tuple) (U Int) (V Bool) (W uint_array_tuple_array_tuple) (X uint_array_tuple_array_tuple) (Y uint_array_tuple_array_tuple) (Z Int) (A1 Int) (B1 uint_array_tuple) (C1 uint_array_tuple) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 uint_array_tuple_array_tuple) (I1 Int) (J1 state_type) (K1 state_type) (L1 Int) (M1 tx_type) (N1 Int) (O1 Int) (P1 Int) (Q1 Int) (R1 Int) (S1 Int) ) - (=> - (and - (block_44_h_149_335_0 H L1 C G M1 J1 A D P1 R1 N1 K1 B E Q1 S1 O1) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array X) - Z - (uint_array_tuple (store (uint_array_tuple_accessor_array B1) - A1 - G1) - (uint_array_tuple_accessor_length B1))))) - (and (not (= (<= U Q) V)) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length X))) - (= N E) - (= R E) - (= Y F) - (= X E) - (= W E) - (= H1 F) - (= B1 (select (uint_array_tuple_array_tuple_accessor_array E) Z)) - (= C1 (select (uint_array_tuple_array_tuple_accessor_array X) Z)) - (= T (select (uint_array_tuple_array_tuple_accessor_array E) S)) - (= S Q1) - (= G1 F1) - (= F1 O1) - (= O (uint_array_tuple_array_tuple_accessor_length N)) - (= K J) - (= M Q1) - (= L 13) - (= U (uint_array_tuple_accessor_length T)) - (= J I) - (= I H) - (= A1 S1) - (= Z Q1) - (= Q S1) - (= E1 (select (uint_array_tuple_accessor_array B1) A1)) - (= D1 (select (uint_array_tuple_accessor_array B1) A1)) - (= I1 Q1) - (>= (uint_array_tuple_accessor_length B1) 0) - (>= (uint_array_tuple_accessor_length T) 0) - (>= S 0) - (>= G1 0) - (>= F1 0) - (>= O 0) - (>= M 0) - (>= O1 0) - (>= U 0) - (>= A1 0) - (>= Z 0) - (>= Q 0) - (>= E1 0) - (>= D1 0) - (>= S1 0) - (>= Q1 0) - (>= I1 0) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 I1)) - (>= I1 (uint_array_tuple_array_tuple_accessor_length H1))) - (= P true) - (= V true) - (not (= (<= O M) P)))) - ) - (block_49_function_h__150_335_0 L L1 C G M1 J1 A D P1 R1 N1 K1 B F Q1 S1 O1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R Bool) (S Int) (T uint_array_tuple_array_tuple) (U Int) (V uint_array_tuple) (W Int) (X Bool) (Y uint_array_tuple_array_tuple) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 Int) (C1 Int) (D1 uint_array_tuple) (E1 uint_array_tuple) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 uint_array_tuple_array_tuple) (K1 uint_array_tuple_array_tuple) (L1 uint_array_tuple_array_tuple) (M1 Int) (N1 uint_array_tuple) (O1 uint_array_tuple) (P1 uint_array_tuple) (Q1 uint_array_tuple_array_tuple) (R1 Int) (S1 state_type) (T1 state_type) (U1 Int) (V1 tx_type) (W1 Int) (X1 Int) (Y1 Int) (Z1 Int) (A2 Int) (B2 Int) ) - (=> - (and - (block_44_h_149_335_0 I U1 C H V1 S1 A D Y1 A2 W1 T1 B E Z1 B2 X1) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array Z) - B1 - (uint_array_tuple (store (uint_array_tuple_accessor_array D1) - C1 - I1) - (uint_array_tuple_accessor_length D1)))) - (a!2 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array K1) M1 O1) - (uint_array_tuple_array_tuple_accessor_length K1))))) - (and (not (= (<= W S) X)) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length Z))) - a!2 - (= P E) - (= T E) - (= A1 F) - (= J1 F) - (= K1 F) - (= Z E) - (= Y E) - (= L1 G) - (= Q1 G) - (= D1 (select (uint_array_tuple_array_tuple_accessor_array E) B1)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array Z) B1)) - (= V (select (uint_array_tuple_array_tuple_accessor_array E) U)) - (= P1 (select (uint_array_tuple_array_tuple_accessor_array K1) M1)) - (= O1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= N1 (select (uint_array_tuple_array_tuple_accessor_array F) M1)) - (= L K) - (= Q (uint_array_tuple_array_tuple_accessor_length P)) - (= B1 Z1) - (= J I) - (= K J) - (= H1 X1) - (= U Z1) - (= M L) - (= O Z1) - (= N 14) - (= C1 B2) - (= W (uint_array_tuple_accessor_length V)) - (= S B2) - (= I1 H1) - (= G1 (select (uint_array_tuple_accessor_array D1) C1)) - (= F1 (select (uint_array_tuple_accessor_array D1) C1)) - (= M1 Z1) - (= R1 Z1) - (>= (uint_array_tuple_accessor_length D1) 0) - (>= (uint_array_tuple_accessor_length V) 0) - (>= (uint_array_tuple_accessor_length N1) 0) - (>= Q 0) - (>= B1 0) - (>= H1 0) - (>= U 0) - (>= O 0) - (>= X1 0) - (>= C1 0) - (>= W 0) - (>= S 0) - (>= I1 0) - (>= G1 0) - (>= F1 0) - (>= M1 0) - (>= B2 0) - (>= Z1 0) - (>= R1 0) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 R1)) - (>= R1 (uint_array_tuple_array_tuple_accessor_length Q1))) - (= R true) - (= X true) - (not (= (<= Q O) R)))) - ) - (block_50_function_h__150_335_0 N U1 C H V1 S1 A D Y1 A2 W1 T1 B G Z1 B2 X1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q uint_array_tuple_array_tuple) (R Int) (S Bool) (T Int) (U uint_array_tuple_array_tuple) (V Int) (W uint_array_tuple) (X Int) (Y Bool) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 uint_array_tuple_array_tuple) (C1 Int) (D1 Int) (E1 uint_array_tuple) (F1 uint_array_tuple) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 uint_array_tuple_array_tuple) (L1 uint_array_tuple_array_tuple) (M1 uint_array_tuple_array_tuple) (N1 Int) (O1 uint_array_tuple) (P1 uint_array_tuple) (Q1 uint_array_tuple) (R1 uint_array_tuple_array_tuple) (S1 Int) (T1 uint_array_tuple) (U1 Int) (V1 Int) (W1 Bool) (X1 state_type) (Y1 state_type) (Z1 Int) (A2 tx_type) (B2 Int) (C2 Int) (D2 Int) (E2 Int) (F2 Int) (G2 Int) ) - (=> - (and - (block_44_h_149_335_0 I Z1 C H A2 X1 A D D2 F2 B2 Y1 B E E2 G2 C2) - (let ((a!1 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array L1) N1 P1) - (uint_array_tuple_array_tuple_accessor_length L1)))) - (a!2 (store (uint_array_tuple_array_tuple_accessor_array A1) - C1 - (uint_array_tuple (store (uint_array_tuple_accessor_array E1) - D1 - J1) - (uint_array_tuple_accessor_length E1))))) - (and (not (= (<= X T) Y)) - (= W1 (= U1 V1)) - (= Z E) - (= A1 E) - (= U E) - (= Q E) - (= B1 F) - (= M1 G) - a!1 - (= F - (uint_array_tuple_array_tuple - a!2 - (uint_array_tuple_array_tuple_accessor_length A1))) - (= L1 F) - (= K1 F) - (= R1 G) - (= W (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array E) C1)) - (= P1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= Q1 (select (uint_array_tuple_array_tuple_accessor_array L1) N1)) - (= F1 (select (uint_array_tuple_array_tuple_accessor_array A1) C1)) - (= O1 (select (uint_array_tuple_array_tuple_accessor_array F) N1)) - (= T1 (select (uint_array_tuple_array_tuple_accessor_array G) S1)) - (= V E2) - (= G1 (select (uint_array_tuple_accessor_array E1) D1)) - (= U1 (uint_array_tuple_accessor_length T1)) - (= D1 G2) - (= C1 E2) - (= O 15) - (= P E2) - (= K J) - (= J I) - (= L K) - (= R (uint_array_tuple_array_tuple_accessor_length Q)) - (= N M) - (= M L) - (= T G2) - (= I1 C2) - (= H1 (select (uint_array_tuple_accessor_array E1) D1)) - (= X (uint_array_tuple_accessor_length W)) - (= N1 E2) - (= J1 I1) - (= S1 E2) - (= V1 0) - (>= (uint_array_tuple_accessor_length W) 0) - (>= (uint_array_tuple_accessor_length E1) 0) - (>= (uint_array_tuple_accessor_length O1) 0) - (>= (uint_array_tuple_accessor_length T1) 0) - (>= V 0) - (>= G1 0) - (>= U1 0) - (>= D1 0) - (>= C1 0) - (>= P 0) - (>= R 0) - (>= T 0) - (>= C2 0) - (>= I1 0) - (>= H1 0) - (>= X 0) - (>= N1 0) - (>= J1 0) - (>= S1 0) - (>= G2 0) - (>= E2 0) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= S true) - (= Y true) - (not W1) - (not (= (<= R P) S)))) - ) - (block_51_function_h__150_335_0 O Z1 C H A2 X1 A D D2 F2 B2 Y1 B G E2 G2 C2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q uint_array_tuple_array_tuple) (R Int) (S Bool) (T Int) (U uint_array_tuple_array_tuple) (V Int) (W uint_array_tuple) (X Int) (Y Bool) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 uint_array_tuple_array_tuple) (C1 Int) (D1 Int) (E1 uint_array_tuple) (F1 uint_array_tuple) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 uint_array_tuple_array_tuple) (L1 uint_array_tuple_array_tuple) (M1 uint_array_tuple_array_tuple) (N1 Int) (O1 uint_array_tuple) (P1 uint_array_tuple) (Q1 uint_array_tuple) (R1 uint_array_tuple_array_tuple) (S1 Int) (T1 uint_array_tuple) (U1 Int) (V1 Int) (W1 Bool) (X1 state_type) (Y1 state_type) (Z1 Int) (A2 tx_type) (B2 Int) (C2 Int) (D2 Int) (E2 Int) (F2 Int) (G2 Int) ) - (=> - (and - (block_44_h_149_335_0 I Z1 C H A2 X1 A D D2 F2 B2 Y1 B E E2 G2 C2) - (let ((a!1 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array L1) N1 P1) - (uint_array_tuple_array_tuple_accessor_length L1)))) - (a!2 (store (uint_array_tuple_array_tuple_accessor_array A1) - C1 - (uint_array_tuple (store (uint_array_tuple_accessor_array E1) - D1 - J1) - (uint_array_tuple_accessor_length E1))))) - (and (not (= (<= X T) Y)) - (= W1 (= U1 V1)) - (= Z E) - (= A1 E) - (= U E) - (= Q E) - (= B1 F) - (= M1 G) - a!1 - (= F - (uint_array_tuple_array_tuple - a!2 - (uint_array_tuple_array_tuple_accessor_length A1))) - (= L1 F) - (= K1 F) - (= R1 G) - (= W (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array E) C1)) - (= P1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= Q1 (select (uint_array_tuple_array_tuple_accessor_array L1) N1)) - (= F1 (select (uint_array_tuple_array_tuple_accessor_array A1) C1)) - (= O1 (select (uint_array_tuple_array_tuple_accessor_array F) N1)) - (= T1 (select (uint_array_tuple_array_tuple_accessor_array G) S1)) - (= V E2) - (= G1 (select (uint_array_tuple_accessor_array E1) D1)) - (= U1 (uint_array_tuple_accessor_length T1)) - (= D1 G2) - (= C1 E2) - (= O N) - (= P E2) - (= K J) - (= J I) - (= L K) - (= R (uint_array_tuple_array_tuple_accessor_length Q)) - (= N M) - (= M L) - (= T G2) - (= I1 C2) - (= H1 (select (uint_array_tuple_accessor_array E1) D1)) - (= X (uint_array_tuple_accessor_length W)) - (= N1 E2) - (= J1 I1) - (= S1 E2) - (= V1 0) - (>= (uint_array_tuple_accessor_length W) 0) - (>= (uint_array_tuple_accessor_length E1) 0) - (>= (uint_array_tuple_accessor_length O1) 0) - (>= (uint_array_tuple_accessor_length T1) 0) - (>= V 0) - (>= G1 0) - (>= U1 0) - (>= D1 0) - (>= C1 0) - (>= P 0) - (>= R 0) - (>= T 0) - (>= C2 0) - (>= I1 0) - (>= H1 0) - (>= X 0) - (>= N1 0) - (>= J1 0) - (>= S1 0) - (>= G2 0) - (>= E2 0) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= S true) - (= Y true) - (not (= (<= R P) S)))) - ) - (block_45_return_function_h__150_335_0 - O - Z1 - C - H - A2 - X1 - A - D - D2 - F2 - B2 - Y1 - B - G - E2 - G2 - C2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_52_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) ) - (=> - (and - (block_52_function_h__150_335_0 I P D H Q L A E U X R M B F V Y S) - (summary_11_function_h__150_335_0 J P D H Q N B F V Y S O C G W Z T) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 47)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 58)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 197)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 122)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= N (state_type a!1)) - (= M L) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 2059745839) - (= V U) - (= I 0) - (= S R) - (= Y X) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_12_function_h__150_335_0 J P D H Q L A E U X R O C G W Z T) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_53_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_53_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - (and (= B A) (= I H) (= M L) (= Q P) (= O N) (= G 0) (= E D)) - ) - (block_54_i_204_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J uint_array_tuple_array_tuple) (K Int) (L Bool) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) ) - (=> - (and - (block_54_i_204_335_0 G R C F S P A D V X T Q B E W Y U) - (and (= J E) - (= N E) - (= M Y) - (= K (uint_array_tuple_array_tuple_accessor_length J)) - (= H 17) - (= I W) - (= O W) - (>= M 0) - (>= U 0) - (>= K 0) - (>= I 0) - (>= Y 0) - (>= W 0) - (>= O 0) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 O)) (>= O (uint_array_tuple_array_tuple_accessor_length N))) - (= L true) - (not (= (<= K I) L))) - ) - (block_56_function_i__205_335_0 H R C F S P A D V X T Q B E W Y U) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_56_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_13_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_57_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_13_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_58_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_13_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_59_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_13_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_60_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_13_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_61_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_13_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_55_return_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - true - ) - (summary_13_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K uint_array_tuple_array_tuple) (L Int) (M Bool) (N Int) (O uint_array_tuple_array_tuple) (P Int) (Q uint_array_tuple) (R Int) (S Bool) (T uint_array_tuple_array_tuple) (U Int) (V Int) (W state_type) (X state_type) (Y Int) (Z tx_type) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) ) - (=> - (and - (block_54_i_204_335_0 G Y C F Z W A D C1 E1 A1 X B E D1 F1 B1) - (and (not (= (<= R N) S)) - (= T E) - (= O E) - (= K E) - (= Q (select (uint_array_tuple_array_tuple_accessor_array E) P)) - (= L (uint_array_tuple_array_tuple_accessor_length K)) - (= H G) - (= N F1) - (= I 18) - (= R (uint_array_tuple_accessor_length Q)) - (= J D1) - (= U D1) - (= P D1) - (= V B1) - (>= (uint_array_tuple_accessor_length Q) 0) - (>= L 0) - (>= B1 0) - (>= N 0) - (>= R 0) - (>= J 0) - (>= U 0) - (>= P 0) - (>= F1 0) - (>= D1 0) - (>= V 0) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 U)) (>= U (uint_array_tuple_array_tuple_accessor_length T))) - (= M true) - (= S true) - (not (= (<= L J) M))) - ) - (block_57_function_i__205_335_0 I Y C F Z W A D C1 E1 A1 X B E D1 F1 B1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K Int) (L uint_array_tuple_array_tuple) (M Int) (N Bool) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R uint_array_tuple) (S Int) (T Bool) (U uint_array_tuple_array_tuple) (V Int) (W Int) (X uint_array_tuple) (Y Int) (Z state_type) (A1 state_type) (B1 Int) (C1 tx_type) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) ) - (=> - (and - (block_54_i_204_335_0 G B1 C F C1 Z A D F1 H1 D1 A1 B E G1 I1 E1) - (and (not (= (<= S O) T)) - (= P E) - (= L E) - (= U E) - (= X (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= R (select (uint_array_tuple_array_tuple_accessor_array E) Q)) - (= I H) - (= W I1) - (= V G1) - (= O I1) - (= K G1) - (= J 19) - (= Q G1) - (= H G) - (= M (uint_array_tuple_array_tuple_accessor_length L)) - (= S (uint_array_tuple_accessor_length R)) - (= Y E1) - (>= (uint_array_tuple_accessor_length X) 0) - (>= (uint_array_tuple_accessor_length R) 0) - (>= W 0) - (>= V 0) - (>= O 0) - (>= E1 0) - (>= K 0) - (>= Q 0) - (>= M 0) - (>= S 0) - (>= I1 0) - (>= G1 0) - (>= Y 0) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 W)) (>= W (uint_array_tuple_accessor_length X))) - (= T true) - (= N true) - (not (= (<= M K) N))) - ) - (block_58_function_i__205_335_0 J B1 C F C1 Z A D F1 H1 D1 A1 B E G1 I1 E1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G crypto_type) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P Bool) (Q Int) (R uint_array_tuple_array_tuple) (S Int) (T uint_array_tuple) (U Int) (V Bool) (W uint_array_tuple_array_tuple) (X uint_array_tuple_array_tuple) (Y uint_array_tuple_array_tuple) (Z Int) (A1 Int) (B1 uint_array_tuple) (C1 uint_array_tuple) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 uint_array_tuple_array_tuple) (J1 Int) (K1 Bool) (L1 uint_array_tuple_array_tuple) (M1 Int) (N1 state_type) (O1 state_type) (P1 Int) (Q1 tx_type) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) ) - (=> - (and - (block_54_i_204_335_0 H P1 C G Q1 N1 A D T1 V1 R1 O1 B E U1 W1 S1) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array X) - Z - (uint_array_tuple (store (uint_array_tuple_accessor_array B1) - A1 - G1) - (uint_array_tuple_accessor_length B1))))) - (and (not (= (<= O M) P)) - (not (= (<= U Q) V)) - (= W E) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length X))) - (= X E) - (= Y F) - (= R E) - (= N E) - (= I1 F) - (= L1 F) - (= T (select (uint_array_tuple_array_tuple_accessor_array E) S)) - (= B1 (select (uint_array_tuple_array_tuple_accessor_array E) Z)) - (= C1 (select (uint_array_tuple_array_tuple_accessor_array X) Z)) - (= K J) - (= L 20) - (= J1 (uint_array_tuple_array_tuple_accessor_length I1)) - (= S U1) - (= O (uint_array_tuple_array_tuple_accessor_length N)) - (= Q W1) - (= J I) - (= I H) - (= M U1) - (= E1 (select (uint_array_tuple_accessor_array B1) A1)) - (= D1 (select (uint_array_tuple_accessor_array B1) A1)) - (= Z U1) - (= U (uint_array_tuple_accessor_length T)) - (= F1 S1) - (= A1 W1) - (= H1 W1) - (= G1 F1) - (= M1 W1) - (>= (uint_array_tuple_accessor_length T) 0) - (>= (uint_array_tuple_accessor_length B1) 0) - (>= J1 0) - (>= S 0) - (>= O 0) - (>= Q 0) - (>= S1 0) - (>= M 0) - (>= E1 0) - (>= D1 0) - (>= Z 0) - (>= U 0) - (>= F1 0) - (>= A1 0) - (>= H1 0) - (>= G1 0) - (>= W1 0) - (>= U1 0) - (>= M1 0) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 M1)) - (>= M1 (uint_array_tuple_array_tuple_accessor_length L1))) - (= P true) - (= V true) - (= K1 true) - (not (= (<= J1 H1) K1)))) - ) - (block_59_function_i__205_335_0 L P1 C G Q1 N1 A D T1 V1 R1 O1 B F U1 W1 S1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R Bool) (S Int) (T uint_array_tuple_array_tuple) (U Int) (V uint_array_tuple) (W Int) (X Bool) (Y uint_array_tuple_array_tuple) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 Int) (C1 Int) (D1 uint_array_tuple) (E1 uint_array_tuple) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 uint_array_tuple_array_tuple) (L1 Int) (M1 Bool) (N1 uint_array_tuple_array_tuple) (O1 uint_array_tuple_array_tuple) (P1 uint_array_tuple_array_tuple) (Q1 Int) (R1 uint_array_tuple) (S1 uint_array_tuple) (T1 uint_array_tuple) (U1 uint_array_tuple_array_tuple) (V1 Int) (W1 state_type) (X1 state_type) (Y1 Int) (Z1 tx_type) (A2 Int) (B2 Int) (C2 Int) (D2 Int) (E2 Int) (F2 Int) ) - (=> - (and - (block_54_i_204_335_0 I Y1 C H Z1 W1 A D C2 E2 A2 X1 B E D2 F2 B2) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array Z) - B1 - (uint_array_tuple (store (uint_array_tuple_accessor_array D1) - C1 - I1) - (uint_array_tuple_accessor_length D1)))) - (a!2 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array O1) Q1 S1) - (uint_array_tuple_array_tuple_accessor_length O1))))) - (and (not (= (<= Q O) R)) - (not (= (<= W S) X)) - (= Y E) - (= Z E) - (= T E) - (= P E) - (= A1 F) - (= N1 F) - (= O1 F) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length Z))) - a!2 - (= K1 F) - (= P1 G) - (= U1 G) - (= V (select (uint_array_tuple_array_tuple_accessor_array E) U)) - (= D1 (select (uint_array_tuple_array_tuple_accessor_array E) B1)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array Z) B1)) - (= T1 (select (uint_array_tuple_array_tuple_accessor_array O1) Q1)) - (= S1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= R1 (select (uint_array_tuple_array_tuple_accessor_array F) Q1)) - (= U D2) - (= F1 (select (uint_array_tuple_accessor_array D1) C1)) - (= C1 F2) - (= B1 D2) - (= N 21) - (= O D2) - (= J I) - (= L1 (uint_array_tuple_array_tuple_accessor_length K1)) - (= K J) - (= Q (uint_array_tuple_array_tuple_accessor_length P)) - (= M L) - (= L K) - (= S F2) - (= H1 B2) - (= G1 (select (uint_array_tuple_accessor_array D1) C1)) - (= W (uint_array_tuple_accessor_length V)) - (= I1 H1) - (= J1 F2) - (= Q1 F2) - (= V1 F2) - (>= (uint_array_tuple_accessor_length V) 0) - (>= (uint_array_tuple_accessor_length D1) 0) - (>= (uint_array_tuple_accessor_length R1) 0) - (>= U 0) - (>= F1 0) - (>= C1 0) - (>= B1 0) - (>= O 0) - (>= L1 0) - (>= Q 0) - (>= S 0) - (>= B2 0) - (>= H1 0) - (>= G1 0) - (>= W 0) - (>= I1 0) - (>= J1 0) - (>= Q1 0) - (>= F2 0) - (>= D2 0) - (>= V1 0) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 V1)) - (>= V1 (uint_array_tuple_array_tuple_accessor_length U1))) - (= R true) - (= X true) - (= M1 true) - (not (= (<= L1 J1) M1)))) - ) - (block_60_function_i__205_335_0 N Y1 C H Z1 W1 A D C2 E2 A2 X1 B G D2 F2 B2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q uint_array_tuple_array_tuple) (R Int) (S Bool) (T Int) (U uint_array_tuple_array_tuple) (V Int) (W uint_array_tuple) (X Int) (Y Bool) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 uint_array_tuple_array_tuple) (C1 Int) (D1 Int) (E1 uint_array_tuple) (F1 uint_array_tuple) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 uint_array_tuple_array_tuple) (M1 Int) (N1 Bool) (O1 uint_array_tuple_array_tuple) (P1 uint_array_tuple_array_tuple) (Q1 uint_array_tuple_array_tuple) (R1 Int) (S1 uint_array_tuple) (T1 uint_array_tuple) (U1 uint_array_tuple) (V1 uint_array_tuple_array_tuple) (W1 Int) (X1 uint_array_tuple) (Y1 Int) (Z1 Int) (A2 Bool) (B2 state_type) (C2 state_type) (D2 Int) (E2 tx_type) (F2 Int) (G2 Int) (H2 Int) (I2 Int) (J2 Int) (K2 Int) ) - (=> - (and - (block_54_i_204_335_0 I D2 C H E2 B2 A D H2 J2 F2 C2 B E I2 K2 G2) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array A1) - C1 - (uint_array_tuple (store (uint_array_tuple_accessor_array E1) - D1 - J1) - (uint_array_tuple_accessor_length E1)))) - (a!2 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array P1) R1 T1) - (uint_array_tuple_array_tuple_accessor_length P1))))) - (and (not (= (<= X T) Y)) - (not (= (<= M1 K1) N1)) - (= A2 (= Y1 Z1)) - (= U E) - (= L1 F) - (= Q1 G) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length A1))) - a!2 - (= Q E) - (= Z E) - (= A1 E) - (= B1 F) - (= P1 F) - (= O1 F) - (= V1 G) - (= F1 (select (uint_array_tuple_array_tuple_accessor_array A1) C1)) - (= T1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= U1 (select (uint_array_tuple_array_tuple_accessor_array P1) R1)) - (= W (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array E) C1)) - (= S1 (select (uint_array_tuple_array_tuple_accessor_array F) R1)) - (= X1 (select (uint_array_tuple_array_tuple_accessor_array G) W1)) - (= K1 K2) - (= Y1 (uint_array_tuple_accessor_length X1)) - (= H1 (select (uint_array_tuple_accessor_array E1) D1)) - (= G1 (select (uint_array_tuple_accessor_array E1) D1)) - (= L K) - (= C1 I2) - (= T K2) - (= M L) - (= J I) - (= O 22) - (= N M) - (= K J) - (= D1 K2) - (= P I2) - (= V I2) - (= R (uint_array_tuple_array_tuple_accessor_length Q)) - (= X (uint_array_tuple_accessor_length W)) - (= M1 (uint_array_tuple_array_tuple_accessor_length L1)) - (= R1 K2) - (= J1 I1) - (= I1 G2) - (= W1 K2) - (= Z1 0) - (>= (uint_array_tuple_accessor_length W) 0) - (>= (uint_array_tuple_accessor_length E1) 0) - (>= (uint_array_tuple_accessor_length S1) 0) - (>= (uint_array_tuple_accessor_length X1) 0) - (>= K1 0) - (>= Y1 0) - (>= H1 0) - (>= G1 0) - (>= C1 0) - (>= T 0) - (>= D1 0) - (>= P 0) - (>= V 0) - (>= R 0) - (>= X 0) - (>= G2 0) - (>= M1 0) - (>= R1 0) - (>= J1 0) - (>= I1 0) - (>= W1 0) - (>= K2 0) - (>= I2 0) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= S true) - (= Y true) - (= N1 true) - (not A2) - (not (= (<= R P) S)))) - ) - (block_61_function_i__205_335_0 O D2 C H E2 B2 A D H2 J2 F2 C2 B G I2 K2 G2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q uint_array_tuple_array_tuple) (R Int) (S Bool) (T Int) (U uint_array_tuple_array_tuple) (V Int) (W uint_array_tuple) (X Int) (Y Bool) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 uint_array_tuple_array_tuple) (C1 Int) (D1 Int) (E1 uint_array_tuple) (F1 uint_array_tuple) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 uint_array_tuple_array_tuple) (M1 Int) (N1 Bool) (O1 uint_array_tuple_array_tuple) (P1 uint_array_tuple_array_tuple) (Q1 uint_array_tuple_array_tuple) (R1 Int) (S1 uint_array_tuple) (T1 uint_array_tuple) (U1 uint_array_tuple) (V1 uint_array_tuple_array_tuple) (W1 Int) (X1 uint_array_tuple) (Y1 Int) (Z1 Int) (A2 Bool) (B2 state_type) (C2 state_type) (D2 Int) (E2 tx_type) (F2 Int) (G2 Int) (H2 Int) (I2 Int) (J2 Int) (K2 Int) ) - (=> - (and - (block_54_i_204_335_0 I D2 C H E2 B2 A D H2 J2 F2 C2 B E I2 K2 G2) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array A1) - C1 - (uint_array_tuple (store (uint_array_tuple_accessor_array E1) - D1 - J1) - (uint_array_tuple_accessor_length E1)))) - (a!2 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array P1) R1 T1) - (uint_array_tuple_array_tuple_accessor_length P1))))) - (and (not (= (<= X T) Y)) - (not (= (<= M1 K1) N1)) - (= A2 (= Y1 Z1)) - (= U E) - (= L1 F) - (= Q1 G) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length A1))) - a!2 - (= Q E) - (= Z E) - (= A1 E) - (= B1 F) - (= P1 F) - (= O1 F) - (= V1 G) - (= F1 (select (uint_array_tuple_array_tuple_accessor_array A1) C1)) - (= T1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= U1 (select (uint_array_tuple_array_tuple_accessor_array P1) R1)) - (= W (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array E) C1)) - (= S1 (select (uint_array_tuple_array_tuple_accessor_array F) R1)) - (= X1 (select (uint_array_tuple_array_tuple_accessor_array G) W1)) - (= K1 K2) - (= Y1 (uint_array_tuple_accessor_length X1)) - (= H1 (select (uint_array_tuple_accessor_array E1) D1)) - (= G1 (select (uint_array_tuple_accessor_array E1) D1)) - (= L K) - (= C1 I2) - (= T K2) - (= M L) - (= J I) - (= O N) - (= N M) - (= K J) - (= D1 K2) - (= P I2) - (= V I2) - (= R (uint_array_tuple_array_tuple_accessor_length Q)) - (= X (uint_array_tuple_accessor_length W)) - (= M1 (uint_array_tuple_array_tuple_accessor_length L1)) - (= R1 K2) - (= J1 I1) - (= I1 G2) - (= W1 K2) - (= Z1 0) - (>= (uint_array_tuple_accessor_length W) 0) - (>= (uint_array_tuple_accessor_length E1) 0) - (>= (uint_array_tuple_accessor_length S1) 0) - (>= (uint_array_tuple_accessor_length X1) 0) - (>= K1 0) - (>= Y1 0) - (>= H1 0) - (>= G1 0) - (>= C1 0) - (>= T 0) - (>= D1 0) - (>= P 0) - (>= V 0) - (>= R 0) - (>= X 0) - (>= G2 0) - (>= M1 0) - (>= R1 0) - (>= J1 0) - (>= I1 0) - (>= W1 0) - (>= K2 0) - (>= I2 0) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= S true) - (= Y true) - (= N1 true) - (not (= (<= R P) S)))) - ) - (block_55_return_function_i__205_335_0 - O - D2 - C - H - E2 - B2 - A - D - H2 - J2 - F2 - C2 - B - G - I2 - K2 - G2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_62_function_i__205_335_0 G J C F K H A D N P L I B E O Q M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) ) - (=> - (and - (block_62_function_i__205_335_0 I P D H Q L A E U X R M B F V Y S) - (summary_13_function_i__205_335_0 J P D H Q N B F V Y S O C G W Z T) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 27)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 241)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 63)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 53)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= N (state_type a!1)) - (= M L) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 893382939) - (= V U) - (= I 0) - (= S R) - (= Y X) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_14_function_i__205_335_0 J P D H Q L A E U X R O C G W Z T) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - true - ) - (block_63_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_63_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - (and (= B A) (= I H) (= G 0) (= O N) (= S R) (= Q P) (= M L) (= E D)) - ) - (block_64_j_278_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J uint_array_tuple_array_tuple) (K Int) (L Bool) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Int) ) - (=> - (and - (block_64_j_278_335_0 G R C F S P A D V X Z T Q B E W Y A1 U) - (and (= N E) - (= J E) - (= O W) - (= I W) - (= H 24) - (= M Y) - (= K (uint_array_tuple_array_tuple_accessor_length J)) - (>= O 0) - (>= W 0) - (>= I 0) - (>= M 0) - (>= K 0) - (>= A1 0) - (>= Y 0) - (>= U 0) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 O)) (>= O (uint_array_tuple_array_tuple_accessor_length N))) - (= L true) - (not (= (<= K I) L))) - ) - (block_66_function_j__279_335_0 H R C F S P A D V X Z T Q B E W Y A1 U) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_66_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_67_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_68_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_69_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_70_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_71_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_72_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_73_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - (block_65_return_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - true - ) - (summary_15_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K uint_array_tuple_array_tuple) (L Int) (M Bool) (N Int) (O uint_array_tuple_array_tuple) (P Int) (Q uint_array_tuple) (R Int) (S Bool) (T uint_array_tuple_array_tuple) (U Int) (V Int) (W state_type) (X state_type) (Y Int) (Z tx_type) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) ) - (=> - (and - (block_64_j_278_335_0 G Y C F Z W A D C1 E1 G1 A1 X B E D1 F1 H1 B1) - (and (not (= (<= R N) S)) - (= O E) - (= K E) - (= T E) - (= Q (select (uint_array_tuple_array_tuple_accessor_array E) P)) - (= H G) - (= V B1) - (= U D1) - (= N F1) - (= J D1) - (= I 25) - (= P D1) - (= L (uint_array_tuple_array_tuple_accessor_length K)) - (= R (uint_array_tuple_accessor_length Q)) - (>= (uint_array_tuple_accessor_length Q) 0) - (>= V 0) - (>= U 0) - (>= N 0) - (>= D1 0) - (>= J 0) - (>= P 0) - (>= L 0) - (>= R 0) - (>= H1 0) - (>= F1 0) - (>= B1 0) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 U)) (>= U (uint_array_tuple_array_tuple_accessor_length T))) - (= S true) - (= M true) - (not (= (<= L J) M))) - ) - (block_67_function_j__279_335_0 I Y C F Z W A D C1 E1 G1 A1 X B E D1 F1 H1 B1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K Int) (L uint_array_tuple_array_tuple) (M Int) (N Bool) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R uint_array_tuple) (S Int) (T Bool) (U uint_array_tuple_array_tuple) (V Int) (W Int) (X uint_array_tuple) (Y Int) (Z state_type) (A1 state_type) (B1 Int) (C1 tx_type) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) ) - (=> - (and - (block_64_j_278_335_0 G B1 C F C1 Z A D F1 H1 J1 D1 A1 B E G1 I1 K1 E1) - (and (not (= (<= S O) T)) - (= L E) - (= P E) - (= U E) - (= R (select (uint_array_tuple_array_tuple_accessor_array E) Q)) - (= X (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= K G1) - (= Y E1) - (= H G) - (= Q G1) - (= M (uint_array_tuple_array_tuple_accessor_length L)) - (= S (uint_array_tuple_accessor_length R)) - (= J 26) - (= I H) - (= W I1) - (= O I1) - (= V G1) - (>= (uint_array_tuple_accessor_length R) 0) - (>= (uint_array_tuple_accessor_length X) 0) - (>= K 0) - (>= Y 0) - (>= Q 0) - (>= G1 0) - (>= M 0) - (>= S 0) - (>= W 0) - (>= O 0) - (>= V 0) - (>= K1 0) - (>= I1 0) - (>= E1 0) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 W)) (>= W (uint_array_tuple_accessor_length X))) - (= T true) - (= N true) - (not (= (<= M K) N))) - ) - (block_68_function_j__279_335_0 - J - B1 - C - F - C1 - Z - A - D - F1 - H1 - J1 - D1 - A1 - B - E - G1 - I1 - K1 - E1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G crypto_type) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P Bool) (Q Int) (R uint_array_tuple_array_tuple) (S Int) (T uint_array_tuple) (U Int) (V Bool) (W uint_array_tuple_array_tuple) (X uint_array_tuple_array_tuple) (Y uint_array_tuple_array_tuple) (Z Int) (A1 Int) (B1 uint_array_tuple) (C1 uint_array_tuple) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 uint_array_tuple_array_tuple) (J1 Int) (K1 Bool) (L1 uint_array_tuple_array_tuple) (M1 Int) (N1 state_type) (O1 state_type) (P1 Int) (Q1 tx_type) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) (X1 Int) (Y1 Int) ) - (=> - (and - (block_64_j_278_335_0 H P1 C G Q1 N1 A D T1 V1 X1 R1 O1 B E U1 W1 Y1 S1) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array X) - Z - (uint_array_tuple (store (uint_array_tuple_accessor_array B1) - A1 - G1) - (uint_array_tuple_accessor_length B1))))) - (and (not (= (<= O M) P)) - (not (= (<= J1 H1) K1)) - (= Y F) - (= R E) - (= X E) - (= L1 F) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length X))) - (= N E) - (= W E) - (= I1 F) - (= T (select (uint_array_tuple_array_tuple_accessor_array E) S)) - (= B1 (select (uint_array_tuple_array_tuple_accessor_array E) Z)) - (= C1 (select (uint_array_tuple_array_tuple_accessor_array X) Z)) - (= I H) - (= M U1) - (= M1 Y1) - (= U (uint_array_tuple_accessor_length T)) - (= Q W1) - (= E1 (select (uint_array_tuple_accessor_array B1) A1)) - (= S U1) - (= J I) - (= L 27) - (= K J) - (= A1 W1) - (= Z U1) - (= O (uint_array_tuple_array_tuple_accessor_length N)) - (= G1 F1) - (= F1 S1) - (= H1 Y1) - (= D1 (select (uint_array_tuple_accessor_array B1) A1)) - (= J1 (uint_array_tuple_array_tuple_accessor_length I1)) - (>= (uint_array_tuple_accessor_length T) 0) - (>= (uint_array_tuple_accessor_length B1) 0) - (>= M 0) - (>= M1 0) - (>= U 0) - (>= Q 0) - (>= E1 0) - (>= S 0) - (>= U1 0) - (>= A1 0) - (>= Z 0) - (>= O 0) - (>= G1 0) - (>= F1 0) - (>= H1 0) - (>= D1 0) - (>= J1 0) - (>= Y1 0) - (>= W1 0) - (>= S1 0) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 M1)) - (>= M1 (uint_array_tuple_array_tuple_accessor_length L1))) - (= P true) - (= K1 true) - (= V true) - (not (= (<= U Q) V)))) - ) - (block_69_function_j__279_335_0 - L - P1 - C - G - Q1 - N1 - A - D - T1 - V1 - X1 - R1 - O1 - B - F - U1 - W1 - Y1 - S1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R Bool) (S Int) (T uint_array_tuple_array_tuple) (U Int) (V uint_array_tuple) (W Int) (X Bool) (Y uint_array_tuple_array_tuple) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 Int) (C1 Int) (D1 uint_array_tuple) (E1 uint_array_tuple) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 uint_array_tuple_array_tuple) (L1 Int) (M1 Bool) (N1 uint_array_tuple_array_tuple) (O1 uint_array_tuple_array_tuple) (P1 uint_array_tuple_array_tuple) (Q1 Int) (R1 uint_array_tuple) (S1 uint_array_tuple) (T1 uint_array_tuple) (U1 Int) (V1 uint_array_tuple_array_tuple) (W1 Int) (X1 Bool) (Y1 Int) (Z1 uint_array_tuple_array_tuple) (A2 Int) (B2 state_type) (C2 state_type) (D2 Int) (E2 tx_type) (F2 Int) (G2 Int) (H2 Int) (I2 Int) (J2 Int) (K2 Int) (L2 Int) (M2 Int) ) - (=> - (and - (block_64_j_278_335_0 I D2 C H E2 B2 A D H2 J2 L2 F2 C2 B E I2 K2 M2 G2) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array Z) - B1 - (uint_array_tuple (store (uint_array_tuple_accessor_array D1) - C1 - I1) - (uint_array_tuple_accessor_length D1)))) - (a!2 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array O1) Q1 S1) - (uint_array_tuple_array_tuple_accessor_length O1))))) - (and (not (= (<= Q O) R)) - (not (= (<= L1 J1) M1)) - (not (= (<= W1 U1) X1)) - (= A1 F) - (= Y E) - (= Z E) - (= N1 F) - (= O1 F) - (= Z1 G) - (= V1 G) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length Z))) - a!2 - (= P E) - (= T E) - (= K1 F) - (= P1 G) - (= V (select (uint_array_tuple_array_tuple_accessor_array E) U)) - (= D1 (select (uint_array_tuple_array_tuple_accessor_array E) B1)) - (= R1 (select (uint_array_tuple_array_tuple_accessor_array F) Q1)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array Z) B1)) - (= T1 (select (uint_array_tuple_array_tuple_accessor_array O1) Q1)) - (= S1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= W (uint_array_tuple_accessor_length V)) - (= B1 I2) - (= A2 I2) - (= J1 M2) - (= I1 H1) - (= U I2) - (= N 28) - (= O I2) - (= L K) - (= J I) - (= Q (uint_array_tuple_array_tuple_accessor_length P)) - (= M L) - (= G1 (select (uint_array_tuple_accessor_array D1) C1)) - (= F1 (select (uint_array_tuple_accessor_array D1) C1)) - (= K J) - (= S K2) - (= H1 G2) - (= C1 K2) - (= U1 K2) - (= L1 (uint_array_tuple_array_tuple_accessor_length K1)) - (= Y1 I2) - (= Q1 M2) - (= W1 (uint_array_tuple_array_tuple_accessor_length V1)) - (>= (uint_array_tuple_accessor_length V) 0) - (>= (uint_array_tuple_accessor_length D1) 0) - (>= (uint_array_tuple_accessor_length R1) 0) - (>= W 0) - (>= B1 0) - (>= A2 0) - (>= J1 0) - (>= I1 0) - (>= U 0) - (>= O 0) - (>= Q 0) - (>= G1 0) - (>= F1 0) - (>= S 0) - (>= I2 0) - (>= H1 0) - (>= C1 0) - (>= U1 0) - (>= L1 0) - (>= Y1 0) - (>= Q1 0) - (>= W1 0) - (>= M2 0) - (>= K2 0) - (>= G2 0) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 A2)) - (>= A2 (uint_array_tuple_array_tuple_accessor_length Z1))) - (= R true) - (= X true) - (= M1 true) - (= X1 true) - (not (= (<= W S) X)))) - ) - (block_70_function_j__279_335_0 - N - D2 - C - H - E2 - B2 - A - D - H2 - J2 - L2 - F2 - C2 - B - G - I2 - K2 - M2 - G2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q uint_array_tuple_array_tuple) (R Int) (S Bool) (T Int) (U uint_array_tuple_array_tuple) (V Int) (W uint_array_tuple) (X Int) (Y Bool) (Z uint_array_tuple_array_tuple) (A1 uint_array_tuple_array_tuple) (B1 uint_array_tuple_array_tuple) (C1 Int) (D1 Int) (E1 uint_array_tuple) (F1 uint_array_tuple) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 uint_array_tuple_array_tuple) (M1 Int) (N1 Bool) (O1 uint_array_tuple_array_tuple) (P1 uint_array_tuple_array_tuple) (Q1 uint_array_tuple_array_tuple) (R1 Int) (S1 uint_array_tuple) (T1 uint_array_tuple) (U1 uint_array_tuple) (V1 Int) (W1 uint_array_tuple_array_tuple) (X1 Int) (Y1 Bool) (Z1 Int) (A2 uint_array_tuple_array_tuple) (B2 Int) (C2 uint_array_tuple) (D2 Int) (E2 Bool) (F2 uint_array_tuple_array_tuple) (G2 Int) (H2 state_type) (I2 state_type) (J2 Int) (K2 tx_type) (L2 Int) (M2 Int) (N2 Int) (O2 Int) (P2 Int) (Q2 Int) (R2 Int) (S2 Int) ) - (=> - (and - (block_64_j_278_335_0 I J2 C H K2 H2 A D N2 P2 R2 L2 I2 B E O2 Q2 S2 M2) - (let ((a!1 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array P1) R1 T1) - (uint_array_tuple_array_tuple_accessor_length P1)))) - (a!2 (store (uint_array_tuple_array_tuple_accessor_array A1) - C1 - (uint_array_tuple (store (uint_array_tuple_accessor_array E1) - D1 - J1) - (uint_array_tuple_accessor_length E1))))) - (and (not (= (<= M1 K1) N1)) - (not (= (<= X T) Y)) - (not (= (<= X1 V1) Y1)) - (not (= (<= D2 Z1) E2)) - a!1 - (= L1 F) - (= B1 F) - (= F2 G) - (= A2 G) - (= Q E) - (= F - (uint_array_tuple_array_tuple - a!2 - (uint_array_tuple_array_tuple_accessor_length A1))) - (= U E) - (= Z E) - (= A1 E) - (= Q1 G) - (= P1 F) - (= O1 F) - (= W1 G) - (= U1 (select (uint_array_tuple_array_tuple_accessor_array P1) R1)) - (= C2 (select (uint_array_tuple_array_tuple_accessor_array G) B2)) - (= W (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= E1 (select (uint_array_tuple_array_tuple_accessor_array E) C1)) - (= F1 (select (uint_array_tuple_array_tuple_accessor_array A1) C1)) - (= T1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= S1 (select (uint_array_tuple_array_tuple_accessor_array F) R1)) - (= C1 O2) - (= G1 (select (uint_array_tuple_accessor_array E1) D1)) - (= H1 (select (uint_array_tuple_accessor_array E1) D1)) - (= G2 Q2) - (= J I) - (= K J) - (= T Q2) - (= K1 S2) - (= R (uint_array_tuple_array_tuple_accessor_length Q)) - (= P O2) - (= O 29) - (= V O2) - (= M1 (uint_array_tuple_array_tuple_accessor_length L1)) - (= X (uint_array_tuple_accessor_length W)) - (= L K) - (= M L) - (= N M) - (= D1 Q2) - (= J1 I1) - (= I1 M2) - (= Z1 O2) - (= V1 Q2) - (= R1 S2) - (= B2 O2) - (= X1 (uint_array_tuple_array_tuple_accessor_length W1)) - (= D2 (uint_array_tuple_accessor_length C2)) - (>= (uint_array_tuple_accessor_length C2) 0) - (>= (uint_array_tuple_accessor_length W) 0) - (>= (uint_array_tuple_accessor_length E1) 0) - (>= (uint_array_tuple_accessor_length S1) 0) - (>= C1 0) - (>= G1 0) - (>= H1 0) - (>= G2 0) - (>= T 0) - (>= K1 0) - (>= R 0) - (>= P 0) - (>= V 0) - (>= M1 0) - (>= X 0) - (>= D1 0) - (>= O2 0) - (>= J1 0) - (>= I1 0) - (>= Z1 0) - (>= V1 0) - (>= R1 0) - (>= B2 0) - (>= X1 0) - (>= D2 0) - (>= S2 0) - (>= Q2 0) - (>= M2 0) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 G2)) - (>= G2 (uint_array_tuple_array_tuple_accessor_length F2))) - (= S true) - (= Y true) - (= N1 true) - (= Y1 true) - (= E2 true) - (not (= (<= R P) S)))) - ) - (block_71_function_j__279_335_0 - O - J2 - C - H - K2 - H2 - A - D - N2 - P2 - R2 - L2 - I2 - B - G - O2 - Q2 - S2 - M2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R uint_array_tuple_array_tuple) (S Int) (T Bool) (U Int) (V uint_array_tuple_array_tuple) (W Int) (X uint_array_tuple) (Y Int) (Z Bool) (A1 uint_array_tuple_array_tuple) (B1 uint_array_tuple_array_tuple) (C1 uint_array_tuple_array_tuple) (D1 Int) (E1 Int) (F1 uint_array_tuple) (G1 uint_array_tuple) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 Int) (M1 uint_array_tuple_array_tuple) (N1 Int) (O1 Bool) (P1 uint_array_tuple_array_tuple) (Q1 uint_array_tuple_array_tuple) (R1 uint_array_tuple_array_tuple) (S1 Int) (T1 uint_array_tuple) (U1 uint_array_tuple) (V1 uint_array_tuple) (W1 Int) (X1 uint_array_tuple_array_tuple) (Y1 Int) (Z1 Bool) (A2 Int) (B2 uint_array_tuple_array_tuple) (C2 Int) (D2 uint_array_tuple) (E2 Int) (F2 Bool) (G2 uint_array_tuple_array_tuple) (H2 Int) (I2 uint_array_tuple) (J2 Int) (K2 state_type) (L2 state_type) (M2 Int) (N2 tx_type) (O2 Int) (P2 Int) (Q2 Int) (R2 Int) (S2 Int) (T2 Int) (U2 Int) (V2 Int) ) - (=> - (and - (block_64_j_278_335_0 I M2 C H N2 K2 A D Q2 S2 U2 O2 L2 B E R2 T2 V2 P2) - (let ((a!1 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array Q1) S1 U1) - (uint_array_tuple_array_tuple_accessor_length Q1)))) - (a!2 (store (uint_array_tuple_array_tuple_accessor_array B1) - D1 - (uint_array_tuple (store (uint_array_tuple_accessor_array F1) - E1 - K1) - (uint_array_tuple_accessor_length F1))))) - (and (not (= (<= S Q) T)) - (not (= (<= Y U) Z)) - (not (= (<= Y1 W1) Z1)) - (not (= (<= E2 A2) F2)) - (= P1 F) - (= A1 E) - (= X1 G) - (= Q1 F) - (= B2 G) - a!1 - (= V E) - (= R E) - (= F - (uint_array_tuple_array_tuple - a!2 - (uint_array_tuple_array_tuple_accessor_length B1))) - (= B1 E) - (= C1 F) - (= M1 F) - (= R1 G) - (= G2 G) - (= F1 (select (uint_array_tuple_array_tuple_accessor_array E) D1)) - (= T1 (select (uint_array_tuple_array_tuple_accessor_array F) S1)) - (= X (select (uint_array_tuple_array_tuple_accessor_array E) W)) - (= G1 (select (uint_array_tuple_array_tuple_accessor_array B1) D1)) - (= U1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= V1 (select (uint_array_tuple_array_tuple_accessor_array Q1) S1)) - (= D2 (select (uint_array_tuple_array_tuple_accessor_array G) C2)) - (= I2 (select (uint_array_tuple_array_tuple_accessor_array G) H2)) - (= J1 P2) - (= K1 J1) - (= J2 R2) - (= S1 V2) - (= D1 R2) - (= M L) - (= K J) - (= N M) - (= W R2) - (= N1 (uint_array_tuple_array_tuple_accessor_length M1)) - (= E1 T2) - (= U T2) - (= S (uint_array_tuple_array_tuple_accessor_length R)) - (= L K) - (= J I) - (= Y (uint_array_tuple_accessor_length X)) - (= O N) - (= P 30) - (= Q R2) - (= I1 (select (uint_array_tuple_accessor_array F1) E1)) - (= H1 (select (uint_array_tuple_accessor_array F1) E1)) - (= W1 T2) - (= L1 V2) - (= C2 R2) - (= Y1 (uint_array_tuple_array_tuple_accessor_length X1)) - (= H2 T2) - (= E2 (uint_array_tuple_accessor_length D2)) - (= A2 R2) - (>= (uint_array_tuple_accessor_length F1) 0) - (>= (uint_array_tuple_accessor_length T1) 0) - (>= (uint_array_tuple_accessor_length X) 0) - (>= (uint_array_tuple_accessor_length D2) 0) - (>= (uint_array_tuple_accessor_length I2) 0) - (>= J1 0) - (>= K1 0) - (>= J2 0) - (>= S1 0) - (>= D1 0) - (>= W 0) - (>= N1 0) - (>= E1 0) - (>= U 0) - (>= S 0) - (>= Y 0) - (>= Q 0) - (>= I1 0) - (>= H1 0) - (>= R2 0) - (>= W1 0) - (>= L1 0) - (>= C2 0) - (>= Y1 0) - (>= H2 0) - (>= E2 0) - (>= A2 0) - (>= V2 0) - (>= T2 0) - (>= P2 0) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= H2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 J2)) (>= J2 (uint_array_tuple_accessor_length I2))) - (= Z1 true) - (= F2 true) - (= O1 true) - (= T true) - (= Z true) - (not (= (<= N1 L1) O1)))) - ) - (block_72_function_j__279_335_0 - P - M2 - C - H - N2 - K2 - A - D - Q2 - S2 - U2 - O2 - L2 - B - G - R2 - T2 - V2 - P2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S uint_array_tuple_array_tuple) (T Int) (U Bool) (V Int) (W uint_array_tuple_array_tuple) (X Int) (Y uint_array_tuple) (Z Int) (A1 Bool) (B1 uint_array_tuple_array_tuple) (C1 uint_array_tuple_array_tuple) (D1 uint_array_tuple_array_tuple) (E1 Int) (F1 Int) (G1 uint_array_tuple) (H1 uint_array_tuple) (I1 Int) (J1 Int) (K1 Int) (L1 Int) (M1 Int) (N1 uint_array_tuple_array_tuple) (O1 Int) (P1 Bool) (Q1 uint_array_tuple_array_tuple) (R1 uint_array_tuple_array_tuple) (S1 uint_array_tuple_array_tuple) (T1 Int) (U1 uint_array_tuple) (V1 uint_array_tuple) (W1 uint_array_tuple) (X1 Int) (Y1 uint_array_tuple_array_tuple) (Z1 Int) (A2 Bool) (B2 Int) (C2 uint_array_tuple_array_tuple) (D2 Int) (E2 uint_array_tuple) (F2 Int) (G2 Bool) (H2 uint_array_tuple_array_tuple) (I2 Int) (J2 uint_array_tuple) (K2 Int) (L2 Int) (M2 Int) (N2 Bool) (O2 state_type) (P2 state_type) (Q2 Int) (R2 tx_type) (S2 Int) (T2 Int) (U2 Int) (V2 Int) (W2 Int) (X2 Int) (Y2 Int) (Z2 Int) ) - (=> - (and - (block_64_j_278_335_0 I Q2 C H R2 O2 A D U2 W2 Y2 S2 P2 B E V2 X2 Z2 T2) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array C1) - E1 - (uint_array_tuple (store (uint_array_tuple_accessor_array G1) - F1 - L1) - (uint_array_tuple_accessor_length G1)))) - (a!2 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array R1) T1 V1) - (uint_array_tuple_array_tuple_accessor_length R1))))) - (and (not (= (<= Z1 X1) A2)) - (not (= (<= Z V) A1)) - (not (= (<= F2 B2) G2)) - (not (= (<= T R) U)) - (= N2 (= L2 M2)) - (= S1 G) - (= D1 F) - (= N1 F) - (= R1 F) - (= Y1 G) - (= H2 G) - (= W E) - (= S E) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length C1))) - a!2 - (= B1 E) - (= C1 E) - (= Q1 F) - (= C2 G) - (= G1 (select (uint_array_tuple_array_tuple_accessor_array E) E1)) - (= W1 (select (uint_array_tuple_array_tuple_accessor_array R1) T1)) - (= H1 (select (uint_array_tuple_array_tuple_accessor_array C1) E1)) - (= U1 (select (uint_array_tuple_array_tuple_accessor_array F) T1)) - (= V1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= E2 (select (uint_array_tuple_array_tuple_accessor_array G) D2)) - (= J2 (select (uint_array_tuple_array_tuple_accessor_array G) I2)) - (= Y (select (uint_array_tuple_array_tuple_accessor_array E) X)) - (= J1 (select (uint_array_tuple_accessor_array G1) F1)) - (= O1 (uint_array_tuple_array_tuple_accessor_length N1)) - (= J I) - (= Z1 (uint_array_tuple_array_tuple_accessor_length Y1)) - (= M2 0) - (= Q 31) - (= O N) - (= M L) - (= R V2) - (= I1 (select (uint_array_tuple_accessor_array G1) F1)) - (= V X2) - (= P O) - (= N M) - (= Z (uint_array_tuple_accessor_length Y)) - (= F2 (uint_array_tuple_accessor_length E2)) - (= T1 Z2) - (= K J) - (= E1 V2) - (= T (uint_array_tuple_array_tuple_accessor_length S)) - (= X V2) - (= L K) - (= K1 T2) - (= F1 X2) - (= M1 Z2) - (= L1 K1) - (= B2 V2) - (= X1 X2) - (= L2 (select (uint_array_tuple_accessor_array J2) K2)) - (= I2 X2) - (= D2 V2) - (= K2 V2) - (>= (uint_array_tuple_accessor_length G1) 0) - (>= (uint_array_tuple_accessor_length U1) 0) - (>= (uint_array_tuple_accessor_length E2) 0) - (>= (uint_array_tuple_accessor_length J2) 0) - (>= (uint_array_tuple_accessor_length Y) 0) - (>= J1 0) - (>= O1 0) - (>= Z1 0) - (>= R 0) - (>= I1 0) - (>= V 0) - (>= Z 0) - (>= F2 0) - (>= T1 0) - (>= E1 0) - (>= T 0) - (>= X 0) - (>= K1 0) - (>= F1 0) - (>= M1 0) - (>= L1 0) - (>= V2 0) - (>= B2 0) - (>= X1 0) - (>= L2 0) - (>= I2 0) - (>= D2 0) - (>= K2 0) - (>= Z2 0) - (>= X2 0) - (>= T2 0) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= A2 true) - (not N2) - (= P1 true) - (= G2 true) - (= U true) - (= A1 true) - (not (= (<= O1 M1) P1)))) - ) - (block_73_function_j__279_335_0 - Q - Q2 - C - H - R2 - O2 - A - D - U2 - W2 - Y2 - S2 - P2 - B - G - V2 - X2 - Z2 - T2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S uint_array_tuple_array_tuple) (T Int) (U Bool) (V Int) (W uint_array_tuple_array_tuple) (X Int) (Y uint_array_tuple) (Z Int) (A1 Bool) (B1 uint_array_tuple_array_tuple) (C1 uint_array_tuple_array_tuple) (D1 uint_array_tuple_array_tuple) (E1 Int) (F1 Int) (G1 uint_array_tuple) (H1 uint_array_tuple) (I1 Int) (J1 Int) (K1 Int) (L1 Int) (M1 Int) (N1 uint_array_tuple_array_tuple) (O1 Int) (P1 Bool) (Q1 uint_array_tuple_array_tuple) (R1 uint_array_tuple_array_tuple) (S1 uint_array_tuple_array_tuple) (T1 Int) (U1 uint_array_tuple) (V1 uint_array_tuple) (W1 uint_array_tuple) (X1 Int) (Y1 uint_array_tuple_array_tuple) (Z1 Int) (A2 Bool) (B2 Int) (C2 uint_array_tuple_array_tuple) (D2 Int) (E2 uint_array_tuple) (F2 Int) (G2 Bool) (H2 uint_array_tuple_array_tuple) (I2 Int) (J2 uint_array_tuple) (K2 Int) (L2 Int) (M2 Int) (N2 Bool) (O2 state_type) (P2 state_type) (Q2 Int) (R2 tx_type) (S2 Int) (T2 Int) (U2 Int) (V2 Int) (W2 Int) (X2 Int) (Y2 Int) (Z2 Int) ) - (=> - (and - (block_64_j_278_335_0 I Q2 C H R2 O2 A D U2 W2 Y2 S2 P2 B E V2 X2 Z2 T2) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array C1) - E1 - (uint_array_tuple (store (uint_array_tuple_accessor_array G1) - F1 - L1) - (uint_array_tuple_accessor_length G1)))) - (a!2 (= G - (uint_array_tuple_array_tuple - (store (uint_array_tuple_array_tuple_accessor_array R1) T1 V1) - (uint_array_tuple_array_tuple_accessor_length R1))))) - (and (not (= (<= Z1 X1) A2)) - (not (= (<= Z V) A1)) - (not (= (<= F2 B2) G2)) - (not (= (<= T R) U)) - (= N2 (= L2 M2)) - (= S1 G) - (= D1 F) - (= N1 F) - (= R1 F) - (= Y1 G) - (= H2 G) - (= W E) - (= S E) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length C1))) - a!2 - (= B1 E) - (= C1 E) - (= Q1 F) - (= C2 G) - (= G1 (select (uint_array_tuple_array_tuple_accessor_array E) E1)) - (= W1 (select (uint_array_tuple_array_tuple_accessor_array R1) T1)) - (= H1 (select (uint_array_tuple_array_tuple_accessor_array C1) E1)) - (= U1 (select (uint_array_tuple_array_tuple_accessor_array F) T1)) - (= V1 (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= E2 (select (uint_array_tuple_array_tuple_accessor_array G) D2)) - (= J2 (select (uint_array_tuple_array_tuple_accessor_array G) I2)) - (= Y (select (uint_array_tuple_array_tuple_accessor_array E) X)) - (= J1 (select (uint_array_tuple_accessor_array G1) F1)) - (= O1 (uint_array_tuple_array_tuple_accessor_length N1)) - (= J I) - (= Z1 (uint_array_tuple_array_tuple_accessor_length Y1)) - (= M2 0) - (= Q P) - (= O N) - (= M L) - (= R V2) - (= I1 (select (uint_array_tuple_accessor_array G1) F1)) - (= V X2) - (= P O) - (= N M) - (= Z (uint_array_tuple_accessor_length Y)) - (= F2 (uint_array_tuple_accessor_length E2)) - (= T1 Z2) - (= K J) - (= E1 V2) - (= T (uint_array_tuple_array_tuple_accessor_length S)) - (= X V2) - (= L K) - (= K1 T2) - (= F1 X2) - (= M1 Z2) - (= L1 K1) - (= B2 V2) - (= X1 X2) - (= L2 (select (uint_array_tuple_accessor_array J2) K2)) - (= I2 X2) - (= D2 V2) - (= K2 V2) - (>= (uint_array_tuple_accessor_length G1) 0) - (>= (uint_array_tuple_accessor_length U1) 0) - (>= (uint_array_tuple_accessor_length E2) 0) - (>= (uint_array_tuple_accessor_length J2) 0) - (>= (uint_array_tuple_accessor_length Y) 0) - (>= J1 0) - (>= O1 0) - (>= Z1 0) - (>= R 0) - (>= I1 0) - (>= V 0) - (>= Z 0) - (>= F2 0) - (>= T1 0) - (>= E1 0) - (>= T 0) - (>= X 0) - (>= K1 0) - (>= F1 0) - (>= M1 0) - (>= L1 0) - (>= V2 0) - (>= B2 0) - (>= X1 0) - (>= L2 0) - (>= I2 0) - (>= D2 0) - (>= K2 0) - (>= Z2 0) - (>= X2 0) - (>= T2 0) - (<= J1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= X2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T2 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= A2 true) - (= P1 true) - (= G2 true) - (= U true) - (= A1 true) - (not (= (<= O1 M1) P1)))) - ) - (block_65_return_function_j__279_335_0 - Q - Q2 - C - H - R2 - O2 - A - D - U2 - W2 - Y2 - S2 - P2 - B - G - V2 - X2 - Z2 - T2) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) ) - (=> - (and - true - ) - (block_74_function_j__279_335_0 G J C F K H A D N P R L I B E O Q S M) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Int) (B1 Int) (C1 Int) ) - (=> - (and - (block_74_function_j__279_335_0 I P D H Q L A E U X A1 R M B F V Y B1 S) - (summary_15_function_j__279_335_0 J P D H Q N B F V Y B1 S O C G W Z C1 T) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 26)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 241)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 74)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 158)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= M L) - (= N (state_type a!1)) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 2655711514) - (= I 0) - (= Y X) - (= V U) - (= S R) - (= B1 A1) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_16_function_j__279_335_0 J P D H Q L A E U X A1 R O C G W Z C1 T) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - true - ) - (block_75_function_setA__300_335_0 G J C F K H A D L N I B E M O) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (block_75_function_setA__300_335_0 G J C F K H A D L N I B E M O) - (and (= B A) (= I H) (= G 0) (= O N) (= M L) (= E D)) - ) - (block_76_setA_299_335_0 G J C F K H A D L N I B E M O) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J uint_array_tuple) (K Int) (L Bool) (M uint_array_tuple) (N Int) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) (T Int) (U Int) (V Int) (W Int) ) - (=> - (and - (block_76_setA_299_335_0 G R C F S P A D T V Q B E U W) - (and (= M B) - (= J B) - (= K (uint_array_tuple_accessor_length J)) - (= O W) - (= I U) - (= H 33) - (= N U) - (>= K 0) - (>= O 0) - (>= I 0) - (>= W 0) - (>= U 0) - (>= N 0) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 N)) (>= N (uint_array_tuple_accessor_length M))) - (= L true) - (not (= (<= K I) L))) - ) - (block_78_function_setA__300_335_0 H R C F S P A D T V Q B E U W) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (block_78_function_setA__300_335_0 G J C F K H A D L N I B E M O) - true - ) - (summary_17_function_setA__300_335_0 G J C F K H A D L N I B E M O) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - (block_77_return_function_setA__300_335_0 G J C F K H A D L N I B E M O) - true - ) - (summary_17_function_setA__300_335_0 G J C F K H A D L N I B E M O) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G crypto_type) (H Int) (I Int) (J Int) (K uint_array_tuple) (L Int) (M Bool) (N uint_array_tuple) (O uint_array_tuple) (P uint_array_tuple) (Q Int) (R Int) (S Int) (T Int) (U Int) (V state_type) (W state_type) (X Int) (Y tx_type) (Z Int) (A1 Int) (B1 Int) (C1 Int) ) - (=> - (and - (block_76_setA_299_335_0 H X D G Y V A E Z B1 W B F A1 C1) - (let ((a!1 (= C - (uint_array_tuple (store (uint_array_tuple_accessor_array O) Q U) - (uint_array_tuple_accessor_length O))))) - (and a!1 - (= K B) - (= N B) - (= P C) - (= O B) - (= Q A1) - (= I H) - (= J A1) - (= U T) - (= L (uint_array_tuple_accessor_length K)) - (= R (select (uint_array_tuple_accessor_array B) Q)) - (= T C1) - (= S (select (uint_array_tuple_accessor_array O) Q)) - (>= Q 0) - (>= J 0) - (>= U 0) - (>= L 0) - (>= R 0) - (>= C1 0) - (>= A1 0) - (>= T 0) - (>= S 0) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= A1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= M true) - (not (= (<= L J) M)))) - ) - (block_77_return_function_setA__300_335_0 I X D G Y V A E Z B1 W C F A1 C1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) ) - (=> - (and - true - ) - (block_79_function_setA__300_335_0 G J C F K H A D L N I B E M O) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) ) - (=> - (and - (block_79_function_setA__300_335_0 I P D H Q L A E R U M B F S V) - (summary_17_function_setA__300_335_0 J P D H Q N B F S V O C G T W) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 213)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 163)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 169)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 122)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= M L) - (= N (state_type a!1)) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 2057937877) - (= S R) - (= I 0) - (= V U) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_18_function_setA__300_335_0 J P D H Q L A E R U O C G T W) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_80_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_80_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - (and (= B A) (= I H) (= M L) (= Q P) (= O N) (= G 0) (= E D)) - ) - (block_81_setB_333_335_0 G J C F K H A D L N P I B E M O Q) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J uint_array_tuple_array_tuple) (K Int) (L Bool) (M Int) (N uint_array_tuple_array_tuple) (O Int) (P state_type) (Q state_type) (R Int) (S tx_type) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) ) - (=> - (and - (block_81_setB_333_335_0 G R C F S P A D T V X Q B E U W Y) - (and (= J E) - (= N E) - (= M W) - (= K (uint_array_tuple_array_tuple_accessor_length J)) - (= H 35) - (= I U) - (= O U) - (>= M 0) - (>= U 0) - (>= K 0) - (>= I 0) - (>= Y 0) - (>= W 0) - (>= O 0) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 O)) (>= O (uint_array_tuple_array_tuple_accessor_length N))) - (= L true) - (not (= (<= K I) L))) - ) - (block_83_function_setB__334_335_0 H R C F S P A D T V X Q B E U W Y) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_83_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - true - ) - (summary_19_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_84_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - true - ) - (summary_19_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_85_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - true - ) - (summary_19_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (block_82_return_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - true - ) - (summary_19_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K uint_array_tuple_array_tuple) (L Int) (M Bool) (N Int) (O uint_array_tuple_array_tuple) (P Int) (Q uint_array_tuple) (R Int) (S Bool) (T uint_array_tuple_array_tuple) (U Int) (V Int) (W state_type) (X state_type) (Y Int) (Z tx_type) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) ) - (=> - (and - (block_81_setB_333_335_0 G Y C F Z W A D A1 C1 E1 X B E B1 D1 F1) - (and (not (= (<= R N) S)) - (= T E) - (= O E) - (= K E) - (= Q (select (uint_array_tuple_array_tuple_accessor_array E) P)) - (= L (uint_array_tuple_array_tuple_accessor_length K)) - (= H G) - (= N D1) - (= I 36) - (= R (uint_array_tuple_accessor_length Q)) - (= J B1) - (= U B1) - (= P B1) - (= V F1) - (>= (uint_array_tuple_accessor_length Q) 0) - (>= L 0) - (>= B1 0) - (>= N 0) - (>= R 0) - (>= J 0) - (>= U 0) - (>= P 0) - (>= F1 0) - (>= D1 0) - (>= V 0) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= B1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= J - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= U - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 U)) (>= U (uint_array_tuple_array_tuple_accessor_length T))) - (= M true) - (= S true) - (not (= (<= L J) M))) - ) - (block_84_function_setB__334_335_0 I Y C F Z W A D A1 C1 E1 X B E B1 D1 F1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H Int) (I Int) (J Int) (K Int) (L uint_array_tuple_array_tuple) (M Int) (N Bool) (O Int) (P uint_array_tuple_array_tuple) (Q Int) (R uint_array_tuple) (S Int) (T Bool) (U uint_array_tuple_array_tuple) (V Int) (W Int) (X uint_array_tuple) (Y Int) (Z state_type) (A1 state_type) (B1 Int) (C1 tx_type) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) ) - (=> - (and - (block_81_setB_333_335_0 G B1 C F C1 Z A D D1 F1 H1 A1 B E E1 G1 I1) - (and (not (= (<= S O) T)) - (= P E) - (= L E) - (= U E) - (= X (select (uint_array_tuple_array_tuple_accessor_array E) V)) - (= R (select (uint_array_tuple_array_tuple_accessor_array E) Q)) - (= I H) - (= W G1) - (= V E1) - (= O G1) - (= K E1) - (= J 37) - (= Q E1) - (= H G) - (= M (uint_array_tuple_array_tuple_accessor_length L)) - (= S (uint_array_tuple_accessor_length R)) - (= Y I1) - (>= (uint_array_tuple_accessor_length X) 0) - (>= (uint_array_tuple_accessor_length R) 0) - (>= W 0) - (>= V 0) - (>= O 0) - (>= E1 0) - (>= K 0) - (>= Q 0) - (>= M 0) - (>= S 0) - (>= I1 0) - (>= G1 0) - (>= Y 0) - (<= W - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= V - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= O - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= K - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Q - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= M - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= S - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= I1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= G1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (or (not (<= 0 W)) (>= W (uint_array_tuple_accessor_length X))) - (= T true) - (= N true) - (not (= (<= M K) N))) - ) - (block_85_function_setB__334_335_0 J B1 C F C1 Z A D D1 F1 H1 A1 B E E1 G1 I1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G crypto_type) (H Int) (I Int) (J Int) (K Int) (L Int) (M uint_array_tuple_array_tuple) (N Int) (O Bool) (P Int) (Q uint_array_tuple_array_tuple) (R Int) (S uint_array_tuple) (T Int) (U Bool) (V uint_array_tuple_array_tuple) (W uint_array_tuple_array_tuple) (X uint_array_tuple_array_tuple) (Y Int) (Z Int) (A1 uint_array_tuple) (B1 uint_array_tuple) (C1 Int) (D1 Int) (E1 Int) (F1 Int) (G1 state_type) (H1 state_type) (I1 Int) (J1 tx_type) (K1 Int) (L1 Int) (M1 Int) (N1 Int) (O1 Int) (P1 Int) ) - (=> - (and - (block_81_setB_333_335_0 H I1 C G J1 G1 A D K1 M1 O1 H1 B E L1 N1 P1) - (let ((a!1 (store (uint_array_tuple_array_tuple_accessor_array W) - Y - (uint_array_tuple (store (uint_array_tuple_accessor_array A1) - Z - F1) - (uint_array_tuple_accessor_length A1))))) - (and (not (= (<= T P) U)) - (= Q E) - (= V E) - (= W E) - (= X F) - (= F - (uint_array_tuple_array_tuple - a!1 - (uint_array_tuple_array_tuple_accessor_length W))) - (= M E) - (= S (select (uint_array_tuple_array_tuple_accessor_array E) R)) - (= A1 (select (uint_array_tuple_array_tuple_accessor_array E) Y)) - (= B1 (select (uint_array_tuple_array_tuple_accessor_array W) Y)) - (= P N1) - (= D1 (select (uint_array_tuple_accessor_array A1) Z)) - (= C1 (select (uint_array_tuple_accessor_array A1) Z)) - (= L L1) - (= J I) - (= I H) - (= R L1) - (= K J) - (= N (uint_array_tuple_array_tuple_accessor_length M)) - (= Y L1) - (= T (uint_array_tuple_accessor_length S)) - (= E1 P1) - (= Z N1) - (= F1 E1) - (>= (uint_array_tuple_accessor_length S) 0) - (>= (uint_array_tuple_accessor_length A1) 0) - (>= P 0) - (>= D1 0) - (>= C1 0) - (>= L 0) - (>= L1 0) - (>= R 0) - (>= N 0) - (>= Y 0) - (>= T 0) - (>= E1 0) - (>= Z 0) - (>= P1 0) - (>= N1 0) - (>= F1 0) - (<= P - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= D1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= C1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= L1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= R - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Y - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= T - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= E1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= Z - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= P1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= N1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= F1 - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (= O true) - (= U true) - (not (= (<= N L) O)))) - ) - (block_82_return_function_setB__334_335_0 - K - I1 - C - G - J1 - G1 - A - D - K1 - M1 - O1 - H1 - B - F - L1 - N1 - P1) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - true - ) - (block_86_function_setB__334_335_0 G J C F K H A D L N P I B E M O Q) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K Int) (L state_type) (M state_type) (N state_type) (O state_type) (P Int) (Q tx_type) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) ) - (=> - (and - (block_86_function_setB__334_335_0 I P D H Q L A E R U X M B F S V Y) - (summary_19_function_setB__334_335_0 J P D H Q N B F S V Y O C G T W Z) - (let ((a!1 (store (balances M) P (+ (select (balances M) P) K))) - (a!2 (= (select (bytes_tuple_accessor_array (msg.data Q)) 3) 225)) - (a!3 (= (select (bytes_tuple_accessor_array (msg.data Q)) 2) 25)) - (a!4 (= (select (bytes_tuple_accessor_array (msg.data Q)) 1) 196)) - (a!5 (= (select (bytes_tuple_accessor_array (msg.data Q)) 0) 90)) - (a!6 (>= (+ (select (balances M) P) K) 0)) - (a!7 (<= (+ (select (balances M) P) K) - 115792089237316195423570985008687907853269984665640564039457584007913129639935))) - (and (= B A) - (= N (state_type a!1)) - (= M L) - a!2 - a!3 - a!4 - a!5 - (= (msg.value Q) 0) - (= (msg.sig Q) 1522801121) - (= V U) - (= I 0) - (= S R) - (= Y X) - (>= (tx.origin Q) 0) - (>= (tx.gasprice Q) 0) - (>= (msg.value Q) 0) - (>= (msg.sender Q) 0) - (>= (block.timestamp Q) 0) - (>= (block.number Q) 0) - (>= (block.gaslimit Q) 0) - (>= (block.difficulty Q) 0) - (>= (block.coinbase Q) 0) - (>= (block.chainid Q) 0) - (>= (block.basefee Q) 0) - (>= (bytes_tuple_accessor_length (msg.data Q)) 4) - a!6 - (>= K (msg.value Q)) - (<= (tx.origin Q) 1461501637330902918203684832716283019655932542975) - (<= (tx.gasprice Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.value Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (msg.sender Q) 1461501637330902918203684832716283019655932542975) - (<= (block.timestamp Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.number Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.gaslimit Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.difficulty Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.coinbase Q) 1461501637330902918203684832716283019655932542975) - (<= (block.chainid Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - (<= (block.basefee Q) - 115792089237316195423570985008687907853269984665640564039457584007913129639935) - a!7 - (= F E))) - ) - (summary_20_function_setB__334_335_0 J P D H Q L A E R U X O C G T W Z) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (and (= B A) (= I H) (= G 0) (= E D)) - ) - (contract_initializer_entry_88_C_335_0 G J C F K H I A D B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (contract_initializer_entry_88_C_335_0 G J C F K H I A D B E) - true - ) - (contract_initializer_after_init_89_C_335_0 G J C F K H I A D B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (contract_initializer_after_init_89_C_335_0 G J C F K H I A D B E) - true - ) - (contract_initializer_87_C_335_0 G J C F K H I A D B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) ) - (=> - (and - (let ((a!1 (uint_array_tuple_array_tuple - ((as const (Array Int uint_array_tuple)) - (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - 0))) - (and (= E D) - (= B (uint_array_tuple ((as const (Array Int Int)) 0) 0)) - (= B A) - (= I H) - (= G 0) - (>= (select (balances I) J) (msg.value K)) - (= E a!1))) - ) - (implicit_constructor_entry_90_C_335_0 G J C F K H I A D B E) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K state_type) (L state_type) (M state_type) (N Int) (O tx_type) ) - (=> - (and - (implicit_constructor_entry_90_C_335_0 I N D H O K L A E B F) - (contract_initializer_87_C_335_0 J N D H O L M B F C G) - (not (<= J 0)) - ) - (summary_constructor_2_C_335_0 J N D H O K M A E C G) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C uint_array_tuple) (D abi_type) (E uint_array_tuple_array_tuple) (F uint_array_tuple_array_tuple) (G uint_array_tuple_array_tuple) (H crypto_type) (I Int) (J Int) (K state_type) (L state_type) (M state_type) (N Int) (O tx_type) ) - (=> - (and - (contract_initializer_87_C_335_0 J N D H O L M B F C G) - (implicit_constructor_entry_90_C_335_0 I N D H O K L A E B F) - (= J 0) - ) - (summary_constructor_2_C_335_0 J N D H O K M A E C G) - ) - ) -) -(assert - (forall ( (A uint_array_tuple) (B uint_array_tuple) (C abi_type) (D uint_array_tuple_array_tuple) (E uint_array_tuple_array_tuple) (F crypto_type) (G Int) (H state_type) (I state_type) (J Int) (K tx_type) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) - (=> - (and - (summary_12_function_h__150_335_0 G J C F K H A D N P L I B E O Q M) - (interface_0_C_335_0 J C F H A D) - (= G 10) - ) - error_target_45_0 - ) - ) -) -(assert - (forall ( (CHC_COMP_UNUSED Bool) ) - (=> - (and - error_target_45_0 - true - ) - false - ) - ) -) - -(check-sat) -(exit) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index 2b13530304..c1db6b71b5 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -77,6 +77,7 @@ class ChcPasses(parseContext: ParseContext) : ProcedurePassManager(listOf( // FpFunctionsToExprsPass(), // PthreadFunctionsPass(), // trying to inline procedures +), listOf( InlineProceduresPass(parseContext), RemoveDeadEnds(parseContext), EliminateSelfLoops(parseContext),