path: root/test/regress/regress0/quantifiers/javafe.ast.StmtVec.009.smt2

(set-logic AUFLIA)
(set-info :source | 
  Simplify front end test suite.
  This benchmark was translated by Michal Moskal.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun after_133.8_133.8 () Int)
(declare-fun integralOr (Int Int) Int)
(declare-fun els_81.27 () Int)
(declare-fun arrayShapeMore (Int Int) Int)
(declare-fun count_150.3 () Int)
(declare-fun tmp0_cor_166.15 () Int)
(declare-fun tmp1_elements_179.1 () Int)
(declare-fun integralAnd (Int Int) Int)
(declare-fun T_.TYPE () Int)
(declare-fun EC_167.11_167.11 () Int)
(declare-fun EC_178.11_178.11 () Int)
(declare-fun elements_83.6 () Int)
(declare-fun currentStackBottom_pre_19.87.33 () Int)
(declare-fun index_164.36 () Int)
(declare-fun intFirst () Int)
(declare-fun after_113.8_113.8 () Int)
(declare-fun elementType_pre_19.43.27 () Int)
(declare-fun eClosedTime (Int) Int)
(declare-fun int_m9223372036854775808 () Int)
(declare-fun RES_167.11_167.11 () Int)
(declare-fun RES_121.14_121.14 () Int)
(declare-fun int_m2147483648 () Int)
(declare-fun T_java.lang.Comparable () Int)
(declare-fun EC_81.32_81.32 () Int)
(declare-fun arrayPosition (Int) Int)
(declare-fun after_81.32_81.32 () Int)
(declare-fun RES_91.29_91.29 () Int)
(declare-fun EC_169.20_169.20 () Int)
(declare-fun after_151.3_151.3_19.296.17 () Int)
(declare-fun select1 (Int Int) Int)
(declare-fun select2 (Int Int Int) Int)
(declare-fun T_java.util.EscjavaKeyValue () Int)
(declare-fun cnt_91.24 () Int)
(declare-fun elems_1_ () Int)
(declare-fun owner_84.18 () Int)
(declare-fun T_long () Int)
(declare-fun T_javafe.util.StackVector () Int)
(declare-fun count_123.8 () Int)
(declare-fun lockLE (Int Int) Bool)
(declare-fun classLiteral (Int) Int)
(declare-fun after_86.8_86.8_9.342.17 () Int)
(declare-fun elements_61.33 () Int)
(declare-fun count_82.6 () Int)
(declare-fun T_java.lang.RuntimeException () Int)
(declare-fun RES_147.12_147.12 () Int)
(declare-fun lockLT (Int Int) Bool)
(declare-fun elems_2_ () Int)
(declare-fun RES_107.8_107.8 () Int)
(declare-fun elements_zero () Int)
(declare-fun T_float () Int)
(declare-fun elements_19.72.21 () Int)
(declare-fun alloc () Int)
(declare-fun RES_122.18_122.18 () Int)
(declare-fun asChild (Int Int) Int)
(declare-fun CONCVARSYM (Int) Int)
(declare-fun T_int () Int)
(declare-fun int_2147483647 () Int)
(declare-fun elementCount_pre_19.79.33 () Int)
(declare-fun int_9223372036854775807 () Int)
(declare-fun this () Int)
(declare-fun T_byte () Int)
(declare-fun T_java.lang.System () Int)
(declare-fun store1 (Int Int Int) Int)
(declare-fun store2 (Int Int Int Int) Int)
(declare-fun RES_148.13_148.13 () Int)
(declare-fun elementType_12.65.27 () Int)
(declare-fun owner_pre_4.35.28 () Int)
(declare-fun containsNull_12.70.29 () Int)
(declare-fun elements_pre_19.72.21 () Int)
(declare-fun max (Int) Int)
(declare-fun currentStackBottom_19.87.33 () Int)
(declare-fun T_java.util.List () Int)
(declare-fun objectToBeConstructed () Int)
(declare-fun T_java.util.Map () Int)
(declare-fun elementData_10.79.35 () Int)
(declare-fun EC_91.29_91.29 () Int)
(declare-fun integralDiv (Int Int) Int)
(declare-fun after_151.3_151.3_19.298.17 () Int)
(declare-fun T_java.util.AbstractCollection () Int)
(declare-fun elems_86.8_9.342.17 () Int)
(declare-fun T_java.lang.Class () Int)
(declare-fun obj_169.20_169.20_23.30.38 () Int)
(declare-fun after_151.3_151.3_19.298.31 () Int)
(declare-fun vectorCount_19.97.33 () Int)
(declare-fun T_java.lang.Object () Int)
(declare-fun tmp1_elements_84.9 () Int)
(declare-fun tmp1_cond_92.36 () Int)
(declare-fun RES_178.11_178.11 () Int)
(declare-fun tmp3_elements_86.25 () Int)
(declare-fun longLast () Int)
(declare-fun termConditional (Int Int Int) Int)
(declare-fun vectorCount_151.3_19.296.17 () Int)
(declare-fun elements_92.6 () Int)
(declare-fun T_java.util.Dictionary () Int)
(declare-fun vec_120.38 () Int)
(declare-fun elements_pre_61.33 () Int)
(declare-fun bool_false () Int)
(declare-fun Smt.true () Int)
(declare-fun EC_149.3_149.3 () Int)
(declare-fun asLockSet (Int) Int)
(declare-fun integralMod (Int Int) Int)
(declare-fun count_67.33_1_ () Int)
(declare-fun Smt.false () Int)
(declare-fun typeof (Int) Int)
(declare-fun int_18446744073709551615 () Int)
(declare-fun owner_4.35.28 () Int)
(declare-fun count_112.35 () Int)
(declare-fun elementCount_pre_10.90.35 () Int)
(declare-fun x_175.40 () Int)
(declare-fun stringCat (Int Int) Int)
(declare-fun T_java.util.Vector () Int)
(declare-fun tmp0_cor_177.5 () Int)
(declare-fun T_boolean () Int)
(declare-fun longFirst () Int)
(declare-fun T_java.util.Hashtable () Int)
(declare-fun T_java.util.Properties () Int)
(declare-fun after_91.29_91.29 () Int)
(declare-fun arrayFresh (Int Int Int Int Int Int Int) Bool)
(declare-fun tmp0_new_Stmt___92.17 () Int)
(declare-fun RES () Int)
(declare-fun EC_86.8_86.8 () Int)
(declare-fun count_95.6 () Int)
(declare-fun EC_107.8_107.8 () Int)
(declare-fun elementCount_19.79.33 () Int)
(declare-fun after_107.8_107.8 () Int)
(declare-fun intLast () Int)
(declare-fun arrayType () Int)
(declare-fun boolEq (Int Int) Bool)
(declare-fun arrayLength (Int) Int)
(declare-fun cast (Int Int) Int)
(declare-fun tmp0_cor_166.5 () Int)
(declare-fun asElems (Int) Int)
(declare-fun s_145.71 () Int)
(declare-fun T_char () Int)
(declare-fun RES_133.8_133.8 () Int)
(declare-fun owner_93.18 () Int)
(declare-fun dst_149.3_149.3_19.228.40 () Int)
(declare-fun count_pre_67.33 () Int)
(declare-fun elementType_pre_12.65.27 () Int)
(declare-fun T_javafe.ast.ASTNode () Int)
(declare-fun ecThrow () Int)
(declare-fun elementCount_151.3_19.298.17 () Int)
(declare-fun divides (Int Int) Int)
(declare-fun RES_113.8_113.8 () Int)
(declare-fun length_86.8_86.8_9.360.44 () Int)
(declare-fun anArray_124.5_124.5_10.188.45 () Int)
(declare-fun elementType_19.43.27 () Int)
(declare-fun T_javafe.util.Assert () Int)
(declare-fun InRange (Int Int) Bool)
(declare-fun count_67.33 () Int)
(declare-fun RES_81.32_81.32 () Int)
(declare-fun tmp0_cor_177.15 () Int)
(declare-fun elems_149.3_19.225.17 () Int)
(declare-fun tmp2_elements_93.9 () Int)
(declare-fun elementData_pre_10.79.35 () Int)
(declare-fun refEQ (Int Int) Int)
(declare-fun after_149.3_149.3_19.225.17 () Int)
(declare-fun is (Int Int) Int)
(declare-fun index_175.48 () Int)
(declare-fun vectorCount_pre_19.97.33 () Int)
(declare-fun integralEQ (Int Int) Int)
(declare-fun T_java.lang.ArrayIndexOutOfBoundsException () Int)
(declare-fun containsNull_pre_12.70.29 () Int)
(declare-fun boolNE (Int Int) Bool)
(declare-fun isNewArray (Int) Int)
(declare-fun elems_pre () Int)
(declare-fun T_javafe.ast.Stmt () Int)
(declare-fun intShiftL (Int Int) Int)
(declare-fun nonnullelements (Int Int) Bool)
(declare-fun T_java.util.AbstractList () Int)
(declare-fun elementCount_10.90.35 () Int)
(declare-fun multiply (Int Int) Int)
(declare-fun integralGE (Int Int) Int)
(declare-fun T_short () Int)
(declare-fun EC_151.3_151.3 () Int)
(declare-fun alloc_pre () Int)
(declare-fun integralGT (Int Int) Int)
(declare-fun EC () Int)
(declare-fun elements_61.33_1_ () Int)
(declare-fun EC_121.14_121.14 () Int)
(declare-fun boolAnd (Int Int) Bool)
(declare-fun EC_113.8_113.8 () Int)
(declare-fun T_java.util.Collection () Int)
(declare-fun arrayShapeOne (Int) Int)
(declare-fun T_double () Int)
(declare-fun longShiftL (Int Int) Int)
(declare-fun T_java.io.Serializable () Int)
(declare-fun boolOr (Int Int) Bool)
(declare-fun int_4294967295 () Int)
(declare-fun modulo (Int Int) Int)
(declare-fun EC_124.5_124.5 () Int)
(declare-fun T_java.lang.StringBuffer () Int)
(declare-fun after_122.18_122.18 () Int)
(declare-fun EC_147.12_147.12 () Int)
(declare-fun null () Int)
(declare-fun T_java.lang.Exception () Int)
(declare-fun T_java.lang.Throwable () Int)
(declare-fun currentStackBottom_151.3_19.298.31 () Int)
(declare-fun T_java.lang.String () Int)
(declare-fun EC_122.18_122.18 () Int)
(declare-fun asField (Int Int) Int)
(declare-fun after_148.13_148.13 () Int)
(declare-fun T_javafe.ast.StmtVec () Int)
(declare-fun T_java.lang.IndexOutOfBoundsException () Int)
(declare-fun boolImplies (Int Int) Bool)
(declare-fun integralLE (Int Int) Int)
(declare-fun RES_1_ () Int)
(declare-fun integralLT (Int Int) Int)
(declare-fun vAllocTime (Int) Int)
(declare-fun EC_148.13_148.13 () Int)
(declare-fun T_java.lang.Cloneable () Int)
(declare-fun boolNot (Int) Bool)
(declare-fun refNE (Int Int) Int)
(declare-fun integralXor (Int Int) Int)
(declare-fun classDown (Int Int) Int)
(declare-fun els_132.38 () Int)
(declare-fun integralNE (Int Int) Int)
(declare-fun arrayParent (Int) Int)
(declare-fun elemtype (Int) Int)
(declare-fun fClosedTime (Int) Int)
(declare-fun alloc_1_ () Int)
(declare-fun array (Int) Int)
(declare-fun LS () Int)
(declare-fun ecReturn () Int)
(declare-fun isAllocated (Int Int) Bool)
(declare-fun after_167.11_167.11 () Int)
(declare-fun after_178.11_178.11 () Int)
(declare-fun elems () Int)
(declare-fun subtypes (Int Int) Bool)
(declare-fun tmp0_new_Stmt___83.17 () Int)
(declare-fun EC_133.8_133.8 () Int)
(assert (subtypes T_java.lang.Exception T_java.lang.Throwable))
(assert (= T_java.lang.Exception (asChild T_java.lang.Exception T_java.lang.Throwable)))
(assert (subtypes T_javafe.ast.Stmt T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.Stmt (asChild T_javafe.ast.Stmt T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.util.Assert T_java.lang.Object))
(assert (= T_javafe.util.Assert (asChild T_javafe.util.Assert T_java.lang.Object)))
(assert (subtypes T_java.util.Properties T_java.util.Hashtable))
(assert (= T_java.util.Properties (asChild T_java.util.Properties T_java.util.Hashtable)))
(assert (subtypes T_java.lang.Cloneable T_java.lang.Object))
(assert (subtypes T_java.lang.IndexOutOfBoundsException T_java.lang.RuntimeException))
(assert (= T_java.lang.IndexOutOfBoundsException (asChild T_java.lang.IndexOutOfBoundsException T_java.lang.RuntimeException)))
(assert (subtypes T_java.util.Dictionary T_java.lang.Object))
(assert (= T_java.util.Dictionary (asChild T_java.util.Dictionary T_java.lang.Object)))
(assert (subtypes T_java.util.Dictionary T_java.util.EscjavaKeyValue))
(assert (subtypes T_java.lang.ArrayIndexOutOfBoundsException T_java.lang.IndexOutOfBoundsException))
(assert (= T_java.lang.ArrayIndexOutOfBoundsException (asChild T_java.lang.ArrayIndexOutOfBoundsException T_java.lang.IndexOutOfBoundsException)))
(assert (subtypes T_java.util.Map T_java.lang.Object))
(assert (subtypes T_java.util.Map T_java.util.EscjavaKeyValue))
(assert (subtypes T_java.io.Serializable T_java.lang.Object))
(assert (subtypes T_java.lang.StringBuffer T_java.lang.Object))
(assert (= T_java.lang.StringBuffer (asChild T_java.lang.StringBuffer T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.StringBuffer) (= ?t T_java.lang.StringBuffer)) :pattern ((subtypes ?t T_java.lang.StringBuffer)) )))
(assert (subtypes T_java.lang.StringBuffer T_java.io.Serializable))
(assert (subtypes T_javafe.ast.StmtVec T_java.lang.Object))
(assert (= T_javafe.ast.StmtVec (asChild T_javafe.ast.StmtVec T_java.lang.Object)))
(assert (subtypes T_java.util.AbstractCollection T_java.lang.Object))
(assert (= T_java.util.AbstractCollection (asChild T_java.util.AbstractCollection T_java.lang.Object)))
(assert (subtypes T_java.util.AbstractCollection T_java.util.Collection))
(assert (subtypes T_java.util.Vector T_java.util.AbstractList))
(assert (= T_java.util.Vector (asChild T_java.util.Vector T_java.util.AbstractList)))
(assert (subtypes T_java.util.Vector T_java.util.List))
(assert (subtypes T_java.util.Vector T_java.lang.Cloneable))
(assert (subtypes T_java.util.Vector T_java.io.Serializable))
(assert (subtypes T_java.util.Hashtable T_java.util.Dictionary))
(assert (= T_java.util.Hashtable (asChild T_java.util.Hashtable T_java.util.Dictionary)))
(assert (subtypes T_java.util.Hashtable T_java.util.Map))
(assert (subtypes T_java.util.Hashtable T_java.lang.Cloneable))
(assert (subtypes T_java.util.Hashtable T_java.io.Serializable))
(assert (subtypes T_java.lang.System T_java.lang.Object))
(assert (= T_java.lang.System (asChild T_java.lang.System T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.System) (= ?t T_java.lang.System)) :pattern ((subtypes ?t T_java.lang.System)) )))
(assert (subtypes T_javafe.util.StackVector T_java.lang.Object))
(assert (= T_javafe.util.StackVector (asChild T_javafe.util.StackVector T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_javafe.util.StackVector) (= ?t T_javafe.util.StackVector)) :pattern ((subtypes ?t T_javafe.util.StackVector)) )))
(assert (subtypes T_java.lang.String T_java.lang.Object))
(assert (= T_java.lang.String (asChild T_java.lang.String T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.String) (= ?t T_java.lang.String)) :pattern ((subtypes ?t T_java.lang.String)) )))
(assert (subtypes T_java.lang.String T_java.io.Serializable))
(assert (subtypes T_java.lang.String T_java.lang.Comparable))
(assert (subtypes T_java.util.AbstractList T_java.util.AbstractCollection))
(assert (= T_java.util.AbstractList (asChild T_java.util.AbstractList T_java.util.AbstractCollection)))
(assert (subtypes T_java.util.AbstractList T_java.util.List))
(assert (subtypes T_java.util.List T_java.lang.Object))
(assert (subtypes T_java.util.List T_java.util.Collection))
(assert (subtypes T_java.lang.Throwable T_java.lang.Object))
(assert (= T_java.lang.Throwable (asChild T_java.lang.Throwable T_java.lang.Object)))
(assert (subtypes T_java.lang.Throwable T_java.io.Serializable))
(assert (subtypes T_java.util.Collection T_java.lang.Object))
(assert (subtypes T_java.lang.RuntimeException T_java.lang.Exception))
(assert (= T_java.lang.RuntimeException (asChild T_java.lang.RuntimeException T_java.lang.Exception)))
(assert (subtypes T_java.util.EscjavaKeyValue T_java.lang.Object))
(assert (subtypes T_java.lang.Comparable T_java.lang.Object))
(assert (subtypes T_javafe.ast.ASTNode T_java.lang.Object))
(assert (= T_javafe.ast.ASTNode (asChild T_javafe.ast.ASTNode T_java.lang.Object)))
(assert (subtypes T_javafe.ast.ASTNode T_java.lang.Cloneable))
(assert (distinct arrayType T_boolean T_char T_byte T_short T_int T_long T_float T_double T_.TYPE T_java.lang.Exception T_javafe.ast.Stmt T_javafe.util.Assert T_java.util.Properties T_java.lang.Cloneable T_java.lang.IndexOutOfBoundsException T_java.util.Dictionary T_java.lang.ArrayIndexOutOfBoundsException T_java.util.Map T_java.io.Serializable T_java.lang.StringBuffer T_javafe.ast.StmtVec T_java.util.AbstractCollection T_java.util.Vector T_java.util.Hashtable T_java.lang.System T_javafe.util.StackVector T_java.lang.String T_java.lang.Object T_java.util.AbstractList T_java.util.List T_java.lang.Throwable T_java.util.Collection T_java.lang.RuntimeException T_java.util.EscjavaKeyValue T_java.lang.Comparable T_javafe.ast.ASTNode))
(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 63)) (<= 1 (longShiftL 1 ?n))) :pattern ((longShiftL 1 ?n)) )))
(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 31)) (<= 1 (intShiftL 1 ?n))) :pattern ((intShiftL 1 ?n)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (and (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralXor ?x ?y))) :pattern ((integralXor ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralDiv ?x ?y))) (=> (and (<= 0 ?x) (< 0 ?y)) (and (<= 0 ?v_0) (<= ?v_0 ?x)))) :pattern ((integralDiv ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralOr ?x ?y))) (=> (and (<= 0 ?x) (<= 0 ?y)) (and (<= ?x ?v_0) (<= ?y ?v_0)))) :pattern ((integralOr ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?y) (<= (integralAnd ?x ?y) ?y)) :pattern ((integralAnd ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?x) (<= (integralAnd ?x ?y) ?x)) :pattern ((integralAnd ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (or (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralAnd ?x ?y))) :pattern ((integralAnd ?x ?y)) )))
(assert (forall ((?t Int)) (! (let ((?v_0 (classLiteral ?t))) (and (not (= ?v_0 null)) (= Smt.true (is ?v_0 T_java.lang.Class)) (isAllocated ?v_0 alloc))) :pattern ((classLiteral ?t)) )))
(assert (forall ((?x Int) (?e Int)) (= (nonnullelements ?x ?e) (and (not (= ?x null)) (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i (arrayLength ?x))) (not (= (select1 (select1 ?e ?x) ?i) null))))))))
(assert (forall ((?b Int) (?x Int) (?y Int)) (! (=> (not (= ?b Smt.true)) (= (termConditional ?b ?x ?y) ?y)) :pattern ((termConditional ?b ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (termConditional Smt.true ?x ?y) ?x) :pattern ((termConditional Smt.true ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (refNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((refNE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (refEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((refEQ ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((integralNE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLT ?x ?y) Smt.true) (< ?x ?y)) :pattern ((integralLT ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLE ?x ?y) Smt.true) (<= ?x ?y)) :pattern ((integralLE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGT ?x ?y) Smt.true) (> ?x ?y)) :pattern ((integralGT ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGE ?x ?y) Smt.true) (>= ?x ?y)) :pattern ((integralGE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (stringCat ?x ?y))) (and (not (= ?v_0 null)) (subtypes (typeof ?v_0) T_java.lang.String))) :pattern ((stringCat ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((integralEQ ?x ?y)) )))
(assert (forall ((?a Int) (?b Int)) (= (boolOr ?a ?b) (or (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?a Int)) (= (boolNot ?a) (not (= ?a Smt.true)))))
(assert (forall ((?a Int) (?b Int)) (= (boolNE ?a ?b) (not (= (= ?a Smt.true) (= ?b Smt.true))))))
(assert (forall ((?a Int) (?b Int)) (= (boolImplies ?a ?b) (=> (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?a Int) (?b Int)) (= (boolEq ?a ?b) (= (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?a Int) (?b Int)) (= (boolAnd ?a ?b) (and (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (multiply ?x ?y))) (= (multiply (integralDiv ?v_0 ?y) ?y) ?v_0))))
(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?j ?i) ?j) (integralMod ?i ?j))))
(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?i ?j) ?j) (integralMod ?i ?j))))
(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< ?j 0) (and (< ?j ?v_0) (<= ?v_0 0)))) :pattern ((integralMod ?i ?j)) )))
(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< 0 ?j) (and (<= 0 ?v_0) (< ?v_0 ?j)))) :pattern ((integralMod ?i ?j)) )))
(assert (forall ((?i Int) (?j Int)) (! (= (+ (multiply (integralDiv ?i ?j) ?j) (integralMod ?i ?j)) ?i) :pattern ((integralMod ?i ?j))  :pattern ((integralDiv ?i ?j)) )))
(assert (forall ((?s Int)) (! (=> (= Smt.true (isNewArray ?s)) (subtypes (typeof ?s) arrayType)) :pattern ((isNewArray ?s)) )))
(assert (forall ((?t Int)) (! (subtypes (array ?t) arrayType) :pattern ((array ?t)) )))
(assert (= arrayType (asChild arrayType T_java.lang.Object)))
(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (= (select1 (select1 ?e ?a) ?i) ?v) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v)) )))
(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?s Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (let ((?v_0 (select1 (select1 ?e ?a) ?i))) (and (arrayFresh ?v_0 ?a0 ?b0 ?e ?s (elemtype ?T) ?v) (= (arrayParent ?v_0) ?a) (= (arrayPosition ?v_0) ?i))) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v)) )))
(assert (forall ((?a Int)) (! (let ((?v_0 (arrayLength ?a))) (and (<= 0 ?v_0) (= Smt.true (is ?v_0 T_int)))) :pattern ((arrayLength ?a)) )))
(assert (forall ((?x Int)) (! (=> (subtypes (typeof ?x) T_java.lang.Object) (lockLE null ?x)) :pattern ((lockLE null ?x))  :pattern ((lockLT null ?x))  :pattern ((lockLE ?x null))  :pattern ((lockLT ?x null)) )))
(assert (forall ((?S Int) (?mu Int)) (let ((?v_0 (asLockSet ?S))) (=> (= (select1 ?v_0 ?mu) Smt.true) (lockLE ?mu (max ?v_0))))))
(assert (forall ((?x Int) (?y Int)) (= (lockLT ?x ?y) (< ?x ?y))))
(assert (forall ((?x Int) (?y Int)) (= (lockLE ?x ?y) (<= ?x ?y))))
(assert (forall ((?S Int)) (! (= (select1 (asLockSet ?S) null) Smt.true) :pattern ((asLockSet ?S)) )))
(assert (forall ((?S Int)) (let ((?v_0 (asLockSet ?S))) (= (select1 ?v_0 (max ?v_0)) Smt.true))))
(assert (forall ((?a Int) (?e Int) (?i Int) (?a0 Int)) (! (=> (and (< (eClosedTime ?e) ?a0) (isAllocated ?a ?a0)) (isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) :pattern ((isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) )))
(assert (forall ((?x Int) (?f Int) (?a0 Int)) (! (=> (and (< (fClosedTime ?f) ?a0) (isAllocated ?x ?a0)) (isAllocated (select1 ?f ?x) ?a0)) :pattern ((isAllocated (select1 ?f ?x) ?a0)) )))
(assert (forall ((?x Int) (?a0 Int)) (= (isAllocated ?x ?a0) (< (vAllocTime ?x) ?a0))))
(assert (forall ((?e Int) (?a Int) (?i Int)) (! (= Smt.true (is (select1 (select1 (asElems ?e) ?a) ?i) (elemtype (typeof ?a)))) :pattern ((select1 (select1 (asElems ?e) ?a) ?i)) )))
(assert (forall ((?f Int) (?t Int) (?x Int)) (! (= Smt.true (is (select1 (asField ?f ?t) ?x) ?t)) :pattern ((select1 (asField ?f ?t) ?x)) )))
(assert (forall ((?x Int) (?t Int)) (! (=> (subtypes ?t T_java.lang.Object) (= (= Smt.true (is ?x ?t)) (or (= ?x null) (subtypes (typeof ?x) ?t)))) :pattern ((subtypes ?t T_java.lang.Object) (is ?x ?t)) )))
(assert (< intLast longLast))
(assert (< 1000000 intLast))
(assert (< intFirst (- 1000000)))
(assert (< longFirst intFirst))
(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_long)) (and (<= longFirst ?x) (<= ?x longLast))) :pattern ((is ?x T_long)) )))
(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_int)) (and (<= intFirst ?x) (<= ?x intLast))) :pattern ((is ?x T_int)) )))
(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_short)) (and (<= (- 32768) ?x) (<= ?x 32767)))))
(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_byte)) (and (<= (- 128) ?x) (<= ?x 127)))))
(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_char)) (and (<= 0 ?x) (<= ?x 65535))) :pattern ((is ?x T_char)) )))
(assert (distinct bool_false Smt.true))
(assert (forall ((?x Int) (?t Int)) (! (=> (= Smt.true (is ?x ?t)) (= (cast ?x ?t) ?x)) :pattern ((cast ?x ?t)) )))
(assert (forall ((?x Int) (?t Int)) (! (= Smt.true (is (cast ?x ?t) ?t)) :pattern ((cast ?x ?t)) )))
(assert (forall ((?t0 Int) (?t1 Int)) (! (let ((?v_0 (elemtype ?t0))) (= (subtypes ?t0 (array ?t1)) (and (= ?t0 (array ?v_0)) (subtypes ?v_0 ?t1)))) :pattern ((subtypes ?t0 (array ?t1))) )))
(assert (forall ((?t Int)) (! (= (elemtype (array ?t)) ?t) :pattern ((elemtype (array ?t))) )))
(assert (forall ((?t Int)) (! (subtypes (array ?t) T_java.lang.Cloneable) :pattern ((array ?t)) )))
(assert (subtypes T_java.lang.Cloneable T_java.lang.Object))
(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (let ((?v_0 (asChild ?t1 ?t2))) (=> (subtypes ?t0 ?v_0) (= (classDown ?t2 ?t0) ?v_0)))))
(assert (forall ((?t Int)) (! (=> (subtypes T_double ?t) (= ?t T_double)) :pattern ((subtypes T_double ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_float ?t) (= ?t T_float)) :pattern ((subtypes T_float ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_long ?t) (= ?t T_long)) :pattern ((subtypes T_long ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_int ?t) (= ?t T_int)) :pattern ((subtypes T_int ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_short ?t) (= ?t T_short)) :pattern ((subtypes T_short ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_byte ?t) (= ?t T_byte)) :pattern ((subtypes T_byte ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_char ?t) (= ?t T_char)) :pattern ((subtypes T_char ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_boolean ?t) (= ?t T_boolean)) :pattern ((subtypes T_boolean ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_double) (= ?t T_double)) :pattern ((subtypes ?t T_double)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_float) (= ?t T_float)) :pattern ((subtypes ?t T_float)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_long) (= ?t T_long)) :pattern ((subtypes ?t T_long)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_int) (= ?t T_int)) :pattern ((subtypes ?t T_int)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_short) (= ?t T_short)) :pattern ((subtypes ?t T_short)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_byte) (= ?t T_byte)) :pattern ((subtypes ?t T_byte)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_char) (= ?t T_char)) :pattern ((subtypes ?t T_char)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_boolean) (= ?t T_boolean)) :pattern ((subtypes ?t T_boolean)) )))
(assert (forall ((?t0 Int) (?t1 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) (= ?t0 ?t1)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) )))
(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) (subtypes ?t0 ?t2)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) )))
(assert (subtypes T_java.lang.Object T_java.lang.Object))
(assert (forall ((?t Int)) (! (subtypes ?t ?t) :pattern ((subtypes ?t ?t)) )))
(assert (forall ((?m Int) (?i Int) (?j Int) (?x Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?m ?i ?x) ?j) (select1 ?m ?j)))))
(assert (forall ((?m Int) (?i Int) (?x Int)) (= (select1 (store1 ?m ?i ?x) ?i) ?x)))
(assert (let ((?v_0 (array T_java.lang.Object)) (?v_6 (<= 0 index_175.48)) (?v_2 (select1 count_67.33 this)) (?v_1 (< index_175.48 0)) (?v_3 (= Smt.true Smt.true))) (let ((?v_8 (or (and ?v_1 ?v_3 (= tmp0_cor_177.15 Smt.true)) (and (not ?v_1) (= tmp0_cor_177.5 (integralGE index_175.48 ?v_2)) (= tmp0_cor_177.15 tmp0_cor_177.5)))) (?v_5 (= Smt.true tmp0_cor_177.15)) (?v_12 (< alloc after_178.11_178.11)) (?v_4 (not (= RES_178.11_178.11 null))) (?v_13 (not (isAllocated RES_178.11_178.11 alloc))) (?v_14 (= Smt.true (is RES_178.11_178.11 T_java.lang.ArrayIndexOutOfBoundsException))) (?v_15 (isAllocated RES_178.11_178.11 after_178.11_178.11)) (?v_16 (= EC_178.11_178.11 ecReturn)) (?v_17 (= (select1 owner_4.35.28 RES_178.11_178.11) null)) (?v_18 (= (typeof RES_178.11_178.11) T_java.lang.ArrayIndexOutOfBoundsException))) (let ((?v_9 (not ?v_5)) (?v_10 (= tmp1_elements_179.1 (select1 elements_61.33 this))) (?v_7 (< index_175.48 (arrayLength tmp1_elements_179.1))) (?v_11 (= Smt.true (is x_175.40 (elemtype (typeof tmp1_elements_179.1))))) (?v_19 (= EC ecReturn))) (not (=> (distinct ecReturn ecThrow) (=> (and (= elementCount_pre_19.79.33 elementCount_19.79.33) (= elementCount_19.79.33 (asField elementCount_19.79.33 T_int)) (= elementData_pre_10.79.35 elementData_10.79.35) (= elementData_10.79.35 (asField elementData_10.79.35 ?v_0)) (< (fClosedTime elementData_10.79.35) alloc) (forall ((?s Int)) (=> (not (= ?s null)) (not (= (select1 elementData_10.79.35 ?s) null)))) (= count_pre_67.33 count_67.33) (= count_67.33 (asField count_67.33 T_int)) (= owner_pre_4.35.28 owner_4.35.28) (= owner_4.35.28 (asField owner_4.35.28 T_java.lang.Object)) (< (fClosedTime owner_4.35.28) alloc) (= elementType_pre_19.43.27 elementType_19.43.27) (= elementType_19.43.27 (asField elementType_19.43.27 T_.TYPE)) (= containsNull_pre_12.70.29 containsNull_12.70.29) (= containsNull_12.70.29 (asField containsNull_12.70.29 T_boolean)) (= elements_pre_19.72.21 elements_19.72.21) (= elements_19.72.21 (asField elements_19.72.21 ?v_0)) (< (fClosedTime elements_19.72.21) alloc) (= elements_pre_61.33 elements_61.33) (= elements_61.33 (asField elements_61.33 (array T_javafe.ast.Stmt))) (< (fClosedTime elements_61.33) alloc) (forall ((?s_1_ Int)) (=> (not (= ?s_1_ null)) (not (= (select1 elements_61.33 ?s_1_) null)))) (= elementType_pre_12.65.27 elementType_12.65.27) (= elementType_12.65.27 (asField elementType_12.65.27 T_.TYPE)) (= elementCount_pre_10.90.35 elementCount_10.90.35) (= elementCount_10.90.35 (asField elementCount_10.90.35 T_int)) (= currentStackBottom_pre_19.87.33 currentStackBottom_19.87.33) (= currentStackBottom_19.87.33 (asField currentStackBottom_19.87.33 T_int)) (= vectorCount_pre_19.97.33 vectorCount_19.97.33) (= vectorCount_19.97.33 (asField vectorCount_19.97.33 T_int)) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= Smt.true (is this T_javafe.ast.StmtVec)) (isAllocated this alloc) (not (= this null)) (= Smt.true (is x_175.40 T_javafe.ast.Stmt)) (isAllocated x_175.40 alloc) (= Smt.true (is index_175.48 T_int)) ?v_6 (< index_175.48 ?v_2) (not (= x_175.40 null)) (forall ((?brokenObj Int)) (=> (and (= Smt.true (is ?brokenObj T_javafe.ast.StmtVec)) (not (= ?brokenObj null))) (forall ((?i_62.31 Int)) (=> (and (<= 0 ?i_62.31) (< ?i_62.31 (select1 count_67.33 ?brokenObj))) (not (= (select1 (select1 elems (select1 elements_61.33 ?brokenObj)) ?i_62.31) null)))))) (forall ((?brokenObj_1_ Int)) (=> (and (= Smt.true (is ?brokenObj_1_ T_javafe.ast.StmtVec)) (not (= ?brokenObj_1_ null))) (<= (select1 count_67.33 ?brokenObj_1_) (arrayLength (select1 elements_61.33 ?brokenObj_1_))))) (forall ((?brokenObj_2_ Int)) (=> (and (= Smt.true (is ?brokenObj_2_ T_javafe.ast.StmtVec)) (not (= ?brokenObj_2_ null))) (<= 0 (select1 count_67.33 ?brokenObj_2_)))) (forall ((?brokenObj_3_ Int)) (=> (and (= Smt.true (is ?brokenObj_3_ T_javafe.ast.StmtVec)) (not (= ?brokenObj_3_ null))) (= (select1 owner_4.35.28 (select1 elements_61.33 ?brokenObj_3_)) ?brokenObj_3_))) (forall ((?brokenObj_4_ Int)) (=> (and (= Smt.true (is ?brokenObj_4_ T_javafe.ast.StmtVec)) (not (= ?brokenObj_4_ null))) (= (typeof (select1 elements_61.33 ?brokenObj_4_)) (array T_javafe.ast.Stmt)))) (or (and ?v_8 (or (and ?v_5 ?v_3 ?v_12 ?v_4 ?v_13 ?v_14 ?v_15 ?v_16 ?v_17 ?v_18 (not ?v_4)) (and ?v_9 ?v_3 ?v_10 (or (not ?v_6) (and ?v_6 (or (not ?v_7) (and ?v_7 (not ?v_11)))))))) (and (or (and ?v_8 ?v_9 ?v_3 ?v_10 ?v_6 ?v_7 ?v_11 (= elems_1_ (store1 elems tmp1_elements_179.1 (store1 (select1 elems tmp1_elements_179.1) index_175.48 x_175.40))) (= elems_2_ elems_1_) ?v_19 (= alloc_1_ alloc)) (and ?v_8 ?v_5 ?v_3 ?v_12 ?v_4 ?v_13 ?v_14 ?v_15 ?v_16 ?v_17 ?v_18 ?v_4 ?v_3 (= elems_2_ elems) (= EC ecThrow) (= alloc_1_ after_178.11_178.11))) (or (not ?v_19) (and ?v_19 (not (forall ((?brokenObj Int)) (=> (and (= Smt.true (is ?brokenObj T_javafe.ast.StmtVec)) (isAllocated ?brokenObj alloc_1_) (not (= ?brokenObj null))) (forall ((?i_62.31 Int)) (=> (and (<= 0 ?i_62.31) (< ?i_62.31 (select1 count_67.33 ?brokenObj))) (not (= (select1 (select1 elems_2_ (select1 elements_61.33 ?brokenObj)) ?i_62.31) null))))))))))))))))))))
(check-sat)
(exit)