path: root/test/regress/regress1/quantifiers/smtlib46f14a.smt2

(set-logic AUFLIRA)
(set-info :source |http://proval.lri.fr/why-benchmarks |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort Unit 0)
(declare-sort c_unique 0)
(declare-sort c_ssorted 0)
(declare-sort c_type 0)
(declare-sort c_Boolean 0)
(declare-fun c_sort (c_type c_unique) c_ssorted)
(declare-fun c_Boolean_true () c_Boolean)
(declare-fun c_Boolean_false () c_Boolean)
(assert (forall ((?b_22_1 c_Boolean)) (or (= c_Boolean_true ?b_22_1) (= c_Boolean_false ?b_22_1))))
(assert (not (= c_Boolean_true c_Boolean_false)))
(declare-fun int2U (Int) c_unique)
(declare-fun ss2Int (c_ssorted) Int)
(declare-fun real2U (Real) c_unique)
(declare-fun ss2Real (c_ssorted) Real)
(declare-fun bool2U (c_Boolean) c_unique)
(declare-fun ss2Bool (c_ssorted) c_Boolean)
(declare-fun c_int () c_type)
(declare-fun c_bool () c_type)
(declare-fun c_real () c_type)
(declare-fun c_unit () c_type)
(declare-fun c_ref (c_unique) c_unique)
(assert (forall ((?t_21_2 c_type)) (forall ((?x_20_3 c_unique)) (forall ((?y_19_4 c_unique)) (=> (= (c_sort ?t_21_2 ?x_20_3) (c_sort ?t_21_2 ?y_19_4)) (= ?x_20_3 ?y_19_4))))))
(assert (forall ((?x_18_5 Int)) (= (ss2Int (c_sort c_int (int2U ?x_18_5))) ?x_18_5)))
(assert (forall ((?x_17_6 Int)) (forall ((?y_16_7 Int)) (=> (= (int2U ?x_17_6) (int2U ?y_16_7)) (= ?x_17_6 ?y_16_7)))))
(assert (forall ((?x_15_8 Real)) (forall ((?y_14_9 Real)) (=> (= (real2U ?x_15_8) (real2U ?y_14_9)) (= ?x_15_8 ?y_14_9)))))
(assert (forall ((?x_13_10 c_Boolean)) (forall ((?y_12_11 c_Boolean)) (=> (= (bool2U ?x_13_10) (bool2U ?y_12_11)) (= ?x_13_10 ?y_12_11)))))
(assert (forall ((?x_11_12 c_ssorted)) (forall ((?y_10_13 c_ssorted)) (=> (= (ss2Int ?x_11_12) (ss2Int ?y_10_13)) (= ?x_11_12 ?y_10_13)))))
(assert (forall ((?x_9_14 c_ssorted)) (forall ((?y_8_15 c_ssorted)) (=> (= (ss2Real ?x_9_14) (ss2Real ?y_8_15)) (= ?x_9_14 ?y_8_15)))))
(assert (forall ((?x_7_16 c_ssorted)) (forall ((?y_6_17 c_ssorted)) (=> (= (ss2Bool ?x_7_16) (ss2Bool ?y_6_17)) (= ?x_7_16 ?y_6_17)))))
(assert (forall ((?x_5_18 Real)) (= (ss2Real (c_sort c_real (real2U ?x_5_18))) ?x_5_18)))
(assert (forall ((?x_4_19 c_Boolean)) (= (ss2Bool (c_sort c_bool (bool2U ?x_4_19))) ?x_4_19)))
(assert (forall ((?x_3_20 c_unique)) (= (int2U (ss2Int (c_sort c_int ?x_3_20))) ?x_3_20)))
(assert (forall ((?x_2_21 c_unique)) (= (real2U (ss2Real (c_sort c_real ?x_2_21))) ?x_2_21)))
(assert (forall ((?x_1_22 c_unique)) (= (bool2U (ss2Bool (c_sort c_bool ?x_1_22))) ?x_1_22)))
(declare-fun eq_int (Int Int) Bool)
(declare-fun neq_int (Int Int) Bool)
(declare-fun lt_int_bool (Int Int) c_Boolean)
(declare-fun le_int_bool (Int Int) c_Boolean)
(declare-fun gt_int_bool (Int Int) c_Boolean)
(declare-fun ge_int_bool (Int Int) c_Boolean)
(declare-fun eq_int_bool (Int Int) c_Boolean)
(declare-fun neq_int_bool (Int Int) c_Boolean)
(assert (forall ((?x_40_23 Int)) (forall ((?y_39_24 Int)) (= (= (lt_int_bool ?x_40_23 ?y_39_24) c_Boolean_true) (< ?x_40_23 ?y_39_24)))))
(assert (forall ((?x_42_25 Int)) (forall ((?y_41_26 Int)) (= (= (le_int_bool ?x_42_25 ?y_41_26) c_Boolean_true) (<= ?x_42_25 ?y_41_26)))))
(assert (forall ((?x_44_27 Int)) (forall ((?y_43_28 Int)) (= (= (gt_int_bool ?x_44_27 ?y_43_28) c_Boolean_true) (> ?x_44_27 ?y_43_28)))))
(assert (forall ((?x_46_29 Int)) (forall ((?y_45_30 Int)) (= (= (ge_int_bool ?x_46_29 ?y_45_30) c_Boolean_true) (>= ?x_46_29 ?y_45_30)))))
(assert (forall ((?x_48_31 Int)) (forall ((?y_47_32 Int)) (= (= (eq_int_bool ?x_48_31 ?y_47_32) c_Boolean_true) (= ?x_48_31 ?y_47_32)))))
(assert (forall ((?x_50_33 Int)) (forall ((?y_49_34 Int)) (= (= (neq_int_bool ?x_50_33 ?y_49_34) c_Boolean_true) (not (= ?x_50_33 ?y_49_34))))))
(declare-fun add_real (Real Real) Real)
(declare-fun sub_real (Real Real) Real)
(declare-fun mul_real (Real Real) Real)
(declare-fun div_real (Real Real) Real)
(declare-fun pow_real (Real Real) Real)
(declare-fun neg_real (Real) Real)
(declare-fun abs_real (Real) Real)
(declare-fun sqrt_real (Real) Real)
(declare-fun real_of_int (Int) Real)
(declare-fun int_of_real (Real) Int)
(declare-fun lt_real (Real Real) Bool)
(declare-fun le_real (Real Real) Bool)
(declare-fun gt_real (Real Real) Bool)
(declare-fun ge_real (Real Real) Bool)
(declare-fun eq_real (Real Real) Bool)
(declare-fun neq_real (Real Real) Bool)
(declare-fun eq_bool (c_Boolean c_Boolean) Bool)
(declare-fun neq_bool (c_Boolean c_Boolean) Bool)
(declare-fun eq_unit (c_ssorted c_ssorted) Bool)
(declare-fun neq_unit (c_ssorted c_ssorted) Bool)
(declare-fun smtlib__ite (c_Boolean c_ssorted c_ssorted) c_unique)
(assert (forall ((?t_1_76_35 c_type)) (forall ((?x_75_36 c_unique)) (forall ((?y_74_37 c_unique)) (= (smtlib__ite c_Boolean_true (c_sort ?t_1_76_35 ?x_75_36) (c_sort ?t_1_76_35 ?y_74_37)) ?x_75_36)))))
(assert (forall ((?t_2_79_38 c_type)) (forall ((?x_78_39 c_unique)) (forall ((?y_77_40 c_unique)) (= (smtlib__ite c_Boolean_false (c_sort ?t_2_79_38 ?x_78_39) (c_sort ?t_2_79_38 ?y_77_40)) ?y_77_40)))))
(declare-fun bw_compl (Int) Int)
(declare-fun bw_and (Int Int) Int)
(declare-fun bw_xor (Int Int) Int)
(declare-fun bw_or (Int Int) Int)
(declare-fun lsl (Int Int) Int)
(declare-fun lsr (Int Int) Int)
(declare-fun non_int (Int) Int)
(declare-fun type_pointer (c_type) c_type)
(declare-fun type_addr (c_type) c_type)
(declare-fun type_alloc_table () c_type)
(declare-fun block_length (c_ssorted c_ssorted) Int)
(declare-fun base_addr (c_ssorted) c_unique)
(declare-fun offset (c_ssorted) Int)
(declare-fun shift (c_ssorted Int) c_unique)
(declare-fun sub_pointer (c_ssorted c_ssorted) Int)
(declare-fun lt_pointer (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_3_88_41 c_type)) (forall ((?p1_87_42 c_unique)) (forall ((?p2_86_43 c_unique)) (let ((?v_0 (type_pointer ?t_3_88_41))) (let ((?v_1 (c_sort ?v_0 ?p1_87_42)) (?v_2 (c_sort ?v_0 ?p2_86_43))) (= (lt_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (< (offset ?v_1) (offset ?v_2))))))))))
(declare-fun le_pointer (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_4_91_44 c_type)) (forall ((?p1_90_45 c_unique)) (forall ((?p2_89_46 c_unique)) (let ((?v_0 (type_pointer ?t_4_91_44))) (let ((?v_1 (c_sort ?v_0 ?p1_90_45)) (?v_2 (c_sort ?v_0 ?p2_89_46))) (= (le_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (<= (offset ?v_1) (offset ?v_2))))))))))
(declare-fun gt_pointer (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_5_94_47 c_type)) (forall ((?p1_93_48 c_unique)) (forall ((?p2_92_49 c_unique)) (let ((?v_0 (type_pointer ?t_5_94_47))) (let ((?v_1 (c_sort ?v_0 ?p1_93_48)) (?v_2 (c_sort ?v_0 ?p2_92_49))) (= (gt_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (> (offset ?v_1) (offset ?v_2))))))))))
(declare-fun ge_pointer (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_6_97_50 c_type)) (forall ((?p1_96_51 c_unique)) (forall ((?p2_95_52 c_unique)) (let ((?v_0 (type_pointer ?t_6_97_50))) (let ((?v_1 (c_sort ?v_0 ?p1_96_51)) (?v_2 (c_sort ?v_0 ?p2_95_52))) (= (ge_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (>= (offset ?v_1) (offset ?v_2))))))))))
(declare-fun valid (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_7_104_53 c_type)) (forall ((?a_103_54 c_unique)) (forall ((?p_102_55 c_unique)) (let ((?v_2 (c_sort type_alloc_table ?a_103_54)) (?v_0 (c_sort (type_pointer ?t_7_104_53) ?p_102_55))) (let ((?v_1 (offset ?v_0))) (= (valid ?v_2 ?v_0) (and (<= 0 ?v_1) (< ?v_1 (block_length ?v_2 ?v_0))))))))))
(declare-fun valid_index (c_ssorted c_ssorted Int) Bool)
(assert (forall ((?t_8_108_56 c_type)) (forall ((?a_107_57 c_unique)) (forall ((?p_106_58 c_unique)) (forall ((?i_105_59 Int)) (let ((?v_2 (c_sort type_alloc_table ?a_107_57)) (?v_0 (c_sort (type_pointer ?t_8_108_56) ?p_106_58))) (let ((?v_1 (+ (offset ?v_0) ?i_105_59))) (= (valid_index ?v_2 ?v_0 ?i_105_59) (and (<= 0 ?v_1) (< ?v_1 (block_length ?v_2 ?v_0)))))))))))
(declare-fun valid_range (c_ssorted c_ssorted Int Int) Bool)
(assert (forall ((?t_9_113_60 c_type)) (forall ((?a_112_61 c_unique)) (forall ((?p_111_62 c_unique)) (forall ((?i_110_63 Int)) (forall ((?j_109_64 Int)) (let ((?v_2 (c_sort type_alloc_table ?a_112_61)) (?v_0 (c_sort (type_pointer ?t_9_113_60) ?p_111_62))) (let ((?v_1 (offset ?v_0))) (= (valid_range ?v_2 ?v_0 ?i_110_63 ?j_109_64) (and (<= 0 (+ ?v_1 ?i_110_63)) (< (+ ?v_1 ?j_109_64) (block_length ?v_2 ?v_0))))))))))))
(assert (forall ((?t_10_116_65 c_type)) (forall ((?p_115_66 c_unique)) (forall ((?i_114_67 Int)) (let ((?v_0 (type_pointer ?t_10_116_65))) (let ((?v_1 (c_sort ?v_0 ?p_115_66))) (= (offset (c_sort ?v_0 (shift ?v_1 ?i_114_67))) (+ (offset ?v_1) ?i_114_67))))))))
(assert (forall ((?t_11_118_68 c_type)) (forall ((?p_117_69 c_unique)) (= (shift (c_sort (type_pointer ?t_11_118_68) ?p_117_69) 0) ?p_117_69))))
(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73))))))))))
(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1))))))))
(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2)))))))))
(assert (forall ((?t_15_133_81 c_type)) (forall ((?a_132_82 c_unique)) (forall ((?p1_131_83 c_unique)) (forall ((?p2_130_84 c_unique)) (let ((?v_0 (type_pointer ?t_15_133_81))) (let ((?v_1 (c_sort ?v_0 ?p1_131_83)) (?v_3 (c_sort ?v_0 ?p2_130_84)) (?v_2 (c_sort type_alloc_table ?a_132_82))) (=> (= (base_addr ?v_1) (base_addr ?v_3)) (= (block_length ?v_2 ?v_1) (block_length ?v_2 ?v_3))))))))))
(assert (forall ((?t_16_136_85 c_type)) (forall ((?p1_135_86 c_unique)) (forall ((?p2_134_87 c_unique)) (let ((?v_0 (type_pointer ?t_16_136_85))) (let ((?v_1 (c_sort ?v_0 ?p1_135_86)) (?v_2 (c_sort ?v_0 ?p2_134_87))) (=> (and (= (base_addr ?v_1) (base_addr ?v_2)) (= (offset ?v_1) (offset ?v_2))) (= ?p1_135_86 ?p2_134_87))))))))
(assert (forall ((?t_17_139_88 c_type)) (forall ((?p1_138_89 c_unique)) (forall ((?p2_137_90 c_unique)) (let ((?v_0 (type_pointer ?t_17_139_88))) (let ((?v_1 (c_sort ?v_0 ?p1_138_89)) (?v_2 (c_sort ?v_0 ?p2_137_90))) (=> (= ?p1_138_89 ?p2_137_90) (and (= (base_addr ?v_1) (base_addr ?v_2)) (= (offset ?v_1) (offset ?v_2))))))))))
(assert (forall ((?t_18_144_91 c_type)) (forall ((?p1_143_92 c_unique)) (forall ((?p2_142_93 c_unique)) (forall ((?i_141_94 Int)) (forall ((?j_140_95 Int)) (let ((?v_0 (type_pointer ?t_18_144_91))) (let ((?v_1 (c_sort ?v_0 ?p1_143_92)) (?v_2 (c_sort ?v_0 ?p2_142_93))) (=> (not (= (base_addr ?v_1) (base_addr ?v_2))) (not (= (shift ?v_1 ?i_141_94) (shift ?v_2 ?j_140_95))))))))))))
(assert (forall ((?t_19_149_96 c_type)) (forall ((?p1_148_97 c_unique)) (forall ((?p2_147_98 c_unique)) (forall ((?i_146_99 Int)) (forall ((?j_145_100 Int)) (let ((?v_0 (type_pointer ?t_19_149_96))) (let ((?v_1 (c_sort ?v_0 ?p1_148_97)) (?v_2 (c_sort ?v_0 ?p2_147_98))) (=> (not (= (+ (offset ?v_1) ?i_146_99) (+ (offset ?v_2) ?j_145_100))) (not (= (shift ?v_1 ?i_146_99) (shift ?v_2 ?j_145_100))))))))))))
(assert (forall ((?t_20_154_101 c_type)) (forall ((?p1_153_102 c_unique)) (forall ((?p2_152_103 c_unique)) (forall ((?i_151_104 Int)) (forall ((?j_150_105 Int)) (let ((?v_0 (type_pointer ?t_20_154_101))) (let ((?v_1 (c_sort ?v_0 ?p1_153_102)) (?v_2 (c_sort ?v_0 ?p2_152_103))) (=> (= (base_addr ?v_1) (base_addr ?v_2)) (=> (= (+ (offset ?v_1) ?i_151_104) (+ (offset ?v_2) ?j_150_105)) (= (shift ?v_1 ?i_151_104) (shift ?v_2 ?j_150_105))))))))))))
(assert (forall ((?t_21_158_106 c_type)) (forall ((?a_157_107 c_unique)) (forall ((?p_156_108 c_unique)) (forall ((?i_155_109 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_157_107)) (?v_1 (type_pointer ?t_21_158_106))) (let ((?v_2 (c_sort ?v_1 ?p_156_108))) (=> (valid_index ?v_0 ?v_2 ?i_155_109) (valid ?v_0 (c_sort ?v_1 (shift ?v_2 ?i_155_109)))))))))))
(assert (forall ((?t_22_164_110 c_type)) (forall ((?a_163_111 c_unique)) (forall ((?p_162_112 c_unique)) (forall ((?i_161_113 Int)) (forall ((?j_160_114 Int)) (forall ((?k_159_115 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_163_111)) (?v_1 (type_pointer ?t_22_164_110))) (let ((?v_2 (c_sort ?v_1 ?p_162_112))) (=> (valid_range ?v_0 ?v_2 ?i_161_113 ?j_160_114) (=> (and (<= ?i_161_113 ?k_159_115) (<= ?k_159_115 ?j_160_114)) (valid ?v_0 (c_sort ?v_1 (shift ?v_2 ?k_159_115))))))))))))))
(assert (forall ((?t_23_169_116 c_type)) (forall ((?a_168_117 c_unique)) (forall ((?p_167_118 c_unique)) (forall ((?i_166_119 Int)) (forall ((?j_165_120 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_168_117)) (?v_1 (c_sort (type_pointer ?t_23_169_116) ?p_167_118))) (=> (valid_range ?v_0 ?v_1 ?i_166_119 ?j_165_120) (=> (and (<= ?i_166_119 0) (<= 0 ?j_165_120)) (valid ?v_0 ?v_1))))))))))
(assert (forall ((?t_24_175_121 c_type)) (forall ((?a_174_122 c_unique)) (forall ((?p_173_123 c_unique)) (forall ((?i_172_124 Int)) (forall ((?j_171_125 Int)) (forall ((?k_170_126 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_174_122)) (?v_1 (c_sort (type_pointer ?t_24_175_121) ?p_173_123))) (=> (valid_range ?v_0 ?v_1 ?i_172_124 ?j_171_125) (=> (and (<= ?i_172_124 ?k_170_126) (<= ?k_170_126 ?j_171_125)) (valid_index ?v_0 ?v_1 ?k_170_126)))))))))))
(assert (forall ((?t_25_178_127 c_type)) (forall ((?p1_177_128 c_unique)) (forall ((?p2_176_129 c_unique)) (let ((?v_0 (type_pointer ?t_25_178_127))) (let ((?v_1 (c_sort ?v_0 ?p1_177_128)) (?v_2 (c_sort ?v_0 ?p2_176_129))) (=> (= (base_addr ?v_1) (base_addr ?v_2)) (= (sub_pointer ?v_1 ?v_2) (- (offset ?v_1) (offset ?v_2))))))))))
(declare-fun type_memory (c_type c_type) c_type)
(declare-fun acc (c_ssorted c_ssorted) c_unique)
(declare-fun upd (c_ssorted c_ssorted c_ssorted) c_unique)
(assert (forall ((?t_27_212_130 c_type)) (forall ((?t_26_211_131 c_type)) (forall ((?m_210_132 c_unique)) (forall ((?p_209_133 c_unique)) (forall ((?a_208_134 c_unique)) (let ((?v_0 (type_memory ?t_26_211_131 ?t_27_212_130)) (?v_1 (c_sort (type_pointer ?t_27_212_130) ?p_209_133))) (= (acc (c_sort ?v_0 (upd (c_sort ?v_0 ?m_210_132) ?v_1 (c_sort ?t_26_211_131 ?a_208_134))) ?v_1) ?a_208_134))))))))
(assert (forall ((?t_29_218_135 c_type)) (forall ((?t_28_217_136 c_type)) (forall ((?m_216_137 c_unique)) (forall ((?p1_215_138 c_unique)) (forall ((?p2_214_139 c_unique)) (forall ((?a_213_140 c_unique)) (let ((?v_0 (type_memory ?t_28_217_136 ?t_29_218_135))) (let ((?v_2 (c_sort ?v_0 ?m_216_137)) (?v_1 (type_pointer ?t_29_218_135))) (let ((?v_3 (c_sort ?v_1 ?p2_214_139))) (=> (not (= ?p1_215_138 ?p2_214_139)) (= (acc (c_sort ?v_0 (upd ?v_2 (c_sort ?v_1 ?p1_215_138) (c_sort ?t_28_217_136 ?a_213_140))) ?v_3) (acc ?v_2 ?v_3)))))))))))))
(assert (not (= c_Boolean_false c_Boolean_true)))
(declare-fun type_pset (c_type) c_type)
(declare-fun pset_empty () c_unique)
(declare-fun pset_singleton (c_ssorted) c_unique)
(declare-fun pset_star (c_ssorted c_ssorted) c_unique)
(declare-fun pset_all (c_ssorted) c_unique)
(declare-fun pset_range (c_ssorted Int Int) c_unique)
(declare-fun pset_range_left (c_ssorted Int) c_unique)
(declare-fun pset_range_right (c_ssorted Int) c_unique)
(declare-fun pset_acc_all (c_ssorted c_ssorted) c_unique)
(declare-fun pset_acc_range (c_ssorted c_ssorted Int Int) c_unique)
(declare-fun pset_acc_range_left (c_ssorted c_ssorted Int) c_unique)
(declare-fun pset_acc_range_right (c_ssorted c_ssorted Int) c_unique)
(declare-fun pset_union (c_ssorted c_ssorted) c_unique)
(declare-fun not_in_pset (c_ssorted c_ssorted) Bool)
(declare-fun not_assigns (c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
(assert (forall ((?t_31_225_141 c_type)) (forall ((?t_30_224_142 c_type)) (forall ((?a_223_143 c_unique)) (forall ((?m1_222_144 c_unique)) (forall ((?m2_221_145 c_unique)) (forall ((?l_220_146 c_unique)) (let ((?v_0 (type_memory ?t_30_224_142 ?t_31_225_141))) (= (not_assigns (c_sort type_alloc_table ?a_223_143) (c_sort ?v_0 ?m1_222_144) (c_sort ?v_0 ?m2_221_145) (c_sort (type_pset ?t_31_225_141) ?l_220_146)) (forall ((?p_219_147 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_31_225_141) ?p_219_147))) (=> (valid (c_sort type_alloc_table ?a_223_143) ?v_1) (=> (not_in_pset ?v_1 (c_sort (type_pset ?t_31_225_141) ?l_220_146)) (= (acc (c_sort ?v_0 ?m2_221_145) ?v_1) (acc (c_sort ?v_0 ?m1_222_144) ?v_1)))))))))))))))
(assert (forall ((?t_32_227_148 c_type)) (forall ((?p_226_149 c_unique)) (not_in_pset (c_sort (type_pointer ?t_32_227_148) ?p_226_149) (c_sort (type_pset ?t_32_227_148) pset_empty)))))
(assert (forall ((?t_33_230_150 c_type)) (forall ((?p1_229_151 c_unique)) (forall ((?p2_228_152 c_unique)) (let ((?v_0 (type_pointer ?t_33_230_150))) (=> (not (= ?p1_229_151 ?p2_228_152)) (not_in_pset (c_sort ?v_0 ?p1_229_151) (c_sort (type_pset ?t_33_230_150) (pset_singleton (c_sort ?v_0 ?p2_228_152))))))))))
(assert (forall ((?t_34_233_153 c_type)) (forall ((?p1_232_154 c_unique)) (forall ((?p2_231_155 c_unique)) (let ((?v_0 (type_pointer ?t_34_233_153))) (=> (not_in_pset (c_sort ?v_0 ?p1_232_154) (c_sort (type_pset ?t_34_233_153) (pset_singleton (c_sort ?v_0 ?p2_231_155)))) (not (= ?p1_232_154 ?p2_231_155))))))))
(assert (forall ((?t_35_235_156 c_type)) (forall ((?p_234_157 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_35_235_156) ?p_234_157))) (not (not_in_pset ?v_0 (c_sort (type_pset ?t_35_235_156) (pset_singleton ?v_0))))))))
(assert (forall ((?t_36_239_158 c_type)) (forall ((?l1_238_159 c_unique)) (forall ((?l2_237_160 c_unique)) (forall ((?p_236_161 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_36_239_158) ?p_236_161)) (?v_1 (type_pset ?t_36_239_158))) (let ((?v_2 (c_sort ?v_1 ?l1_238_159)) (?v_3 (c_sort ?v_1 ?l2_237_160))) (=> (and (not_in_pset ?v_0 ?v_2) (not_in_pset ?v_0 ?v_3)) (not_in_pset ?v_0 (c_sort ?v_1 (pset_union ?v_2 ?v_3)))))))))))
(assert (forall ((?t_37_243_162 c_type)) (forall ((?l1_242_163 c_unique)) (forall ((?l2_241_164 c_unique)) (forall ((?p_240_165 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_37_243_162) ?p_240_165)) (?v_0 (type_pset ?t_37_243_162))) (let ((?v_2 (c_sort ?v_0 ?l1_242_163))) (=> (not_in_pset ?v_1 (c_sort ?v_0 (pset_union ?v_2 (c_sort ?v_0 ?l2_241_164)))) (not_in_pset ?v_1 ?v_2)))))))))
(assert (forall ((?t_38_247_166 c_type)) (forall ((?l1_246_167 c_unique)) (forall ((?l2_245_168 c_unique)) (forall ((?p_244_169 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_38_247_166) ?p_244_169)) (?v_0 (type_pset ?t_38_247_166))) (let ((?v_2 (c_sort ?v_0 ?l2_245_168))) (=> (not_in_pset ?v_1 (c_sort ?v_0 (pset_union (c_sort ?v_0 ?l1_246_167) ?v_2))) (not_in_pset ?v_1 ?v_2)))))))))
(assert (forall ((?t_40_253_170 c_type)) (forall ((?t_39_252_171 c_type)) (forall ((?l_251_172 c_unique)) (forall ((?m_250_173 c_unique)) (forall ((?p_249_174 c_unique)) (let ((?v_0 (type_pointer ?t_40_253_170))) (=> (forall ((?p1_248_175 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_39_252_171) ?p1_248_175))) (=> (= ?p_249_174 (acc (c_sort (type_memory ?v_0 ?t_39_252_171) ?m_250_173) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_39_252_171) ?l_251_172))))) (not_in_pset (c_sort ?v_0 ?p_249_174) (c_sort (type_pset ?t_40_253_170) (pset_star (c_sort (type_pset ?t_39_252_171) ?l_251_172) (c_sort (type_memory ?v_0 ?t_39_252_171) ?m_250_173))))))))))))
(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178)))))))))))))
(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184))))))))))
(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2)))))))))))))
(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194)))))))))))
(assert (forall ((?t_46_281_197 c_type)) (forall ((?p_280_198 c_unique)) (forall ((?l_279_199 c_unique)) (forall ((?a_278_200 Int)) (forall ((?b_277_201 Int)) (let ((?v_0 (type_pset ?t_46_281_197))) (=> (not_in_pset (c_sort (type_pointer ?t_46_281_197) ?p_280_198) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_279_199) ?a_278_200 ?b_277_201))) (forall ((?p1_276_202 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_46_281_197) ?p1_276_202) (c_sort ?v_0 ?l_279_199))) (forall ((?i_275_203 Int)) (=> (and (<= ?a_278_200 ?i_275_203) (<= ?i_275_203 ?b_277_201)) (not (= (shift (c_sort (type_pointer ?t_46_281_197) ?p1_276_202) ?i_275_203) ?p_280_198))))))))))))))
(assert (forall ((?t_47_287_204 c_type)) (forall ((?p_286_205 c_unique)) (forall ((?l_285_206 c_unique)) (forall ((?a_284_207 Int)) (let ((?v_0 (type_pset ?t_47_287_204))) (=> (forall ((?p1_283_208 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_47_287_204) ?p1_283_208) (c_sort ?v_0 ?l_285_206)) (forall ((?i_282_209 Int)) (=> (<= ?i_282_209 ?a_284_207) (not (= ?p_286_205 (shift (c_sort (type_pointer ?t_47_287_204) ?p1_283_208) ?i_282_209))))))) (not_in_pset (c_sort (type_pointer ?t_47_287_204) ?p_286_205) (c_sort ?v_0 (pset_range_left (c_sort ?v_0 ?l_285_206) ?a_284_207))))))))))
(assert (forall ((?t_48_293_210 c_type)) (forall ((?p_292_211 c_unique)) (forall ((?l_291_212 c_unique)) (forall ((?a_290_213 Int)) (let ((?v_0 (type_pset ?t_48_293_210))) (=> (not_in_pset (c_sort (type_pointer ?t_48_293_210) ?p_292_211) (c_sort ?v_0 (pset_range_left (c_sort ?v_0 ?l_291_212) ?a_290_213))) (forall ((?p1_289_214 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_48_293_210) ?p1_289_214) (c_sort ?v_0 ?l_291_212))) (forall ((?i_288_215 Int)) (=> (<= ?i_288_215 ?a_290_213) (not (= (shift (c_sort (type_pointer ?t_48_293_210) ?p1_289_214) ?i_288_215) ?p_292_211)))))))))))))
(assert (forall ((?t_49_299_216 c_type)) (forall ((?p_298_217 c_unique)) (forall ((?l_297_218 c_unique)) (forall ((?a_296_219 Int)) (let ((?v_0 (type_pset ?t_49_299_216))) (=> (forall ((?p1_295_220 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_49_299_216) ?p1_295_220) (c_sort ?v_0 ?l_297_218)) (forall ((?i_294_221 Int)) (=> (<= ?a_296_219 ?i_294_221) (not (= ?p_298_217 (shift (c_sort (type_pointer ?t_49_299_216) ?p1_295_220) ?i_294_221))))))) (not_in_pset (c_sort (type_pointer ?t_49_299_216) ?p_298_217) (c_sort ?v_0 (pset_range_right (c_sort ?v_0 ?l_297_218) ?a_296_219))))))))))
(assert (forall ((?t_50_305_222 c_type)) (forall ((?p_304_223 c_unique)) (forall ((?l_303_224 c_unique)) (forall ((?a_302_225 Int)) (let ((?v_0 (type_pset ?t_50_305_222))) (=> (not_in_pset (c_sort (type_pointer ?t_50_305_222) ?p_304_223) (c_sort ?v_0 (pset_range_right (c_sort ?v_0 ?l_303_224) ?a_302_225))) (forall ((?p1_301_226 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_50_305_222) ?p1_301_226) (c_sort ?v_0 ?l_303_224))) (forall ((?i_300_227 Int)) (=> (<= ?a_302_225 ?i_300_227) (not (= (shift (c_sort (type_pointer ?t_50_305_222) ?p1_301_226) ?i_300_227) ?p_304_223)))))))))))))
(assert (forall ((?t_52_312_228 c_type)) (forall ((?t_51_311_229 c_type)) (forall ((?p_310_230 c_unique)) (forall ((?l_309_231 c_unique)) (forall ((?m_308_232 c_unique)) (let ((?v_0 (type_pointer ?t_51_311_229))) (=> (forall ((?p1_307_233 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_52_312_228) ?p1_307_233) (c_sort (type_pset ?t_52_312_228) ?l_309_231))) (forall ((?i_306_234 Int)) (let ((?v_1 (type_pointer ?t_52_312_228))) (not (= ?p_310_230 (acc (c_sort (type_memory ?v_0 ?t_52_312_228) ?m_308_232) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_307_233) ?i_306_234))))))))) (not_in_pset (c_sort ?v_0 ?p_310_230) (c_sort (type_pset ?t_51_311_229) (pset_acc_all (c_sort (type_pset ?t_52_312_228) ?l_309_231) (c_sort (type_memory ?v_0 ?t_52_312_228) ?m_308_232))))))))))))
(assert (forall ((?t_54_319_235 c_type)) (forall ((?t_53_318_236 c_type)) (forall ((?p_317_237 c_unique)) (forall ((?l_316_238 c_unique)) (forall ((?m_315_239 c_unique)) (let ((?v_0 (type_pointer ?t_53_318_236))) (=> (not_in_pset (c_sort ?v_0 ?p_317_237) (c_sort (type_pset ?t_53_318_236) (pset_acc_all (c_sort (type_pset ?t_54_319_235) ?l_316_238) (c_sort (type_memory ?v_0 ?t_54_319_235) ?m_315_239)))) (forall ((?p1_314_240 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_54_319_235) ?p1_314_240) (c_sort (type_pset ?t_54_319_235) ?l_316_238))) (forall ((?i_313_241 Int)) (let ((?v_1 (type_pointer ?t_54_319_235))) (not (= (acc (c_sort (type_memory ?v_0 ?t_54_319_235) ?m_315_239) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_314_240) ?i_313_241))) ?p_317_237))))))))))))))
(assert (forall ((?t_56_328_242 c_type)) (forall ((?t_55_327_243 c_type)) (forall ((?p_326_244 c_unique)) (forall ((?l_325_245 c_unique)) (forall ((?m_324_246 c_unique)) (forall ((?a_323_247 Int)) (forall ((?b_322_248 Int)) (let ((?v_0 (type_pointer ?t_55_327_243))) (=> (forall ((?p1_321_249 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_56_328_242) ?p1_321_249) (c_sort (type_pset ?t_56_328_242) ?l_325_245))) (forall ((?i_320_250 Int)) (let ((?v_1 (type_pointer ?t_56_328_242))) (=> (and (<= ?a_323_247 ?i_320_250) (<= ?i_320_250 ?b_322_248)) (not (= ?p_326_244 (acc (c_sort (type_memory ?v_0 ?t_56_328_242) ?m_324_246) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_321_249) ?i_320_250)))))))))) (not_in_pset (c_sort ?v_0 ?p_326_244) (c_sort (type_pset ?t_55_327_243) (pset_acc_range (c_sort (type_pset ?t_56_328_242) ?l_325_245) (c_sort (type_memory ?v_0 ?t_56_328_242) ?m_324_246) ?a_323_247 ?b_322_248)))))))))))))
(assert (forall ((?t_58_337_251 c_type)) (forall ((?t_57_336_252 c_type)) (forall ((?p_335_253 c_unique)) (forall ((?l_334_254 c_unique)) (forall ((?m_333_255 c_unique)) (forall ((?a_332_256 Int)) (forall ((?b_331_257 Int)) (let ((?v_0 (type_pointer ?t_57_336_252))) (=> (not_in_pset (c_sort ?v_0 ?p_335_253) (c_sort (type_pset ?t_57_336_252) (pset_acc_range (c_sort (type_pset ?t_58_337_251) ?l_334_254) (c_sort (type_memory ?v_0 ?t_58_337_251) ?m_333_255) ?a_332_256 ?b_331_257))) (forall ((?p1_330_258 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_58_337_251) ?p1_330_258) (c_sort (type_pset ?t_58_337_251) ?l_334_254))) (forall ((?i_329_259 Int)) (let ((?v_1 (type_pointer ?t_58_337_251))) (=> (and (<= ?a_332_256 ?i_329_259) (<= ?i_329_259 ?b_331_257)) (not (= (acc (c_sort (type_memory ?v_0 ?t_58_337_251) ?m_333_255) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_330_258) ?i_329_259))) ?p_335_253)))))))))))))))))
(assert (forall ((?t_60_345_260 c_type)) (forall ((?t_59_344_261 c_type)) (forall ((?p_343_262 c_unique)) (forall ((?l_342_263 c_unique)) (forall ((?m_341_264 c_unique)) (forall ((?a_340_265 Int)) (let ((?v_0 (type_pointer ?t_59_344_261))) (=> (forall ((?p1_339_266 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_60_345_260) ?p1_339_266) (c_sort (type_pset ?t_60_345_260) ?l_342_263))) (forall ((?i_338_267 Int)) (let ((?v_1 (type_pointer ?t_60_345_260))) (=> (<= ?i_338_267 ?a_340_265) (not (= ?p_343_262 (acc (c_sort (type_memory ?v_0 ?t_60_345_260) ?m_341_264) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_339_266) ?i_338_267)))))))))) (not_in_pset (c_sort ?v_0 ?p_343_262) (c_sort (type_pset ?t_59_344_261) (pset_acc_range_left (c_sort (type_pset ?t_60_345_260) ?l_342_263) (c_sort (type_memory ?v_0 ?t_60_345_260) ?m_341_264) ?a_340_265))))))))))))
(assert (forall ((?t_62_353_268 c_type)) (forall ((?t_61_352_269 c_type)) (forall ((?p_351_270 c_unique)) (forall ((?l_350_271 c_unique)) (forall ((?m_349_272 c_unique)) (forall ((?a_348_273 Int)) (let ((?v_0 (type_pointer ?t_61_352_269))) (=> (not_in_pset (c_sort ?v_0 ?p_351_270) (c_sort (type_pset ?t_61_352_269) (pset_acc_range_left (c_sort (type_pset ?t_62_353_268) ?l_350_271) (c_sort (type_memory ?v_0 ?t_62_353_268) ?m_349_272) ?a_348_273))) (forall ((?p1_347_274 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_62_353_268) ?p1_347_274) (c_sort (type_pset ?t_62_353_268) ?l_350_271))) (forall ((?i_346_275 Int)) (let ((?v_1 (type_pointer ?t_62_353_268))) (=> (<= ?i_346_275 ?a_348_273) (not (= (acc (c_sort (type_memory ?v_0 ?t_62_353_268) ?m_349_272) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_347_274) ?i_346_275))) ?p_351_270))))))))))))))))
(assert (forall ((?t_64_361_276 c_type)) (forall ((?t_63_360_277 c_type)) (forall ((?p_359_278 c_unique)) (forall ((?l_358_279 c_unique)) (forall ((?m_357_280 c_unique)) (forall ((?a_356_281 Int)) (let ((?v_0 (type_pointer ?t_63_360_277))) (=> (forall ((?p1_355_282 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_64_361_276) ?p1_355_282) (c_sort (type_pset ?t_64_361_276) ?l_358_279))) (forall ((?i_354_283 Int)) (let ((?v_1 (type_pointer ?t_64_361_276))) (=> (<= ?a_356_281 ?i_354_283) (not (= ?p_359_278 (acc (c_sort (type_memory ?v_0 ?t_64_361_276) ?m_357_280) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_355_282) ?i_354_283)))))))))) (not_in_pset (c_sort ?v_0 ?p_359_278) (c_sort (type_pset ?t_63_360_277) (pset_acc_range_right (c_sort (type_pset ?t_64_361_276) ?l_358_279) (c_sort (type_memory ?v_0 ?t_64_361_276) ?m_357_280) ?a_356_281))))))))))))
(assert (forall ((?t_66_369_284 c_type)) (forall ((?t_65_368_285 c_type)) (forall ((?p_367_286 c_unique)) (forall ((?l_366_287 c_unique)) (forall ((?m_365_288 c_unique)) (forall ((?a_364_289 Int)) (let ((?v_0 (type_pointer ?t_65_368_285))) (=> (not_in_pset (c_sort ?v_0 ?p_367_286) (c_sort (type_pset ?t_65_368_285) (pset_acc_range_right (c_sort (type_pset ?t_66_369_284) ?l_366_287) (c_sort (type_memory ?v_0 ?t_66_369_284) ?m_365_288) ?a_364_289))) (forall ((?p1_363_290 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_66_369_284) ?p1_363_290) (c_sort (type_pset ?t_66_369_284) ?l_366_287))) (forall ((?i_362_291 Int)) (let ((?v_1 (type_pointer ?t_66_369_284))) (=> (<= ?a_364_289 ?i_362_291) (not (= (acc (c_sort (type_memory ?v_0 ?t_66_369_284) ?m_365_288) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_363_290) ?i_362_291))) ?p_367_286))))))))))))))))
(assert (forall ((?t_68_376_292 c_type)) (forall ((?t_67_375_293 c_type)) (forall ((?a_374_294 c_unique)) (forall ((?l_373_295 c_unique)) (forall ((?m1_372_296 c_unique)) (forall ((?m2_371_297 c_unique)) (forall ((?m3_370_298 c_unique)) (let ((?v_1 (c_sort type_alloc_table ?a_374_294)) (?v_0 (type_memory ?t_68_376_292 ?t_67_375_293))) (let ((?v_4 (c_sort ?v_0 ?m1_372_296)) (?v_2 (c_sort ?v_0 ?m2_371_297)) (?v_3 (c_sort (type_pset ?t_67_375_293) ?l_373_295)) (?v_5 (c_sort ?v_0 ?m3_370_298))) (=> (not_assigns ?v_1 ?v_4 ?v_2 ?v_3) (=> (not_assigns ?v_1 ?v_2 ?v_5 ?v_3) (not_assigns ?v_1 ?v_4 ?v_5 ?v_3)))))))))))))
(assert (forall ((?t_70_381_299 c_type)) (forall ((?t_69_380_300 c_type)) (forall ((?a_379_301 c_unique)) (forall ((?l_378_302 c_unique)) (forall ((?m_377_303 c_unique)) (let ((?v_0 (c_sort (type_memory ?t_70_381_299 ?t_69_380_300) ?m_377_303))) (not_assigns (c_sort type_alloc_table ?a_379_301) ?v_0 ?v_0 (c_sort (type_pset ?t_69_380_300) ?l_378_302)))))))))
(declare-fun valid_acc (c_ssorted) Bool)
(assert (forall ((?t_72_386_304 c_type)) (forall ((?t_71_385_305 c_type)) (forall ((?m1_384_306 c_unique)) (= (valid_acc (c_sort (type_memory (type_pointer ?t_71_385_305) ?t_72_386_304) ?m1_384_306)) (forall ((?p_383_307 c_unique)) (forall ((?a_382_308 c_unique)) (let ((?v_1 (type_pointer ?t_71_385_305)) (?v_0 (c_sort type_alloc_table ?a_382_308)) (?v_2 (c_sort (type_pointer ?t_72_386_304) ?p_383_307))) (=> (valid ?v_0 ?v_2) (valid ?v_0 (c_sort ?v_1 (acc (c_sort (type_memory ?v_1 ?t_72_386_304) ?m1_384_306) ?v_2))))))))))))
(declare-fun valid_acc_range (c_ssorted Int) Bool)
(assert (forall ((?t_74_392_309 c_type)) (forall ((?t_73_391_310 c_type)) (forall ((?m1_390_311 c_unique)) (forall ((?size_389_312 Int)) (= (valid_acc_range (c_sort (type_memory (type_pointer ?t_73_391_310) ?t_74_392_309) ?m1_390_311) ?size_389_312) (forall ((?p_388_313 c_unique)) (forall ((?a_387_314 c_unique)) (let ((?v_1 (type_pointer ?t_73_391_310)) (?v_0 (c_sort type_alloc_table ?a_387_314)) (?v_2 (c_sort (type_pointer ?t_74_392_309) ?p_388_313))) (=> (valid ?v_0 ?v_2) (valid_range ?v_0 (c_sort ?v_1 (acc (c_sort (type_memory ?v_1 ?t_74_392_309) ?m1_390_311) ?v_2)) 0 (- ?size_389_312 1))))))))))))
(assert (forall ((?t_76_398_315 c_type)) (forall ((?t_75_397_316 c_type)) (forall ((?m1_396_317 c_unique)) (forall ((?size_395_318 Int)) (forall ((?p_394_319 c_unique)) (forall ((?a_393_320 c_unique)) (let ((?v_1 (type_pointer ?t_75_397_316))) (let ((?v_2 (c_sort (type_memory ?v_1 ?t_76_398_315) ?m1_396_317)) (?v_0 (c_sort type_alloc_table ?a_393_320)) (?v_3 (c_sort (type_pointer ?t_76_398_315) ?p_394_319))) (=> (valid_acc_range ?v_2 ?size_395_318) (=> (valid ?v_0 ?v_3) (valid ?v_0 (c_sort ?v_1 (acc ?v_2 ?v_3))))))))))))))
(declare-fun separation1 (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2))))))))))))))))
(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool)
(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3))))))))))))))))))))
(declare-fun separation1_range (c_ssorted Int) Bool)
(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342))))))))))))))))))))))))
(declare-fun separation2 (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348)))))))))))))))))
(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool)
(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355))))))))))))))))))))
(declare-fun on_heap (c_ssorted c_ssorted) Bool)
(declare-fun on_stack (c_ssorted c_ssorted) Bool)
(declare-fun fresh (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_87_438_358 c_type)) (forall ((?a_437_359 c_unique)) (forall ((?p_436_360 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a_437_359)) (?v_1 (c_sort (type_pointer ?t_87_438_358) ?p_436_360))) (=> (fresh ?v_0 ?v_1) (not (valid ?v_0 ?v_1))))))))
(assert (forall ((?t_88_442_361 c_type)) (forall ((?a_441_362 c_unique)) (forall ((?p_440_363 c_unique)) (=> (fresh (c_sort type_alloc_table ?a_441_362) (c_sort (type_pointer ?t_88_442_361) ?p_440_363)) (forall ((?i_439_364 Int)) (let ((?v_0 (type_pointer ?t_88_442_361))) (not (valid (c_sort type_alloc_table ?a_441_362) (c_sort ?v_0 (shift (c_sort ?v_0 ?p_440_363) ?i_439_364)))))))))))
(declare-fun alloc_extends (c_ssorted c_ssorted) Bool)
(assert (forall ((?t_89_446_365 c_type)) (forall ((?a1_445_366 c_unique)) (forall ((?a2_444_367 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_445_366) (c_sort type_alloc_table ?a2_444_367)) (forall ((?q_443_368 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_89_446_365) ?q_443_368))) (=> (valid (c_sort type_alloc_table ?a1_445_366) ?v_0) (valid (c_sort type_alloc_table ?a2_444_367) ?v_0)))))))))
(assert (forall ((?t_90_451_369 c_type)) (forall ((?a1_450_370 c_unique)) (forall ((?a2_449_371 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_450_370) (c_sort type_alloc_table ?a2_449_371)) (forall ((?q_448_372 c_unique)) (forall ((?i_447_373 Int)) (let ((?v_0 (c_sort (type_pointer ?t_90_451_369) ?q_448_372))) (=> (valid_index (c_sort type_alloc_table ?a1_450_370) ?v_0 ?i_447_373) (valid_index (c_sort type_alloc_table ?a2_449_371) ?v_0 ?i_447_373))))))))))
(assert (forall ((?t_91_457_374 c_type)) (forall ((?a1_456_375 c_unique)) (forall ((?a2_455_376 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_456_375) (c_sort type_alloc_table ?a2_455_376)) (forall ((?q_454_377 c_unique)) (forall ((?i_453_378 Int)) (forall ((?j_452_379 Int)) (let ((?v_0 (c_sort (type_pointer ?t_91_457_374) ?q_454_377))) (=> (valid_range (c_sort type_alloc_table ?a1_456_375) ?v_0 ?i_453_378 ?j_452_379) (valid_range (c_sort type_alloc_table ?a2_455_376) ?v_0 ?i_453_378 ?j_452_379)))))))))))
(assert (forall ((?a_458_380 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a_458_380))) (alloc_extends ?v_0 ?v_0))))
(assert (forall ((?a1_461_381 c_unique)) (forall ((?a2_460_382 c_unique)) (forall ((?a3_459_383 c_unique)) (let ((?v_1 (c_sort type_alloc_table ?a1_461_381)) (?v_0 (c_sort type_alloc_table ?a2_460_382)) (?v_2 (c_sort type_alloc_table ?a3_459_383))) (=> (alloc_extends ?v_1 ?v_0) (=> (alloc_extends ?v_0 ?v_2) (alloc_extends ?v_1 ?v_2))))))))
(declare-fun free_stack (c_ssorted c_ssorted c_ssorted) Bool)
(assert (forall ((?t_92_466_384 c_type)) (forall ((?a1_465_385 c_unique)) (forall ((?a2_464_386 c_unique)) (forall ((?a3_463_387 c_unique)) (=> (free_stack (c_sort type_alloc_table ?a1_465_385) (c_sort type_alloc_table ?a2_464_386) (c_sort type_alloc_table ?a3_463_387)) (forall ((?p_462_388 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a2_464_386)) (?v_1 (c_sort (type_pointer ?t_92_466_384) ?p_462_388))) (=> (valid ?v_0 ?v_1) (=> (on_heap ?v_0 ?v_1) (valid (c_sort type_alloc_table ?a3_463_387) ?v_1)))))))))))
(assert (forall ((?t_93_471_389 c_type)) (forall ((?a1_470_390 c_unique)) (forall ((?a2_469_391 c_unique)) (forall ((?a3_468_392 c_unique)) (=> (free_stack (c_sort type_alloc_table ?a1_470_390) (c_sort type_alloc_table ?a2_469_391) (c_sort type_alloc_table ?a3_468_392)) (forall ((?p_467_393 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a1_470_390)) (?v_1 (c_sort (type_pointer ?t_93_471_389) ?p_467_393))) (=> (valid ?v_0 ?v_1) (=> (on_stack ?v_0 ?v_1) (valid (c_sort type_alloc_table ?a3_468_392) ?v_1)))))))))))
(declare-fun null () c_unique)
(assert (forall ((?t_94_475_394 c_type)) (forall ((?a_474_395 c_unique)) (not (valid (c_sort type_alloc_table ?a_474_395) (c_sort (type_pointer ?t_94_475_394) null))))))
(declare-fun type_global () c_type)
(assert (not (forall ((?alloc c_unique)) (forall ((?b Int)) (forall ((?t c_unique)) (=> (and (= ?b 0) (valid_range (c_sort type_alloc_table ?alloc) (c_sort (type_pointer type_global) ?t) 0 9)) (forall ((?b0 Int)) (=> (= ?b0 (+ ?b 1)) (forall ((?result c_unique)) (let ((?v_0 (type_pointer type_global))) (let ((?v_2 (c_sort ?v_0 ?result))) (let ((?v_1 (offset ?v_2))) (=> (= ?result (shift (c_sort ?v_0 ?t) ?b)) (and (<= 0 ?v_1) (< ?v_1 (block_length (c_sort type_alloc_table ?alloc) ?v_2))))))))))))))))
(check-sat)
(exit)