Commit 769afc7b authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Migrate benchmarks from pending repository.

parent 349270f4
(set-info :smt-lib-version 2.6)
(set-logic UFBVLIA)
(set-info :source |
Generated by: Maria A Schett, Julian Nagele
Generated on: 2021-01-03
Generator: https://github.com/juliannagele/ebso
Application: superoptimization of EVM bytecode:
PUSH 12 SLOAD
Publication: Blockchain Superoptimizer ( https://arxiv.org/abs/2005.05912 )
Target solver: Z3
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun k () Int)
(declare-fun used_gas_t ((_ BitVec 4) Int) Int)
(declare-fun used_gas_s ((_ BitVec 4) Int) Int)
(declare-fun storage_t ((_ BitVec 4) Int (_ BitVec 4)) (_ BitVec 4))
(declare-fun storage_s ((_ BitVec 4) Int (_ BitVec 4)) (_ BitVec 4))
(declare-fun exc_halt_t (Int) Bool)
(declare-fun exc_halt_s (Int) Bool)
(declare-fun sc_t (Int) (_ BitVec 6))
(declare-fun stack_t ((_ BitVec 4) Int (_ BitVec 6)) (_ BitVec 4))
(declare-fun stack_s ((_ BitVec 4) Int (_ BitVec 6)) (_ BitVec 4))
(declare-fun sc_s (Int) (_ BitVec 6))
(declare-fun instr (Int) Int)
(declare-fun a (Int) (_ BitVec 4))
(assert
(forall ((x_SLOAD_0 (_ BitVec 4)) )(let (($x11 (<= k 203)))
(let (($x1986 (forall ((w (_ BitVec 4)) )(let ((?x1984 (storage_s x_SLOAD_0 2 w)))
(= ?x1984 (storage_t x_SLOAD_0 k w))))
))
(let (($x25 (exc_halt_t k)))
(let (($x26 (exc_halt_s 2)))
(let (($x27 (= $x26 $x25)))
(let (($x2693 (forall ((n (_ BitVec 6)) )(let ((?x1989 (stack_s x_SLOAD_0 2 n)))
(let (($x1990 (= ?x1989 (stack_t x_SLOAD_0 k n))))
(or $x1990 (bvsle (sc_t k) n)))))
))
(let ((?x33 (sc_t k)))
(let ((?x43 (sc_s 2)))
(let (($x44 (= ?x43 ?x33)))
(let ((?x1996 (used_gas_s x_SLOAD_0 0)))
(let (($x1997 (= ?x1996 (used_gas_t x_SLOAD_0 0))))
(let (($x2002 (forall ((w (_ BitVec 4)) )(let ((?x2000 (storage_s x_SLOAD_0 0 w)))
(= ?x2000 (storage_t x_SLOAD_0 0 w))))
))
(let (($x58 (exc_halt_t 0)))
(let (($x59 (exc_halt_s 0)))
(let (($x60 (= $x59 $x58)))
(let (($x3230 (forall ((n (_ BitVec 6)) )(let ((?x2005 (stack_s x_SLOAD_0 0 n)))
(let (($x2006 (= ?x2005 (stack_t x_SLOAD_0 0 n))))
(or $x2006 (bvsle (sc_t 0) n)))))
))
(let ((?x65 (sc_t 0)))
(let ((?x74 (sc_s 0)))
(let (($x75 (= ?x74 ?x65)))
(let (($x1018 (>= k 0)))
(let (($x3391 (forall ((j Int) )(let ((?x1027 (instr j)))
(let (($x1028 (= ?x1027 54)))
(let (($x1029 (= ?x1027 53)))
(let (($x1030 (= ?x1027 52)))
(let (($x1031 (= ?x1027 51)))
(let (($x1032 (= ?x1027 50)))
(let (($x1033 (= ?x1027 49)))
(let (($x1034 (= ?x1027 48)))
(let (($x1035 (= ?x1027 47)))
(let (($x1036 (= ?x1027 46)))
(let (($x1037 (= ?x1027 45)))
(let (($x1038 (= ?x1027 44)))
(let (($x1039 (= ?x1027 43)))
(let (($x1040 (= ?x1027 42)))
(let (($x1041 (= ?x1027 41)))
(let (($x1042 (= ?x1027 40)))
(let (($x1043 (= ?x1027 39)))
(let (($x1044 (= ?x1027 38)))
(let (($x1045 (= ?x1027 37)))
(let (($x1046 (= ?x1027 36)))
(let (($x1047 (= ?x1027 35)))
(let (($x1048 (= ?x1027 34)))
(let (($x1049 (= ?x1027 33)))
(let (($x1050 (= ?x1027 32)))
(let (($x1051 (= ?x1027 31)))
(let (($x1052 (= ?x1027 30)))
(let (($x1053 (= ?x1027 29)))
(let (($x1054 (= ?x1027 28)))
(let (($x1055 (= ?x1027 27)))
(let (($x1056 (= ?x1027 26)))
(let (($x1057 (= ?x1027 25)))
(let (($x1058 (= ?x1027 24)))
(let (($x1059 (= ?x1027 23)))
(let (($x1060 (= ?x1027 22)))
(let (($x1061 (= ?x1027 21)))
(let (($x1062 (= ?x1027 20)))
(let (($x1063 (= ?x1027 19)))
(let (($x1064 (= ?x1027 18)))
(let (($x1065 (= ?x1027 17)))
(let (($x1066 (= ?x1027 16)))
(let (($x1067 (= ?x1027 15)))
(let (($x1068 (= ?x1027 14)))
(let (($x1069 (= ?x1027 13)))
(let (($x1070 (= ?x1027 12)))
(let (($x1071 (= ?x1027 11)))
(let (($x1072 (= ?x1027 10)))
(let (($x1073 (= ?x1027 9)))
(let (($x1074 (= ?x1027 8)))
(let (($x1075 (= ?x1027 7)))
(let (($x1076 (= ?x1027 6)))
(let (($x1077 (= ?x1027 5)))
(let (($x1078 (= ?x1027 4)))
(let (($x1079 (= ?x1027 3)))
(let (($x1080 (= ?x1027 2)))
(let (($x1081 (= ?x1027 1)))
(let (($x1082 (= ?x1027 0)))
(let (($x1083 (or $x1082 $x1081 $x1080 $x1079 $x1078 $x1077 $x1076 $x1075 $x1074 $x1073 $x1072 $x1071 $x1070 $x1069 $x1068 $x1067 $x1066 $x1065 $x1064 $x1063 $x1062 $x1061 $x1060 $x1059 $x1058 $x1057 $x1056 $x1055 $x1054 $x1053 $x1052 $x1051 $x1050 $x1049 $x1048 $x1047 $x1046 $x1045 $x1044 $x1043 $x1042 $x1041 $x1040 $x1039 $x1038 $x1037 $x1036 $x1035 $x1034 $x1033 $x1032 $x1031 $x1030 $x1029 $x1028)))
(let (($x2930 (not (= ((_ extract 6 6) (bvadd (_ bv1 7) (concat (_ bv0 1) (sc_t j)))) (_ bv0 1)))))
(let (($x3246 (not (bvsle (_ bv0 6) (bvadd (_ bv48 6) (sc_t j))))))
(let (($x1093 (exc_halt_t j)))
(let ((?x2691 (+ 1 j)))
(let (($x2720 (exc_halt_t ?x2691)))
(let (($x2718 (forall ((w (_ BitVec 4)) )(let ((?x2014 (storage_t x_SLOAD_0 j w)))
(let ((?x2713 (+ 1 j)))
(let ((?x2712 (storage_t x_SLOAD_0 ?x2713 w)))
(= ?x2712 ?x2014)))))
))
(let (($x3245 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv48 6) (sc_t j)) n)))))
))
(let ((?x2692 (sc_t ?x2691)))
(let (($x2922 (= ?x2692 (bvadd (_ bv1 6) (sc_t j)))))
(let ((?x2705 (used_gas_t x_SLOAD_0 ?x2691)))
(let (($x2707 (= ?x2705 (+ 3 (used_gas_t x_SLOAD_0 j)))))
(let ((?x1084 (sc_t j)))
(let ((?x2697 (bvadd (_ bv63 6) ?x1084)))
(let ((?x2698 (stack_t x_SLOAD_0 j ?x2697)))
(let (($x3276 (= (stack_t x_SLOAD_0 ?x2691 ?x2697) ?x2698)))
(let ((?x2701 (bvadd (_ bv62 6) ?x1084)))
(let ((?x2702 (stack_t x_SLOAD_0 j ?x2701)))
(let (($x3283 (= (stack_t x_SLOAD_0 ?x2691 ?x2701) ?x2702)))
(let ((?x2774 (bvadd (_ bv61 6) ?x1084)))
(let ((?x2775 (stack_t x_SLOAD_0 j ?x2774)))
(let (($x3290 (= (stack_t x_SLOAD_0 ?x2691 ?x2774) ?x2775)))
(let ((?x2956 (bvadd (_ bv60 6) ?x1084)))
(let ((?x2957 (stack_t x_SLOAD_0 j ?x2956)))
(let (($x3297 (= (stack_t x_SLOAD_0 ?x2691 ?x2956) ?x2957)))
(let ((?x2979 (bvadd (_ bv59 6) ?x1084)))
(let ((?x2980 (stack_t x_SLOAD_0 j ?x2979)))
(let (($x3304 (= (stack_t x_SLOAD_0 ?x2691 ?x2979) ?x2980)))
(let ((?x3002 (bvadd (_ bv58 6) ?x1084)))
(let ((?x3003 (stack_t x_SLOAD_0 j ?x3002)))
(let (($x3311 (= (stack_t x_SLOAD_0 ?x2691 ?x3002) ?x3003)))
(let ((?x3025 (bvadd (_ bv57 6) ?x1084)))
(let ((?x3026 (stack_t x_SLOAD_0 j ?x3025)))
(let (($x3318 (= (stack_t x_SLOAD_0 ?x2691 ?x3025) ?x3026)))
(let ((?x3048 (bvadd (_ bv56 6) ?x1084)))
(let ((?x3049 (stack_t x_SLOAD_0 j ?x3048)))
(let (($x3325 (= (stack_t x_SLOAD_0 ?x2691 ?x3048) ?x3049)))
(let ((?x3071 (bvadd (_ bv55 6) ?x1084)))
(let ((?x3072 (stack_t x_SLOAD_0 j ?x3071)))
(let (($x3332 (= (stack_t x_SLOAD_0 ?x2691 ?x3071) ?x3072)))
(let ((?x3094 (bvadd (_ bv54 6) ?x1084)))
(let ((?x3095 (stack_t x_SLOAD_0 j ?x3094)))
(let (($x3339 (= (stack_t x_SLOAD_0 ?x2691 ?x3094) ?x3095)))
(let ((?x3117 (bvadd (_ bv53 6) ?x1084)))
(let ((?x3118 (stack_t x_SLOAD_0 j ?x3117)))
(let (($x3346 (= (stack_t x_SLOAD_0 ?x2691 ?x3117) ?x3118)))
(let ((?x3140 (bvadd (_ bv52 6) ?x1084)))
(let ((?x3141 (stack_t x_SLOAD_0 j ?x3140)))
(let (($x3353 (= (stack_t x_SLOAD_0 ?x2691 ?x3140) ?x3141)))
(let ((?x3163 (bvadd (_ bv51 6) ?x1084)))
(let ((?x3164 (stack_t x_SLOAD_0 j ?x3163)))
(let (($x3360 (= (stack_t x_SLOAD_0 ?x2691 ?x3163) ?x3164)))
(let ((?x3186 (bvadd (_ bv50 6) ?x1084)))
(let ((?x3187 (stack_t x_SLOAD_0 j ?x3186)))
(let (($x3367 (= (stack_t x_SLOAD_0 ?x2691 ?x3186) ?x3187)))
(let ((?x3209 (bvadd (_ bv49 6) ?x1084)))
(let ((?x3210 (stack_t x_SLOAD_0 j ?x3209)))
(let (($x3374 (= (stack_t x_SLOAD_0 ?x2691 ?x3209) ?x3210)))
(let ((?x3232 (bvadd (_ bv48 6) ?x1084)))
(let ((?x3233 (stack_t x_SLOAD_0 j ?x3232)))
(let ((?x2695 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv63 6) ?x2692))))
(let (($x3234 (= ?x2695 ?x3233)))
(let (($x3384 (and $x3234 (= (stack_t x_SLOAD_0 ?x2691 ?x3232) ?x3233) $x3374 $x3367 $x3360 $x3353 $x3346 $x3339 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3245 $x2718 (= $x2720 (or $x1093 $x3246 $x2930)))))
(let (($x3222 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv49 6) (sc_t j)) n)))))
))
(let (($x3211 (= ?x2695 ?x3210)))
(let (($x3377 (and $x3211 $x3374 $x3367 $x3360 $x3353 $x3346 $x3339 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3222 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3209)) $x2930)))))
(let (($x3199 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv50 6) (sc_t j)) n)))))
))
(let (($x3188 (= ?x2695 ?x3187)))
(let (($x3370 (and $x3188 $x3367 $x3360 $x3353 $x3346 $x3339 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3199 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3186)) $x2930)))))
(let (($x3176 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv51 6) (sc_t j)) n)))))
))
(let (($x3165 (= ?x2695 ?x3164)))
(let (($x3363 (and $x3165 $x3360 $x3353 $x3346 $x3339 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3176 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3163)) $x2930)))))
(let (($x3153 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv52 6) (sc_t j)) n)))))
))
(let (($x3142 (= ?x2695 ?x3141)))
(let (($x3356 (and $x3142 $x3353 $x3346 $x3339 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3153 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3140)) $x2930)))))
(let (($x3130 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv53 6) (sc_t j)) n)))))
))
(let (($x3119 (= ?x2695 ?x3118)))
(let (($x3349 (and $x3119 $x3346 $x3339 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3130 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3117)) $x2930)))))
(let (($x3107 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv54 6) (sc_t j)) n)))))
))
(let (($x3096 (= ?x2695 ?x3095)))
(let (($x3342 (and $x3096 $x3339 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3107 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3094)) $x2930)))))
(let (($x3084 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv55 6) (sc_t j)) n)))))
))
(let (($x3073 (= ?x2695 ?x3072)))
(let (($x3335 (and $x3073 $x3332 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3084 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3071)) $x2930)))))
(let (($x3061 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv56 6) (sc_t j)) n)))))
))
(let (($x3050 (= ?x2695 ?x3049)))
(let (($x3328 (and $x3050 $x3325 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3061 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3048)) $x2930)))))
(let (($x3038 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv57 6) (sc_t j)) n)))))
))
(let (($x3027 (= ?x2695 ?x3026)))
(let (($x3321 (and $x3027 $x3318 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3038 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3025)) $x2930)))))
(let (($x3015 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv58 6) (sc_t j)) n)))))
))
(let (($x3004 (= ?x2695 ?x3003)))
(let (($x3314 (and $x3004 $x3311 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x3015 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3002)) $x2930)))))
(let (($x2992 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv59 6) (sc_t j)) n)))))
))
(let (($x2981 (= ?x2695 ?x2980)))
(let (($x3307 (and $x2981 $x3304 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x2992 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2979)) $x2930)))))
(let (($x2969 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv60 6) (sc_t j)) n)))))
))
(let (($x2958 (= ?x2695 ?x2957)))
(let (($x3300 (and $x2958 $x3297 $x3290 $x3283 $x3276 $x2707 $x2922 $x2969 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2956)) $x2930)))))
(let (($x2793 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv61 6) (sc_t j)) n)))))
))
(let (($x2944 (= ?x2695 ?x2775)))
(let (($x3293 (and $x2944 $x3290 $x3283 $x3276 $x2707 $x2922 $x2793 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2774)) $x2930)))))
(let (($x2717 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or (bvsle (bvadd (_ bv62 6) (sc_t j)) n) $x2715))))
))
(let (($x2936 (= ?x2695 ?x2702)))
(let (($x3286 (and $x2936 $x3283 $x3276 $x2707 $x2922 $x2717 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2701)) $x2930)))))
(let (($x2856 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv63 6) (sc_t j)) n)))))
))
(let (($x3279 (and (= ?x2695 ?x2698) $x3276 $x2707 $x2922 $x2856 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2697)) $x2930)))))
(let (($x3268 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or $x2715 (bvsle (bvadd (_ bv47 6) (sc_t j)) n)))))
))
(let (($x2850 (= ?x2692 ?x1084)))
(let ((?x2939 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv62 6) ?x2692))))
(let (($x2949 (= ?x2939 ?x2702)))
(let ((?x2947 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv61 6) ?x2692))))
(let (($x2963 (= ?x2947 ?x2775)))
(let ((?x2961 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv60 6) ?x2692))))
(let (($x2986 (= ?x2961 ?x2957)))
(let ((?x2984 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv59 6) ?x2692))))
(let (($x3009 (= ?x2984 ?x2980)))
(let ((?x3007 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv58 6) ?x2692))))
(let (($x3032 (= ?x3007 ?x3003)))
(let ((?x3030 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv57 6) ?x2692))))
(let (($x3055 (= ?x3030 ?x3026)))
(let ((?x3053 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv56 6) ?x2692))))
(let (($x3078 (= ?x3053 ?x3049)))
(let ((?x3076 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv55 6) ?x2692))))
(let (($x3101 (= ?x3076 ?x3072)))
(let ((?x3099 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv54 6) ?x2692))))
(let (($x3124 (= ?x3099 ?x3095)))
(let ((?x3122 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv53 6) ?x2692))))
(let (($x3147 (= ?x3122 ?x3118)))
(let ((?x3145 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv52 6) ?x2692))))
(let (($x3170 (= ?x3145 ?x3141)))
(let ((?x3168 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv51 6) ?x2692))))
(let (($x3193 (= ?x3168 ?x3164)))
(let ((?x3191 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv50 6) ?x2692))))
(let (($x3216 (= ?x3191 ?x3187)))
(let ((?x3214 (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv49 6) ?x2692))))
(let (($x3239 (= ?x3214 ?x3210)))
(let (($x3271 (and (= ?x2695 (stack_t x_SLOAD_0 j (bvadd (_ bv47 6) ?x1084))) (= (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv47 6) ?x2692)) ?x2698) (= (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv48 6) ?x2692)) ?x3233) $x3239 $x3216 $x3193 $x3170 $x3147 $x3124 $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3268 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) (bvadd (_ bv47 6) ?x1084))))))))
(let (($x3249 (and $x3234 (= (stack_t x_SLOAD_0 ?x2691 (bvadd (_ bv48 6) ?x2692)) ?x2698) $x3239 $x3216 $x3193 $x3170 $x3147 $x3124 $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3245 $x2718 (= $x2720 (or $x1093 $x3246)))))
(let (($x3226 (and $x3211 (= ?x3214 ?x2698) $x3216 $x3193 $x3170 $x3147 $x3124 $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3222 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3209)))))))
(let (($x3203 (and $x3188 (= ?x3191 ?x2698) $x3193 $x3170 $x3147 $x3124 $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3199 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3186)))))))
(let (($x3180 (and $x3165 (= ?x3168 ?x2698) $x3170 $x3147 $x3124 $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3176 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3163)))))))
(let (($x3157 (and $x3142 (= ?x3145 ?x2698) $x3147 $x3124 $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3153 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3140)))))))
(let (($x3134 (and $x3119 (= ?x3122 ?x2698) $x3124 $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3130 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3117)))))))
(let (($x3111 (and $x3096 (= ?x3099 ?x2698) $x3101 $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3107 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3094)))))))
(let (($x3088 (and $x3073 (= ?x3076 ?x2698) $x3078 $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3084 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3071)))))))
(let (($x3065 (and $x3050 (= ?x3053 ?x2698) $x3055 $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3061 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3048)))))))
(let (($x3042 (and $x3027 (= ?x3030 ?x2698) $x3032 $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3038 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3025)))))))
(let (($x3019 (and $x3004 (= ?x3007 ?x2698) $x3009 $x2986 $x2963 $x2949 $x2707 $x2850 $x3015 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x3002)))))))
(let (($x2996 (and $x2981 (= ?x2984 ?x2698) $x2986 $x2963 $x2949 $x2707 $x2850 $x2992 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2979)))))))
(let (($x2973 (and $x2958 (= ?x2961 ?x2698) $x2963 $x2949 $x2707 $x2850 $x2969 $x2718 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2956)))))))
(let (($x2796 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2774))))))
(let (($x2952 (or (not $x1058) (and $x2944 (= ?x2947 ?x2698) $x2949 $x2707 $x2850 $x2793 $x2718 $x2796))))
(let (($x2724 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2701))))))
(let (($x2926 (forall ((n (_ BitVec 6)) )(let ((?x2018 (stack_t x_SLOAD_0 j n)))
(let (($x2715 (= (stack_t x_SLOAD_0 (+ 1 j) n) ?x2018)))
(or (bvsle (sc_t j) n) $x2715))))
))
(let (($x2933 (and (= (stack_t x_SLOAD_0 ?x2691 ?x1084) (a j)) $x2707 $x2922 $x2926 $x2718 (= $x2720 (or $x1093 $x2930)))))
(let (($x2787 (= ?x2692 ?x2701)))
(let ((?x2913 (ite (= (storage_t x_SLOAD_0 j ?x2698) (_ bv0 4)) (ite (= ?x2702 (_ bv0 4)) 5000 20000) (ite (= ?x2702 (_ bv0 4)) (- 10000) 5000))))
(let ((?x2026 (used_gas_t x_SLOAD_0 j)))
(let (($x2907 (forall ((w (_ BitVec 4)) )(let ((?x2014 (storage_t x_SLOAD_0 j w)))
(let ((?x2905 (ite (= w (stack_t x_SLOAD_0 j (bvadd (_ bv63 6) (sc_t j)))) (stack_t x_SLOAD_0 j (bvadd (_ bv62 6) (sc_t j))) ?x2014)))
(let ((?x2713 (+ 1 j)))
(let ((?x2712 (storage_t x_SLOAD_0 ?x2713 w)))
(= ?x2712 ?x2905))))))
))
(let (($x2859 (= $x2720 (or $x1093 (not (bvsle (_ bv0 6) ?x2697))))))
(let (($x2897 (and (= ?x2695 (storage_t x_SLOAD_0 j ?x2698)) (= ?x2705 (+ 200 ?x2026)) $x2850 $x2856 $x2718 $x2859)))
(let (($x2892 (or (not $x1063) (and (= ?x2705 (+ 2 ?x2026)) (= ?x2692 ?x2697) $x2856 $x2718 $x2859))))
(let (($x2887 (or (not $x1064) (and (= ?x2695 (bvnot ?x2698)) $x2707 $x2850 $x2856 $x2718 $x2859))))
(let (($x2883 (or (not $x1065) (and (= ?x2695 (bvxor ?x2698 ?x2702)) $x2707 (= ?x2692 ?x2697) $x2717 $x2718 $x2724))))
(let (($x2878 (or (not $x1066) (and (= ?x2695 (bvor ?x2698 ?x2702)) $x2707 (= ?x2692 ?x2697) $x2717 $x2718 $x2724))))
(let (($x2708 (= ?x2692 ?x2697)))
(let (($x2871 (and (= ?x2695 (bvnot (bvor (bvnot ?x2698) (bvnot ?x2702)))) $x2707 $x2708 $x2717 $x2718 $x2724)))
(let (($x2863 (and (= ?x2695 (ite (= ?x2698 (_ bv0 4)) (_ bv1 4) (_ bv0 4))) $x2707 $x2850 $x2856 $x2718 $x2859)))
(let (($x2844 (and (= ?x2695 (ite (= ?x2698 ?x2702) (_ bv1 4) (_ bv0 4))) $x2707 $x2708 $x2717 $x2718 $x2724)))
(let (($x2838 (and (= ?x2695 (ite (bvsle ?x2698 ?x2702) (_ bv0 4) (_ bv1 4))) $x2707 $x2708 $x2717 $x2718 $x2724)))
(let (($x2831 (and (= ?x2695 (ite (bvsle ?x2702 ?x2698) (_ bv0 4) (_ bv1 4))) $x2707 $x2708 $x2717 $x2718 $x2724)))
(let (($x2824 (and (= ?x2695 (ite (bvule ?x2698 ?x2702) (_ bv0 4) (_ bv1 4))) $x2707 $x2708 $x2717 $x2718 $x2724)))
(let (($x2817 (and (= ?x2695 (ite (bvule ?x2702 ?x2698) (_ bv0 4) (_ bv1 4))) $x2707 $x2708 $x2717 $x2718 $x2724)))
(let (($x2786 (= ?x2705 (+ 8 ?x2026))))
(let ((?x2806 (bvurem (bvmul (concat (_ bv0 4) ?x2702) (concat (_ bv0 4) ?x2698)) (concat (_ bv0 4) ?x2775))))
(let (($x2776 (= ?x2775 (_ bv0 4))))
(let (($x2810 (and (= ?x2695 (ite $x2776 (_ bv0 4) ((_ extract 3 0) ?x2806))) $x2786 $x2787 $x2793 $x2718 $x2796)))
(let ((?x2781 (bvurem (bvadd (concat (_ bv0 1) ?x2698) (concat (_ bv0 1) ?x2702)) (concat (_ bv0 1) ?x2775))))
(let (($x2799 (and (= ?x2695 (ite $x2776 (_ bv0 4) ((_ extract 3 0) ?x2781))) $x2786 $x2787 $x2793 $x2718 $x2796)))
(let (($x2734 (= ?x2705 (+ 5 ?x2026))))
(let (($x2768 (and (= ?x2695 (ite (= ?x2702 (_ bv0 4)) (_ bv0 4) (bvsrem ?x2698 ?x2702))) $x2734 $x2708 $x2717 $x2718 $x2724)))
(let (($x2762 (and (= ?x2695 (ite (= ?x2702 (_ bv0 4)) (_ bv0 4) (bvurem ?x2698 ?x2702))) $x2734 $x2708 $x2717 $x2718 $x2724)))
(let (($x2756 (and (= ?x2695 (ite (= ?x2702 (_ bv0 4)) (_ bv0 4) (bvsdiv ?x2698 ?x2702))) $x2734 $x2708 $x2717 $x2718 $x2724)))
(let (($x2750 (and (= ?x2695 (ite (= ?x2702 (_ bv0 4)) (_ bv0 4) (bvudiv ?x2698 ?x2702))) $x2734 $x2708 $x2717 $x2718 $x2724)))
(let (($x2743 (and (= ?x2695 (bvadd ?x2698 (bvmul (_ bv15 4) ?x2702))) $x2707 $x2708 $x2717 $x2718 $x2724)))
(let (($x2738 (or (not $x1081) (and (= ?x2695 (bvmul ?x2702 ?x2698)) $x2734 $x2708 $x2717 $x2718 $x2724))))
(let (($x2730 (or (not $x1082) (and (= ?x2695 (bvadd ?x2698 ?x2702)) $x2707 $x2708 $x2717 $x2718 $x2724))))
(let (($x3387 (and $x2730 $x2738 (or (not $x1080) $x2743) (or (not $x1079) $x2750) (or (not $x1078) $x2756) (or (not $x1077) $x2762) (or (not $x1076) $x2768) (or (not $x1075) $x2799) (or (not $x1074) $x2810) (or (not $x1073) $x2817) (or (not $x1072) $x2824) (or (not $x1071) $x2831) (or (not $x1070) $x2838) (or (not $x1069) $x2844) (or (not $x1068) $x2863) (or (not $x1067) $x2871) $x2878 $x2883 $x2887 $x2892 (or (not $x1062) $x2897) (or (not $x1061) (and $x2907 (= ?x2705 (+ ?x2026 ?x2913)) $x2787 $x2717 $x2724)) (or (not $x1060) $x2933) (or (not $x1059) (and $x2936 (= ?x2939 ?x2698) $x2707 $x2850 $x2717 $x2718 $x2724)) $x2952 (or (not $x1057) $x2973) (or (not $x1056) $x2996) (or (not $x1055) $x3019) (or (not $x1054) $x3042) (or (not $x1053) $x3065) (or (not $x1052) $x3088) (or (not $x1051) $x3111) (or (not $x1050) $x3134) (or (not $x1049) $x3157) (or (not $x1048) $x3180) (or (not $x1047) $x3203) (or (not $x1046) $x3226) (or (not $x1045) $x3249) (or (not $x1044) $x3271) (or (not $x1043) $x3279) (or (not $x1042) $x3286) (or (not $x1041) $x3293) (or (not $x1040) $x3300) (or (not $x1039) $x3307) (or (not $x1038) $x3314) (or (not $x1037) $x3321) (or (not $x1036) $x3328) (or (not $x1035) $x3335) (or (not $x1034) $x3342) (or (not $x1033) $x3349) (or (not $x1032) $x3356) (or (not $x1031) $x3363) (or (not $x1030) $x3370) (or (not $x1029) $x3377) (or (not $x1028) $x3384))))
(and (or (not (and (not (<= k j)) (>= j 0))) $x3387) $x1083)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))
(let (($x2687 (= $x26 (or (exc_halt_s 1) (not (bvsle (_ bv0 6) (bvadd (_ bv63 6) (sc_s 1))))))))
(let (($x2683 (forall ((w (_ BitVec 4)) )(let ((?x2586 (storage_s x_SLOAD_0 1 w)))
(let ((?x1984 (storage_s x_SLOAD_0 2 w)))
(= ?x1984 ?x2586))))
))
(let (($x2682 (forall ((n (_ BitVec 6)) )(or (bvsle (bvadd (_ bv63 6) (sc_s 1)) n) (= (stack_s x_SLOAD_0 2 n) (stack_s x_SLOAD_0 1 n))))
))
(let (($x2674 (= (stack_s x_SLOAD_0 2 (bvadd (_ bv63 6) ?x43)) (storage_s x_SLOAD_0 1 (stack_s x_SLOAD_0 1 (bvadd (_ bv63 6) (sc_s 1)))))))
(let (($x1949 (exc_halt_s 1)))
(let (($x2666 (= $x1949 (or $x59 (not (= ((_ extract 6 6) (bvadd (_ bv1 7) (concat (_ bv0 1) ?x74))) (_ bv0 1)))))))
(let (($x2657 (forall ((w (_ BitVec 4)) )(let ((?x2000 (storage_s x_SLOAD_0 0 w)))
(let ((?x2586 (storage_s x_SLOAD_0 1 w)))
(= ?x2586 ?x2000))))
))
(let (($x2656 (forall ((n (_ BitVec 6)) )(or (bvsle (sc_s 0) n) (= (stack_s x_SLOAD_0 1 n) (stack_s x_SLOAD_0 0 n))))
))
(let (($x2647 (forall ((w (_ BitVec 4)) )(let ((?x2645 (ite (= w (stack_s x_SLOAD_0 1 (bvadd (_ bv63 6) (sc_s 1)))) x_SLOAD_0 (_ bv0 4))))
(let ((?x2000 (storage_s x_SLOAD_0 0 w)))
(= ?x2000 ?x2645))))
))
(let (($x2630 (= ?x1996 0)))
(let (($x1884 (= ?x74 (_ bv0 6))))
(and $x1884 (not $x59) $x2630 $x2647 (= (stack_s x_SLOAD_0 1 ?x74) (_ bv12 4)) (= (used_gas_s x_SLOAD_0 1) (+ 3 ?x1996)) (= (sc_s 1) (bvadd (_ bv1 6) ?x74)) $x2656 $x2657 $x2666 $x2674 (= (used_gas_s x_SLOAD_0 2) (+ 200 (used_gas_s x_SLOAD_0 1))) (= ?x43 (sc_s 1)) $x2682 $x2683 $x2687 $x3391 $x1018 $x75 $x3230 $x60 $x2002 $x1997 $x44 $x2693 $x27 $x1986 (not (<= (used_gas_s x_SLOAD_0 2) (used_gas_t x_SLOAD_0 k))) $x11))))))))))))))))))))))))))))))))))
)
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic UFBVLIA)
(set-info :source |
Generated by: Maria A Schett, Julian Nagele
Generated on: 2021-01-03
Generator: https://github.com/juliannagele/ebso
Application: superoptimization of EVM bytecode:
PUSH 10 SLOAD SWAP1
Publication: Blockchain Superoptimizer ( https://arxiv.org/abs/2005.05912 )
Target solver: Z3
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun k () Int)
(declare-fun used_gas_t ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) Int) Int)
(declare-fun used_gas_s ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) Int) Int)
(declare-fun storage_t ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) Int (_ BitVec 1)) (_ BitVec 1))
(declare-fun storage_s ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) Int (_ BitVec 1)) (_ BitVec 1))
(declare-fun exc_halt_t (Int) Bool)
(declare-fun exc_halt_s (Int) Bool)
(declare-fun sc_t (Int) (_ BitVec 6))
(declare-fun stack_t ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) Int (_ BitVec 6)) (_ BitVec 1))
(declare-fun stack_s ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) Int (_ BitVec 6)) (_ BitVec 1))
(declare-fun sc_s (Int) (_ BitVec 6))
(declare-fun instr (Int) Int)
(declare-fun a (Int) (_ BitVec 1))
(assert
(forall ((x_0 (_ BitVec 1)) (x_SLOAD_0 (_ BitVec 1)) (|10| (_ BitVec 1)) )(let (($x13 (<= k 206)))
(let ((?x2037 (used_gas_t x_0 x_SLOAD_0 |10| k)))
(let ((?x2038 (used_gas_s x_0 x_SLOAD_0 |10| 3)))
(let (($x2045 (forall ((w (_ BitVec 1)) )(let ((?x2043 (storage_s x_0 x_SLOAD_0 |10| 3 w)))
(= ?x2043 (storage_t x_0 x_SLOAD_0 |10| k w))))
))
(let (($x27 (exc_halt_t k)))
(let (($x28 (exc_halt_s 3)))
(let (($x29 (= $x28 $x27)))
(let (($x3153 (forall ((n (_ BitVec 6)) )(let ((?x2048 (stack_s x_0 x_SLOAD_0 |10| 3 n)))
(let (($x2049 (= ?x2048 (stack_t x_0 x_SLOAD_0 |10| k n))))
(or $x2049 (bvsle (sc_t k) n)))))
))
(let ((?x35 (sc_t k)))
(let ((?x45 (sc_s 3)))
(let (($x46 (= ?x45 ?x35)))
(let ((?x2055 (used_gas_s x_0 x_SLOAD_0 |10| 0)))
(let (($x2056 (= ?x2055 (used_gas_t x_0 x_SLOAD_0 |10| 0))))
(let (($x2061 (forall ((w (_ BitVec 1)) )(let ((?x2059 (storage_s x_0 x_SLOAD_0 |10| 0 w)))
(= ?x2059 (storage_t x_0 x_SLOAD_0 |10| 0 w))))
))
(let (($x60 (exc_halt_t 0)))
(let (($x61 (exc_halt_s 0)))
(let (($x62 (= $x61 $x60)))
(let (($x3338 (forall ((n (_ BitVec 6)) )(let ((?x2064 (stack_s x_0 x_SLOAD_0 |10| 0 n)))
(let (($x2065 (= ?x2064 (stack_t x_0 x_SLOAD_0 |10| 0 n))))
(or $x2065 (bvsle (sc_t 0) n)))))
))
(let ((?x67 (sc_t 0)))
(let ((?x76 (sc_s 0)))
(let (($x77 (= ?x76 ?x67)))
(let (($x1021 (>= k 0)))
(let (($x3503 (forall ((j Int) )(let ((?x1030 (instr j)))
(let (($x1031 (= ?x1030 55)))
(let (($x1032 (= ?x1030 54)))
(let (($x1033 (= ?x1030 53)))
(let (($x1034 (= ?x1030 52)))
(let (($x1035 (= ?x1030 51)))
(let (($x1036 (= ?x1030 50)))
(let (($x1037 (= ?x1030 49)))
(let (($x1038 (= ?x1030 48)))
(let (($x1039 (= ?x1030 47)))
(let (($x1040 (= ?x1030 46)))
(let (($x1041 (= ?x1030 45)))
(let (($x1042 (= ?x1030 44)))
(let (($x1043 (= ?x1030 43)))
(let (($x1044 (= ?x1030 42)))
(let (($x1045 (= ?x1030 41)))
(let (($x1046 (= ?x1030 40)))
(let (($x1047 (= ?x1030 39)))
(let (($x1048 (= ?x1030 38)))
(let (($x1049 (= ?x1030 37)))
(let (($x1050 (= ?x1030 36)))
(let (($x1051 (= ?x1030 35)))
(let (($x1052 (= ?x1030 34)))
(let (($x1053 (= ?x1030 33)))
(let (($x1054 (= ?x1030 32)))
(let (($x1055 (= ?x1030 31)))
(let (($x1056 (= ?x1030 30)))
(let (($x1057 (= ?x1030 29)))
(let (($x1058 (= ?x1030 28)))
(let (($x1059 (= ?x1030 27)))
(let (($x1060 (= ?x1030 26)))
(let (($x1061 (= ?x1030 25)))
(let (($x1062 (= ?x1030 24)))
(let (($x1063 (= ?x1030 23)))
(let (($x1064 (= ?x1030 22)))
(let (($x1065 (= ?x1030 21)))
(let (($x1066 (= ?x1030 20)))
(let (($x1067 (= ?x1030 19)))
(let (($x1068 (= ?x1030 18)))
(let (($x1069 (= ?x1030 17)))
(let (($x1070 (= ?x1030 16)))
(let (($x1071 (= ?x1030 15)))
(let (($x1072 (= ?x1030 14)))
(let (($x1073 (= ?x1030 13)))
(let (($x1074 (= ?x1030 12)))
(let (($x1075 (= ?x1030 11)))
(let (($x1076 (= ?x1030 10)))
(let (($x1077 (= ?x1030 9)))
(let (($x1078 (= ?x1030 8)))
(let (($x1079 (= ?x1030 7)))
(let (($x1080 (= ?x1030 6)))
(let (($x1081 (= ?x1030 5)))
(let (($x1082 (= ?x1030 4)))
(let (($x1083 (= ?x1030 3)))
(let (($x1084 (= ?x1030 2)))
(let (($x1085 (= ?x1030 1)))
(let (($x1086 (= ?x1030 0)))
(let (($x1087 (or $x1086 $x1085 $x1084 $x1083 $x1082 $x1081 $x1080 $x1079 $x1078 $x1077 $x1076 $x1075 $x1074 $x1073 $x1072 $x1071 $x1070 $x1069 $x1068 $x1067 $x1066 $x1065 $x1064 $x1063 $x1062 $x1061 $x1060 $x1059 $x1058 $x1057 $x1056 $x1055 $x1054 $x1053 $x1052 $x1051 $x1050 $x1049 $x1048 $x1047 $x1046 $x1045 $x1044 $x1043 $x1042 $x1041 $x1040 $x1039 $x1038 $x1037 $x1036 $x1035 $x1034 $x1033 $x1032 $x1031)))
(let (($x3037 (not (= ((_ extract 6 6) (bvadd (_ bv1 7) (concat (_ bv0 1) (sc_t j)))) (_ bv0 1)))))
(let (($x1095 (exc_halt_t j)))
(let ((?x2805 (+ 1 j)))
(let (($x2833 (exc_halt_t ?x2805)))
(let (($x3039 (= $x2833 (or $x1095 $x3037))))
(let (($x2831 (forall ((w (_ BitVec 1)) )(let ((?x2073 (storage_t x_0 x_SLOAD_0 |10| j w)))
(let ((?x2826 (+ 1 j)))
(let ((?x2825 (storage_t x_0 x_SLOAD_0 |10| ?x2826 w)))
(= ?x2825 ?x2073)))))
))
(let (($x3033 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or (bvsle (sc_t j) n) $x2828))))
))
(let ((?x2806 (sc_t ?x2805)))
(let (($x3029 (= ?x2806 (bvadd (_ bv1 6) (sc_t j)))))
(let ((?x2818 (used_gas_t x_0 x_SLOAD_0 |10| ?x2805)))
(let (($x2820 (= ?x2818 (+ 3 (used_gas_t x_0 x_SLOAD_0 |10| j)))))
(let (($x3496 (and (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 (sc_t j)) |10|) $x2820 $x3029 $x3033 $x2831 $x3039)))
(let (($x3353 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv48 6) (sc_t j)) n)))))
))
(let ((?x1088 (sc_t j)))
(let ((?x2811 (bvadd (_ bv63 6) ?x1088)))
(let ((?x2812 (stack_t x_0 x_SLOAD_0 |10| j ?x2811)))
(let (($x3384 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x2811) ?x2812)))
(let ((?x2814 (bvadd (_ bv62 6) ?x1088)))
(let ((?x2815 (stack_t x_0 x_SLOAD_0 |10| j ?x2814)))
(let (($x3391 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x2814) ?x2815)))
(let ((?x2884 (bvadd (_ bv61 6) ?x1088)))
(let ((?x2885 (stack_t x_0 x_SLOAD_0 |10| j ?x2884)))
(let (($x3398 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x2884) ?x2885)))
(let ((?x3064 (bvadd (_ bv60 6) ?x1088)))
(let ((?x3065 (stack_t x_0 x_SLOAD_0 |10| j ?x3064)))
(let (($x3405 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3064) ?x3065)))
(let ((?x3087 (bvadd (_ bv59 6) ?x1088)))
(let ((?x3088 (stack_t x_0 x_SLOAD_0 |10| j ?x3087)))
(let (($x3412 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3087) ?x3088)))
(let ((?x3110 (bvadd (_ bv58 6) ?x1088)))
(let ((?x3111 (stack_t x_0 x_SLOAD_0 |10| j ?x3110)))
(let (($x3419 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3110) ?x3111)))
(let ((?x3133 (bvadd (_ bv57 6) ?x1088)))
(let ((?x3134 (stack_t x_0 x_SLOAD_0 |10| j ?x3133)))
(let (($x3426 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3133) ?x3134)))
(let ((?x3156 (bvadd (_ bv56 6) ?x1088)))
(let ((?x3157 (stack_t x_0 x_SLOAD_0 |10| j ?x3156)))
(let (($x3433 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3156) ?x3157)))
(let ((?x3179 (bvadd (_ bv55 6) ?x1088)))
(let ((?x3180 (stack_t x_0 x_SLOAD_0 |10| j ?x3179)))
(let (($x3440 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3179) ?x3180)))
(let ((?x3202 (bvadd (_ bv54 6) ?x1088)))
(let ((?x3203 (stack_t x_0 x_SLOAD_0 |10| j ?x3202)))
(let (($x3447 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3202) ?x3203)))
(let ((?x3225 (bvadd (_ bv53 6) ?x1088)))
(let ((?x3226 (stack_t x_0 x_SLOAD_0 |10| j ?x3225)))
(let (($x3454 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3225) ?x3226)))
(let ((?x3248 (bvadd (_ bv52 6) ?x1088)))
(let ((?x3249 (stack_t x_0 x_SLOAD_0 |10| j ?x3248)))
(let (($x3461 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3248) ?x3249)))
(let ((?x3271 (bvadd (_ bv51 6) ?x1088)))
(let ((?x3272 (stack_t x_0 x_SLOAD_0 |10| j ?x3271)))
(let (($x3468 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3271) ?x3272)))
(let ((?x3294 (bvadd (_ bv50 6) ?x1088)))
(let ((?x3295 (stack_t x_0 x_SLOAD_0 |10| j ?x3294)))
(let (($x3475 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3294) ?x3295)))
(let ((?x3317 (bvadd (_ bv49 6) ?x1088)))
(let ((?x3318 (stack_t x_0 x_SLOAD_0 |10| j ?x3317)))
(let (($x3482 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3317) ?x3318)))
(let ((?x3340 (bvadd (_ bv48 6) ?x1088)))
(let ((?x3341 (stack_t x_0 x_SLOAD_0 |10| j ?x3340)))
(let ((?x2809 (stack_t x_0 x_SLOAD_0 |10| ?x2805 (bvadd (_ bv63 6) ?x2806))))
(let (($x3342 (= ?x2809 ?x3341)))
(let (($x3492 (and $x3342 (= (stack_t x_0 x_SLOAD_0 |10| ?x2805 ?x3340) ?x3341) $x3482 $x3475 $x3468 $x3461 $x3454 $x3447 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3353 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3340)) $x3037)))))
(let (($x3330 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv49 6) (sc_t j)) n)))))
))
(let (($x3319 (= ?x2809 ?x3318)))
(let (($x3485 (and $x3319 $x3482 $x3475 $x3468 $x3461 $x3454 $x3447 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3330 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3317)) $x3037)))))
(let (($x3307 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv50 6) (sc_t j)) n)))))
))
(let (($x3296 (= ?x2809 ?x3295)))
(let (($x3478 (and $x3296 $x3475 $x3468 $x3461 $x3454 $x3447 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3307 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3294)) $x3037)))))
(let (($x3284 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv51 6) (sc_t j)) n)))))
))
(let (($x3273 (= ?x2809 ?x3272)))
(let (($x3471 (and $x3273 $x3468 $x3461 $x3454 $x3447 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3284 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3271)) $x3037)))))
(let (($x3261 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv52 6) (sc_t j)) n)))))
))
(let (($x3250 (= ?x2809 ?x3249)))
(let (($x3464 (and $x3250 $x3461 $x3454 $x3447 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3261 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3248)) $x3037)))))
(let (($x3238 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv53 6) (sc_t j)) n)))))
))
(let (($x3227 (= ?x2809 ?x3226)))
(let (($x3457 (and $x3227 $x3454 $x3447 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3238 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3225)) $x3037)))))
(let (($x3215 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv54 6) (sc_t j)) n)))))
))
(let (($x3204 (= ?x2809 ?x3203)))
(let (($x3450 (and $x3204 $x3447 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3215 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3202)) $x3037)))))
(let (($x3192 (forall ((n (_ BitVec 6)) )(let ((?x2077 (stack_t x_0 x_SLOAD_0 |10| j n)))
(let (($x2828 (= (stack_t x_0 x_SLOAD_0 |10| (+ 1 j) n) ?x2077)))
(or $x2828 (bvsle (bvadd (_ bv55 6) (sc_t j)) n)))))
))
(let (($x3181 (= ?x2809 ?x3180)))
(let (($x3443 (and $x3181 $x3440 $x3433 $x3426 $x3419 $x3412 $x3405 $x3398 $x3391 $x3384 $x2820 $x3029 $x3192 $x2831 (= $x2833 (or $x1095 (not (bvsle (_ bv0 6) ?x3179)) $x3037)))))