segfault2.smt2

(declare-datatypes ((bytes_tuple 0)) (((bytes_tuple (bytes_tuple_accessor_array (Array Int Int)) (bytes_tuple_accessor_length Int)))))
(declare-datatypes ((tx_type 0)) (((tx_type (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 ((state_type 0)) (((state_type (balances (Array Int Int))))))
(declare-rel block_7_f_56_66_0 (Int Int tx_type state_type Bool Int Int Bool state_type Bool Int Int Bool Int))
(declare-rel implicit_constructor_C_66_0 (Int Int tx_type state_type))
(declare-rel interface_D_6_0 (Int state_type))
(declare-rel summary_constructor_D_6_0 (Int Int tx_type state_type))
(declare-rel summary_constructor_C_66_0 (Int Int tx_type state_type Bool Int Int))
(declare-rel nondet_interface_C_66_0 (state_type Bool Int Int state_type Bool Int Int))
(declare-rel summary_2_function_f__57_66_0 (Int Int tx_type state_type Bool Int Int Bool state_type Bool Int Int Bool))
(declare-rel interface_C_66_0 (Int state_type Bool Int Int))
(declare-rel block_5_g_28_66_0 (Int Int tx_type state_type Bool Int Int state_type Bool Int Int Int))
(declare-rel summary_0_function_d__5_6_0 (Int Int tx_type state_type state_type))
(declare-rel summary_3_function_h__65_66_0 (Int Int tx_type state_type Bool Int Int state_type Bool Int Int))
(declare-rel block_8_function_h__65_66_0 (Int Int tx_type state_type Bool Int Int state_type Bool Int Int))
(declare-rel block_4_function_g__29_66_0 (Int Int tx_type state_type Bool Int Int state_type Bool Int Int Int))
(declare-rel block_9_h_64_66_0 (Int Int tx_type state_type Bool Int Int state_type Bool Int Int))
(declare-rel error_target_2_0 ())
(declare-rel implicit_constructor_D_6_0 (Int Int tx_type state_type))
(declare-rel nondet_interface_D_6_0 (state_type state_type))
(declare-rel block_6_function_f__57_66_0 (Int Int tx_type state_type Bool Int Int Bool state_type Bool Int Int Bool))
(declare-rel summary_1_function_g__29_66_0 (Int Int tx_type state_type Bool Int Int state_type Bool Int Int Int))
(declare-var A state_type)
(declare-var B tx_type)
(declare-var C Int)
(declare-var D state_type)
(declare-var E state_type)
(declare-var F Int)
(declare-var G Bool)
(declare-var H Int)
(declare-var I Int)
(declare-var J Int)
(declare-var K Int)
(declare-var L Int)
(declare-var M Int)
(declare-var N Bool)
(declare-var O Bool)
(declare-var P Int)
(declare-var Q Bool)
(declare-var R Bool)
(declare-var S Int)
(declare-var T Int)
(declare-var U Int)
(declare-var V Int)
(declare-var W Int)
(declare-var X Int)
(declare-var Y Int)
(declare-var Z Bool)
(declare-var A1 Int)
(declare-var B1 Int)
(declare-var C1 Int)
(declare-var D1 Int)
(declare-var E1 Int)
(declare-var F1 Int)
(declare-var G1 Int)
(declare-var H1 Int)
(declare-var I1 Int)
(declare-var J1 Int)
(declare-var K1 Bool)
(declare-var L1 Bool)
(declare-var M1 Bool)
(declare-var N1 Bool)
(declare-var O1 Int)
(declare-var P1 Int)
(declare-var Q1 Int)
(rule (! (nondet_interface_D_6_0 A A) :named base_nondet))
(rule (! (=> (and (nondet_interface_D_6_0 E D) (summary_0_function_d__5_6_0 F C B D A))
    (nondet_interface_D_6_0 E A)) :named nondet_interface_D_6_0_to_nondet_interface_D_6_0))
(rule (! (nondet_interface_C_66_0 A G C F A G C F) :named base_nondet!))
(rule (! (=> (and (nondet_interface_C_66_0 E O H M D N F L)
         (summary_1_function_g__29_66_0 J I B D N F L A G C K P))
    (nondet_interface_C_66_0 E O H M A G C K)) :named nondet_interface_C_66_0_to_nondet_interface_C_66_0))
(rule (! (=> (and (nondet_interface_C_66_0 E R H M D Q F L)
         (summary_2_function_f__57_66_0 J I B D Q F L N A O C K G))
    (nondet_interface_C_66_0 E R H M A O C K)) :named nondet_interface_C_66_0_to_nondet_interface_C_66_0!))
(rule (! (=> (and (nondet_interface_C_66_0 E O H M D N F L)
         (summary_3_function_h__65_66_0 J I B D N F L A G C K))
    (nondet_interface_C_66_0 E O H M A G C K)) :named nondet_interface_C_66_0_to_nondet_interface_C_66_0!!))
(rule (! (summary_0_function_d__5_6_0 F C B D A) :named summary_function_5))
(rule (! (implicit_constructor_D_6_0 0 C B A) :named implicit_constructor_D_6_0!))
(rule (! (=> (implicit_constructor_D_6_0 F C B D) (summary_constructor_D_6_0 F C B A)) :named implicit_constructor_D_6_0_to_summary_constructor_D_6_0))
(rule (! (=> (and (summary_constructor_D_6_0 F C B A) (= F 0)) (interface_D_6_0 C A)) :named summary_constructor_D_6_0_to_interface_D_6_0))
(rule (! (block_4_function_g__29_66_0 I H B D N F K A G C J L) :named block_4_function_g__29_66_0!))
(rule (! (=> (and (block_4_function_g__29_66_0 I H B D N F K A G C J L)
         (= F C)
         (= K J)
         (= D A)
         (= I 0)
         (= N G))
    (block_5_g_28_66_0 I H B D N F K A G C J L)) :named block_4_function_g__29_66_0_to_block_5_g_28_66_0))
(rule (! (=> (and (block_5_g_28_66_0 T J B E O I W D N H V Y)
         (nondet_interface_C_66_0 D N F V A G C U)
         (= P 2)
         (= M P)
         (= F M)
         (= L V)
         (= T 0)
         (= K C)
         (= K X)
         (= Y 0)
         (= S H))
    (summary_1_function_g__29_66_0 T J B E O I W A G C U X)) :named block_5_g_28_66_0_to_summary_1_function_g__29_66_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data B)) 0) 226))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data B)) 1) 23))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data B)) 2) 155))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data B)) 3) 142)))
  (=> (and (summary_1_function_g__29_66_0 I H B D N F K A G C J L)
           (interface_C_66_0 H D N F K)
           (>= (msg.sender B) 0)
           (<= (msg.sender B) 1461501637330902918203684832716283019655932542975)
           (>= (tx.origin B) 0)
           (<= (tx.origin B) 1461501637330902918203684832716283019655932542975)
           (= (msg.sig B) 3793197966)
           a!1
           a!2
           a!3
           a!4
           (>= (block.coinbase B) 0)
           (= I 0)
           (<= (block.coinbase B)
               1461501637330902918203684832716283019655932542975))
      (interface_C_66_0 H A G C J))) :named interface_C_66_0_to_interface_C_66_0))
(rule (! (block_6_function_f__57_66_0 I H B D Q F K N A O C J G) :named block_6_function_f__57_66_0!))
(rule (! (=> (and (block_6_function_f__57_66_0 J I B D Q H L N A O F K G)
         (= H F)
         (= L K)
         (= N G)
         (= D A)
         (= J 0)
         (= Q O))
    (block_7_f_56_66_0 J I B D Q H L N A O F K G C)) :named block_6_function_f__57_66_0_to_block_7_f_56_66_0))
(rule (! (=> (and (block_7_f_56_66_0 T K B E Z J W O D R I V N C)
         (summary_1_function_g__29_66_0 S K B D R H V A Q F U X)
         (= M 1)
         (= L M)
         (= H L)
         (= G N)
         (= C 0)
         (> S 0)
         (= P I))
    (summary_2_function_f__57_66_0 S K B E Z J W O A Q F U N)) :named block_7_f_56_66_0_to_summary_2_function_f__57_66_0))
(rule (! (=> (and (block_7_f_56_66_0 F1 M B E N1 L J1 Z D M1 K I1 R F)
         (summary_1_function_g__29_66_0 E1 M B D M1 J I1 A L1 I H1 P1)
         (= A1 1)
         (= Y A1)
         (= J Y)
         (= Q R)
         (= E1 0)
         (= D1 F1)
         (= X P1)
         (= W 3)
         (= K1 (ite Q L1 M1))
         (= H (ite Q I J))
         (= G1 (ite Q H1 I1))
         (= O1 (ite Q P1 Q1))
         (= V (ite Q X W))
         (= C V)
         (= U H)
         (= T 2)
         (= O (= U T))
         (= S H)
         (= P 1)
         (= N (= S P))
         (= G (or O N))
         (not (= G true))
         (= F 0)
         (= C1 1)
         (= B1 K))
    (summary_2_function_f__57_66_0 C1 M B E N1 L J1 Z A K1 H G1 R)) :named block_7_f_56_66_0_to_summary_2_function_f__57_66_0!))
(rule (! (=> (and (block_7_f_56_66_0 F1 M B E N1 L J1 Z D M1 K I1 R F)
         (summary_1_function_g__29_66_0 E1 M B D M1 J I1 A L1 I H1 P1)
         (= A1 1)
         (= Y A1)
         (= J Y)
         (= Q R)
         (= E1 0)
         (= D1 F1)
         (= X P1)
         (= W 3)
         (= K1 (ite Q L1 M1))
         (= H (ite Q I J))
         (= G1 (ite Q H1 I1))
         (= O1 (ite Q P1 Q1))
         (= V (ite Q X W))
         (= C V)
         (= U H)
         (= T 2)
         (= O (= U T))
         (= S H)
         (= P 1)
         (= N (= S P))
         (= G (or O N))
         (= C1 D1)
         (= F 0)
         (= B1 K))
    (summary_2_function_f__57_66_0 C1 M B E N1 L J1 Z A K1 H G1 R)) :named block_7_f_56_66_0_to_summary_2_function_f__57_66_0!!))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data B)) 0) 152))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data B)) 1) 195))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data B)) 2) 166))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data B)) 3) 193)))
  (=> (and (summary_2_function_f__57_66_0 I H B D Q F K N A O C J G)
           (interface_C_66_0 H D Q F K)
           (>= (msg.sender B) 0)
           (<= (msg.sender B) 1461501637330902918203684832716283019655932542975)
           (>= (tx.origin B) 0)
           (<= (tx.origin B) 1461501637330902918203684832716283019655932542975)
           (= (msg.sig B) 2562959041)
           a!1
           a!2
           a!3
           a!4
           (>= (block.coinbase B) 0)
           (= I 0)
           (<= (block.coinbase B)
               1461501637330902918203684832716283019655932542975))
      (interface_C_66_0 H A O C J))) :named interface_C_66_0_to_interface_C_66_0!))
(rule (! (block_8_function_h__65_66_0 I H B D N F K A G C J) :named block_8_function_h__65_66_0!))
(rule (! (=> (and (block_8_function_h__65_66_0 I H B D N F K A G C J)
         (= F C)
         (= K J)
         (= D A)
         (= I 0)
         (= N G))
    (block_9_h_64_66_0 I H B D N F K A G C J)) :named block_8_function_h__65_66_0_to_block_9_h_64_66_0))
(rule (! (=> (and (block_9_h_64_66_0 M I B D N H S A G F P)
         (= J K)
         (= C J)
         (= L F)
         (= K 3))
    (summary_3_function_h__65_66_0 M I B D N H S A G C P)) :named block_9_h_64_66_0_to_summary_3_function_h__65_66_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data B)) 0) 184))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data B)) 1) 201))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data B)) 2) 211))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data B)) 3) 101)))
  (=> (and (summary_3_function_h__65_66_0 I H B D N F K A G C J)
           (interface_C_66_0 H D N F K)
           (>= (msg.sender B) 0)
           (<= (msg.sender B) 1461501637330902918203684832716283019655932542975)
           (>= (tx.origin B) 0)
           (<= (tx.origin B) 1461501637330902918203684832716283019655932542975)
           (= (msg.sig B) 3100234597)
           a!1
           a!2
           a!3
           a!4
           (>= (block.coinbase B) 0)
           (= I 0)
           (<= (block.coinbase B)
               1461501637330902918203684832716283019655932542975))
      (interface_C_66_0 H A G C J))) :named interface_C_66_0_to_interface_C_66_0!!))
(rule (! (implicit_constructor_C_66_0 0 C B A) :named implicit_constructor_C_66_0!))
(rule (! (=> (and (implicit_constructor_C_66_0 H F B D) (= I 0) (= G false) (= C 0))
    (summary_constructor_C_66_0 H F B A G C I)) :named implicit_constructor_C_66_0_to_summary_constructor_C_66_0))
(rule (! (=> (and (summary_constructor_C_66_0 H F B A G C I) (= H 0))
    (interface_C_66_0 F A G C I)) :named summary_constructor_C_66_0_to_interface_C_66_0))
(rule (! (=> (and (summary_2_function_f__57_66_0 I H B D Q F K N A O C J G)
         (interface_C_66_0 H D Q F K)
         (= I 1))
    error_target_2_0) :named interface_C_66_0_to_error_target_2_0))

(query error_target_2_0 :print-certificate true)