path: root/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2

(set-logic AUFLIA)
(set-info :source | Simplify Theorem Prover Benchmark Suite |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun true_term () Int)
(declare-fun false_term () Int)
(assert (= true_term 1))
(assert (= false_term 0))
(declare-fun S_select (Int Int) Int)
(declare-fun S_store (Int Int Int) Int)
(assert (forall ((?m Int) (?i Int) (?x Int)) (= (S_select (S_store ?m ?i ?x) ?i) ?x)))
(assert (forall ((?m Int) (?i Int) (?j Int) (?x Int)) (=> (not (= ?i ?j)) (= (S_select (S_store ?m ?i ?x) ?j) (S_select ?m ?j)))))
(declare-fun PO_LT (Int Int) Int)
(assert (forall ((?t Int)) (= (PO_LT ?t ?t) true_term)))
(declare-fun T_java_lang_Object () Int)
(assert (= (PO_LT T_java_lang_Object T_java_lang_Object) true_term))
(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (=> (and (= (PO_LT ?t0 ?t1) true_term) (= (PO_LT ?t1 ?t2) true_term)) (= (PO_LT ?t0 ?t2) true_term))))
(assert (forall ((?t0 Int) (?t1 Int)) (=> (and (= (PO_LT ?t0 ?t1) true_term) (= (PO_LT ?t1 ?t0) true_term)) (= ?t0 ?t1))))
(declare-fun T_boolean () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_boolean) true_term) (= ?t T_boolean))))
(declare-fun T_char () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_char) true_term) (= ?t T_char))))
(declare-fun T_byte () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_byte) true_term) (= ?t T_byte))))
(declare-fun T_short () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_short) true_term) (= ?t T_short))))
(declare-fun T_int () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_int) true_term) (= ?t T_int))))
(declare-fun T_long () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_long) true_term) (= ?t T_long))))
(declare-fun T_float () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_float) true_term) (= ?t T_float))))
(declare-fun T_double () Int)
(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_double) true_term) (= ?t T_double))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_boolean ?t) true_term) (= ?t T_boolean))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_char ?t) true_term) (= ?t T_char))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_byte ?t) true_term) (= ?t T_byte))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_short ?t) true_term) (= ?t T_short))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_int ?t) true_term) (= ?t T_int))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_long ?t) true_term) (= ?t T_long))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_float ?t) true_term) (= ?t T_float))))
(assert (forall ((?t Int)) (=> (= (PO_LT T_double ?t) true_term) (= ?t T_double))))
(declare-fun asChild (Int Int) Int)
(declare-fun classDown (Int Int) Int)
(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (let ((?v_0 (asChild ?t1 ?t2))) (=> (= (PO_LT ?t0 ?v_0) true_term) (= (classDown ?t2 ?t0) ?v_0)))))
(declare-fun T_java_lang_Cloneable () Int)
(assert (= (PO_LT T_java_lang_Cloneable T_java_lang_Object) true_term))
(declare-fun array (Int) Int)
(assert (forall ((?t Int)) (= (PO_LT (array ?t) T_java_lang_Cloneable) true_term)))
(declare-fun elemtype (Int) Int)
(assert (forall ((?t Int)) (= (elemtype (array ?t)) ?t)))
(assert (forall ((?t0 Int) (?t1 Int)) (let ((?v_0 (elemtype ?t0))) (= (= (PO_LT ?t0 (array ?t1)) true_term) (and (= ?t0 (array ?v_0)) (= (PO_LT ?v_0 ?t1) true_term))))))
(declare-fun is (Int Int) Int)
(declare-fun cast (Int Int) Int)
(assert (forall ((?x Int) (?t Int)) (= (is (cast ?x ?t) ?t) true_term)))
(assert (forall ((?x Int) (?t Int)) (=> (= (is ?x ?t) true_term) (= (cast ?x ?t) ?x))))
(assert true)
(assert (forall ((?x Int)) (= (= (is ?x T_char) true_term) (and (<= 0 ?x) (<= ?x 65535)))))
(assert (forall ((?x Int)) (= (= (is ?x T_byte) true_term) (and (<= (- 128) ?x) (<= ?x 127)))))
(assert (forall ((?x Int)) (= (= (is ?x T_short) true_term) (and (<= (- 32768) ?x) (<= ?x 32767)))))
(declare-fun intFirst () Int)
(declare-fun intLast () Int)
(assert (forall ((?x Int)) (= (= (is ?x T_int) true_term) (and (<= intFirst ?x) (<= ?x intLast)))))
(declare-fun longFirst () Int)
(declare-fun longLast () Int)
(assert (forall ((?x Int)) (= (= (is ?x T_long) true_term) (and (<= longFirst ?x) (<= ?x longLast)))))
(assert (< longFirst intFirst))
(assert (< intFirst (- 1000000)))
(assert (< 1000000 intLast))
(assert (< intLast longLast))
(declare-fun null () Int)
(declare-fun typeof (Int) Int)
(assert (forall ((?x Int) (?t Int)) (=> (= (PO_LT ?t T_java_lang_Object) true_term) (= (= (is ?x ?t) true_term) (or (= ?x null) (= (PO_LT (typeof ?x) ?t) true_term))))))
(declare-fun asField (Int Int) Int)
(assert (forall ((?f Int) (?t Int) (?x Int)) (= (is (S_select (asField ?f ?t) ?x) ?t) true_term)))
(declare-fun asElems (Int) Int)
(assert (forall ((?e Int) (?a Int) (?i Int)) (= (is (S_select (S_select (asElems ?e) ?a) ?i) (elemtype (typeof ?a))) true_term)))
(declare-fun vAllocTime (Int) Int)
(declare-fun isAllocated (Int Int) Int)
(assert (forall ((?x Int) (?a0 Int)) (= (= (isAllocated ?x ?a0) true_term) (< (vAllocTime ?x) ?a0))))
(declare-fun fClosedTime (Int) Int)
(assert (forall ((?x Int) (?f Int) (?a0 Int)) (=> (and (< (fClosedTime ?f) ?a0) (= (isAllocated ?x ?a0) true_term)) (= (isAllocated (S_select ?f ?x) ?a0) true_term))))
(declare-fun eClosedTime (Int) Int)
(assert (forall ((?a Int) (?e Int) (?i Int) (?a0 Int)) (=> (and (< (eClosedTime ?e) ?a0) (= (isAllocated ?a ?a0) true_term)) (= (isAllocated (S_select (S_select ?e ?a) ?i) ?a0) true_term))))
(declare-fun asLockSet (Int) Int)
(declare-fun max (Int) Int)
(assert (forall ((?S Int)) (let ((?v_0 (asLockSet ?S))) (= (S_select ?v_0 (max ?v_0)) true_term))))
(assert (forall ((?S Int)) (= (S_select (asLockSet ?S) null) true_term)))
(declare-fun lockLE (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (lockLE ?x ?y) true_term) (<= ?x ?y))))
(declare-fun lockLT (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (lockLT ?x ?y) true_term) (< ?x ?y))))
(assert (forall ((?S Int) (?mu Int)) (let ((?v_0 (asLockSet ?S))) (=> (= (S_select ?v_0 ?mu) true_term) (= (lockLE ?mu (max ?v_0)) true_term)))))
(assert (forall ((?x Int)) (=> (= (PO_LT (typeof ?x) T_java_lang_Object) true_term) (= (lockLE null ?x) true_term))))
(declare-fun arrayLength (Int) Int)
(assert (forall ((?a Int)) (let ((?v_0 (arrayLength ?a))) (and (<= 0 ?v_0) (= (is ?v_0 T_int) true_term)))))
(declare-fun arrayFresh (Int Int Int Int Int Int Int) Int)
(declare-fun arrayShapeMore (Int Int) Int)
(declare-fun arrayParent (Int) Int)
(declare-fun arrayPosition (Int) Int)
(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) true_term) (and (<= ?a0 (vAllocTime ?a)) (= (isAllocated ?a ?b0) true_term) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (let ((?v_0 (S_select (S_select ?e ?a) ?i))) (and (= (arrayFresh ?v_0 ?a0 ?b0 ?e ?s (elemtype ?T) ?v) true_term) (= (arrayParent ?v_0) ?a) (= (arrayPosition ?v_0) ?i))))))))
(declare-fun arrayShapeOne (Int) Int)
(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) true_term) (and (<= ?a0 (vAllocTime ?a)) (= (isAllocated ?a ?b0) true_term) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (= (S_select (S_select ?e ?a) ?i) ?v))))))
(declare-fun arrayType () Int)
(assert (= arrayType (asChild arrayType T_java_lang_Object)))
(assert (forall ((?t Int)) (= (PO_LT (array ?t) arrayType) true_term)))
(declare-fun isNewArray (Int) Int)
(assert (forall ((?s Int)) (=> (= true_term (isNewArray ?s)) (= (PO_LT (typeof ?s) arrayType) true_term))))
(declare-fun boolAnd (Int Int) Int)
(assert (forall ((?a Int) (?b Int)) (= (= (boolAnd ?a ?b) true_term) (and (= ?a true_term) (= ?b true_term)))))
(declare-fun boolEq (Int Int) Int)
(assert (forall ((?a Int) (?b Int)) (= (= (boolEq ?a ?b) true_term) (= (= ?a true_term) (= ?b true_term)))))
(declare-fun boolImplies (Int Int) Int)
(assert (forall ((?a Int) (?b Int)) (= (= (boolImplies ?a ?b) true_term) (=> (= ?a true_term) (= ?b true_term)))))
(declare-fun boolNE (Int Int) Int)
(assert (forall ((?a Int) (?b Int)) (= (= (boolNE ?a ?b) true_term) (not (= (= ?a true_term) (= ?b true_term))))))
(declare-fun boolNot (Int) Int)
(assert (forall ((?a Int)) (= (= (boolNot ?a) true_term) (not (= ?a true_term)))))
(declare-fun boolOr (Int Int) Int)
(assert (forall ((?a Int) (?b Int)) (= (= (boolOr ?a ?b) true_term) (or (= ?a true_term) (= ?b true_term)))))
(declare-fun integralEQ (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (integralEQ ?x ?y) true_term) (= ?x ?y))))
(declare-fun stringCat (Int Int) Int)
(declare-fun T_java_lang_String () Int)
(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (stringCat ?x ?y))) (and (not (= ?v_0 null)) (= (PO_LT (typeof ?v_0) T_java_lang_String) true_term)))))
(declare-fun integralGE (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (integralGE ?x ?y) true_term) (>= ?x ?y))))
(declare-fun integralGT (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (integralGT ?x ?y) true_term) (> ?x ?y))))
(declare-fun integralLE (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (integralLE ?x ?y) true_term) (<= ?x ?y))))
(declare-fun integralLT (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (integralLT ?x ?y) true_term) (< ?x ?y))))
(declare-fun integralNE (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (integralNE ?x ?y) true_term) (not (= ?x ?y)))))
(declare-fun refEQ (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (refEQ ?x ?y) true_term) (= ?x ?y))))
(declare-fun refNE (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (= (= (refNE ?x ?y) true_term) (not (= ?x ?y)))))
(declare-fun nonnullelements (Int Int) Int)
(assert (forall ((?x Int) (?e Int)) (= (= (nonnullelements ?x ?e) true_term) (and (not (= ?x null)) (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i (arrayLength ?x))) (not (= (S_select (S_select ?e ?x) ?i) null))))))))
(declare-fun classLiteral (Int) Int)
(declare-fun T_java_lang_Class () Int)
(declare-fun alloc () Int)
(assert (forall ((?t Int)) (let ((?v_0 (classLiteral ?t))) (and (not (= ?v_0 null)) (= (is ?v_0 T_java_lang_Class) true_term) (= (isAllocated ?v_0 alloc) true_term)))))
(declare-fun integralAnd (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (=> (or (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralAnd ?x ?y)))))
(assert (forall ((?x Int) (?y Int)) (=> (<= 0 ?x) (<= (integralAnd ?x ?y) ?x))))
(assert (forall ((?x Int) (?y Int)) (=> (<= 0 ?y) (<= (integralAnd ?x ?y) ?y))))
(declare-fun integralOr (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (integralOr ?x ?y))) (=> (and (<= 0 ?x) (<= 0 ?y)) (and (<= ?x ?v_0) (<= ?y ?v_0))))))
(declare-fun integralXor (Int Int) Int)
(assert (forall ((?x Int) (?y Int)) (=> (and (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralXor ?x ?y)))))
(declare-fun intShiftL (Int Int) Int)
(assert (forall ((?n Int)) (=> (and (<= 0 ?n) (< ?n 31)) (<= 1 (intShiftL 1 ?n)))))
(declare-fun longShiftL (Int Int) Int)
(assert (forall ((?n Int)) (=> (and (<= 0 ?n) (< ?n 63)) (<= 1 (longShiftL 1 ?n)))))
(assert true)
(declare-fun T_javafe_ast_ConstructorInvocation () Int)
(declare-fun T_javafe_ast_Stmt () Int)
(declare-fun T_javafe_ast_VariableAccess () Int)
(declare-fun T_javafe_ast_Expr () Int)
(declare-fun T_javafe_ast_ImportDecl () Int)
(declare-fun T_javafe_ast_ASTNode () Int)
(declare-fun T_javafe_ast_TryCatchStmt () Int)
(declare-fun T_javafe_ast_OperatorTags () Int)
(declare-fun T_javafe_ast_GeneratedTags () Int)
(declare-fun T_javafe_ast_TagConstants () Int)
(declare-fun T_javafe_tc_FieldDeclVec () Int)
(declare-fun T_javafe_ast_BlockStmt () Int)
(declare-fun T_javafe_ast_GenericBlockStmt () Int)
(declare-fun T_javafe_ast_RoutineDecl () Int)
(declare-fun T_javafe_ast_TypeDeclElem () Int)
(declare-fun T_javafe_ast_VarInit () Int)
(declare-fun T_javafe_ast_ParenExpr () Int)
(declare-fun T_javafe_ast_Type () Int)
(declare-fun T_javafe_ast_EvalStmt () Int)
(declare-fun T_javafe_ast_TypeObjectDesignator () Int)
(declare-fun T_javafe_ast_ObjectDesignator () Int)
(declare-fun T_java_lang_RuntimeException () Int)
(declare-fun T_java_lang_Exception () Int)
(declare-fun T_javafe_ast_IfStmt () Int)
(declare-fun T_javafe_ast_ArrayInit () Int)
(declare-fun T_java_lang_Throwable () Int)
(declare-fun T_java_util_Map () Int)
(declare-fun T_java_util_EscjavaKeyValue () Int)
(declare-fun T_java_lang_Long () Int)
(declare-fun T_java_lang_Number () Int)
(declare-fun T_java_lang_Comparable () Int)
(declare-fun T_javafe_ast_CondExpr () Int)
(declare-fun T_javafe_util_Location () Int)
(declare-fun T_javafe_tc_MethodDeclVec () Int)
(declare-fun T_javafe_ast_VarDeclStmt () Int)
(declare-fun T_javafe_ast_MethodDecl () Int)
(declare-fun T_javafe_ast_TypeName () Int)
(declare-fun T_javafe_ast_LiteralExpr () Int)
(declare-fun T_java_io_Serializable () Int)
(declare-fun T_javafe_ast_ThrowStmt () Int)
(declare-fun T_java_lang_Boolean () Int)
(declare-fun T_javafe_ast_SkipStmt () Int)
(declare-fun T_javafe_ast_LocalVarDecl () Int)
(declare-fun T_javafe_ast_GenericVarDecl () Int)
(declare-fun T_javafe_ast_CastExpr () Int)
(declare-fun T_javafe_ast_WhileStmt () Int)
(declare-fun T_javafe_ast_TypeDecl () Int)
(declare-fun T_javafe_ast_MethodInvocation () Int)
(declare-fun T_javafe_ast_Identifier () Int)
(declare-fun T_javafe_ast_NewInstanceExpr () Int)
(declare-fun T_java_util_Hashtable () Int)
(declare-fun T_java_util_Dictionary () Int)
(declare-fun T_javafe_tc_Env () Int)
(declare-fun T_javafe_ast_SingleTypeImportDecl () Int)
(declare-fun T_javafe_ast_Name () Int)
(declare-fun T_javafe_ast_CompilationUnit () Int)
(declare-fun T_javafe_ast_BreakStmt () Int)
(declare-fun T_javafe_ast_BranchStmt () Int)
(declare-fun T_javafe_ast_VisitorArgResult () Int)
(declare-fun T_javafe_ast_AmbiguousVariableAccess () Int)
(declare-fun T_javafe_ast_FormalParaDecl () Int)
(declare-fun T_javafe_ast_TryFinallyStmt () Int)
(declare-fun T_javafe_ast_SuperObjectDesignator () Int)
(declare-fun T_javafe_ast_UnaryExpr () Int)
(declare-fun T_javafe_ast_InterfaceDecl () Int)
(declare-fun T_javafe_ast_SynchronizeStmt () Int)
(declare-fun T_java_lang_IndexOutOfBoundsException () Int)
(declare-fun T_javafe_ast_LabelStmt () Int)
(declare-fun T_javafe_ast_CompoundName () Int)
(declare-fun T_javafe_ast_CatchClause () Int)
(declare-fun T_javafe_ast_FieldAccess () Int)
(declare-fun T_javafe_ast_IdentifierVec () Int)
(declare-fun T_java_lang_Integer () Int)
(declare-fun T_javafe_ast_ExprVec () Int)
(declare-fun T_javafe_tc_TagConstants () Int)
(declare-fun T_javafe_parser_TagConstants () Int)
(declare-fun T_javafe_ast_ConstructorDecl () Int)
(declare-fun T_javafe_ast_SwitchStmt () Int)
(declare-fun T_java_lang_Double () Int)
(declare-fun T_javafe_ast_PrimitiveType () Int)
(declare-fun T_javafe_ast_ReturnStmt () Int)
(declare-fun T_java_lang_Float () Int)
(declare-fun T_javafe_ast_ThisExpr () Int)
(declare-fun T_javafe_ast_ExprObjectDesignator () Int)
(declare-fun T_javafe_ast_ForStmt () Int)
(declare-fun T_javafe_ast_InstanceOfExpr () Int)
(declare-fun T_javafe_ast_OnDemandImportDecl () Int)
(declare-fun T_javafe_ast_ClassDeclStmt () Int)
(declare-fun T_javafe_tc_TypeSig () Int)
(declare-fun T_javafe_ast_InitBlock () Int)
(declare-fun T_javafe_ast_ArrayRefExpr () Int)
(declare-fun T_javafe_ast_ArrayType () Int)
(declare-fun T_javafe_ast_ASTDecoration () Int)
(declare-fun T_javafe_ast_VarInitVec () Int)
(declare-fun T_javafe_ast_Visitor () Int)
(declare-fun T_javafe_ast_SwitchLabel () Int)
(declare-fun T_javafe_ast_FieldDecl () Int)
(declare-fun T_javafe_ast_BinaryExpr () Int)
(declare-fun T_javafe_ast_ClassDecl () Int)
(declare-fun T_javafe_ast_ClassLiteral () Int)
(declare-fun T_javafe_ast_DoStmt () Int)
(declare-fun T_javafe_ast_NewArrayExpr () Int)
(declare-fun T_javafe_ast_AmbiguousMethodInvocation () Int)
(declare-fun T_javafe_ast_ContinueStmt () Int)
(declare-fun T_javafe_ast_SimpleName () Int)
(declare-fun DIST_ZERO_1 () Int)
(declare-fun T__TYPE () Int)
(declare-fun TRYCATCHSTMT_19_43_7 () Int)
(declare-fun UNARYSUB_18_55_26 () Int)
(declare-fun TYPEDECLELEMPRAGMA_29_27_26 () Int)
(declare-fun SHORTTYPE_17_36_26 () Int)
(declare-fun WHILESTMT_19_29_7 () Int)
(declare-fun STAR_18_37_26 () Int)
(declare-fun VARIABLEACCESS_19_56_7 () Int)
(declare-fun SINGLETYPEIMPORTDECL_19_15_7 () Int)
(declare-fun BITAND_18_23_26 () Int)
(declare-fun TRYFINALLYSTMT_19_42_7 () Int)
(declare-fun UNARYADD_18_54_26 () Int)
(declare-fun BYTETYPE_17_35_26 () Int)
(declare-fun CLASSDECLSTMT_19_28_7 () Int)
(declare-fun MOD_18_36_26 () Int)
(declare-fun STMTPRAGMA_29_26_26 () Int)
(declare-fun AMBIGUOUSVARIABLEACCESS_19_55_7 () Int)
(declare-fun COMPILATIONUNIT_19_14_7 () Int)
(declare-fun BITXOR_18_22_26 () Int)
(declare-fun SWITCHLABEL_19_41_7 () Int)
(declare-fun ASGBITXOR_18_51_26 () Int)
(declare-fun punctuationStrings_29_134_22 () Int)
(declare-fun NULLTYPE_17_34_26 () Int)
(declare-fun VARDECLSTMT_19_27_7 () Int)
(declare-fun DIV_18_35_26 () Int)
(declare-fun otherStrings_29_193_30 () Int)
(declare-fun PARENEXPR_19_54_7 () Int)
(declare-fun BITOR_18_21_26 () Int)
(declare-fun MODIFIERPRAGMA_29_25_26 () Int)
(declare-fun noTokens_29_212_27 () Int)
(declare-fun SKIPSTMT_19_40_7 () Int)
(declare-fun ASGBITOR_18_50_26 () Int)
(declare-fun COMPOUNDNAME_19_67_7 () Int)
(declare-fun VOIDTYPE_17_33_26 () Int)
(declare-fun SWITCHSTMT_19_26_7 () Int)
(declare-fun SUB_18_34_26 () Int)
(declare-fun CASTEXPR_19_53_7 () Int)
(declare-fun TYPESIG_28_6_28 () Int)
(declare-fun FORSTMT_19_39_7 () Int)
(declare-fun LEXICALPRAGMA_29_24_26 () Int)
(declare-fun ASGBITAND_18_49_26 () Int)
(declare-fun SIMPLENAME_19_66_7 () Int)
(declare-fun DOUBLETYPE_17_32_26 () Int)
(declare-fun BLOCKSTMT_19_25_7 () Int)
(declare-fun ADD_18_33_26 () Int)
(declare-fun FIRST_KEYWORD_29_51_26 () Int)
(declare-fun INSTANCEOFEXPR_19_52_7 () Int)
(declare-fun AND_18_20_26 () Int)
(declare-fun IFSTMT_19_38_7 () Int)
(declare-fun LAST_KEYWORD_29_103_26 () Int)
(declare-fun ASGURSHIFT_18_48_26 () Int)
(declare-fun ARRAYTYPE_19_65_7 () Int)
(declare-fun FORMALPARADECL_19_24_7 () Int)
(declare-fun FLOATTYPE_17_31_26 () Int)
(declare-fun URSHIFT_18_32_26 () Int)
(declare-fun CONDEXPR_19_51_7 () Int)
(declare-fun OR_18_19_26 () Int)
(declare-fun LABELSTMT_19_37_7 () Int)
(declare-fun NULLLIT_17_45_26 () Int)
(declare-fun ASGRSHIFT_18_47_26 () Int)
(declare-fun NULL_29_82_26 () Int)
(declare-fun TYPENAME_19_64_7 () Int)
(declare-fun CHARTYPE_17_30_26 () Int)
(declare-fun FIELDDECL_19_23_7 () Int)
(declare-fun RSHIFT_18_31_26 () Int)
(declare-fun NEWARRAYEXPR_19_50_7 () Int)
(declare-fun CONTINUESTMT_19_36_7 () Int)
(declare-fun STRINGLIT_17_44_26 () Int)
(declare-fun ASGLSHIFT_18_46_26 () Int)
(declare-fun SUPEROBJECTDESIGNATOR_19_63_7 () Int)
(declare-fun LONGTYPE_17_29_26 () Int)
(declare-fun LOCALVARDECL_19_22_7 () Int)
(declare-fun LSHIFT_18_30_26 () Int)
(declare-fun NEWINSTANCEEXPR_19_49_7 () Int)
(declare-fun POSTFIXDEC_18_63_26 () Int)
(declare-fun BREAKSTMT_19_35_7 () Int)
(declare-fun DOUBLELIT_17_43_26 () Int)
(declare-fun ASGSUB_18_45_26 () Int)
(declare-fun TYPEOBJECTDESIGNATOR_19_62_7 () Int)
(declare-fun INTTYPE_17_28_26 () Int)
(declare-fun INITBLOCK_19_21_7 () Int)
(declare-fun LT_18_29_26 () Int)
(declare-fun ARRAYREFEXPR_19_48_7 () Int)
(declare-fun POSTFIXINC_18_62_26 () Int)
(declare-fun THROWSTMT_19_34_7 () Int)
(declare-fun FLOATLIT_17_42_26 () Int)
(declare-fun ASGADD_18_44_26 () Int)
(declare-fun EXPROBJECTDESIGNATOR_19_61_7 () Int)
(declare-fun otherCodes_29_202_27 () Int)
(declare-fun BOOLEANTYPE_17_27_26 () Int)
(declare-fun METHODDECL_19_20_7 () Int)
(declare-fun LE_18_28_26 () Int)
(declare-fun THISEXPR_19_47_7 () Int)
(declare-fun DEC_18_59_26 () Int)
(declare-fun CHARLIT_17_41_26 () Int)
(declare-fun RETURNSTMT_19_33_7 () Int)
(declare-fun punctuationCodes_29_164_19 () Int)
(declare-fun ASGREM_18_43_26 () Int)
(declare-fun CLASSLITERAL_19_60_7 () Int)
(declare-fun IDENT_17_25_26 () Int)
(declare-fun CONSTRUCTORDECL_19_19_7 () Int)
(declare-fun GT_18_27_26 () Int)
(declare-fun ARRAYINIT_19_46_7 () Int)
(declare-fun INC_18_58_26 () Int)
(declare-fun LONGLIT_17_40_26 () Int)
(declare-fun EVALSTMT_19_32_7 () Int)
(declare-fun ASGDIV_18_42_26 () Int)
(declare-fun METHODINVOCATION_19_59_7 () Int)
(declare-fun INTERFACEDECL_19_18_7 () Int)
(declare-fun GE_18_26_26 () Int)
(declare-fun CATCHCLAUSE_19_45_7 () Int)
(declare-fun BITNOT_18_57_26 () Int)
(declare-fun keywordStrings_29_181_30 () Int)
(declare-fun NULL_13_60_26 () Int)
(declare-fun SYNCHRONIZESTMT_19_31_7 () Int)
(declare-fun INTLIT_17_39_26 () Int)
(declare-fun ASGMUL_18_41_26 () Int)
(declare-fun AMBIGUOUSMETHODINVOCATION_19_58_7 () Int)
(declare-fun CLASSDECL_19_17_7 () Int)
(declare-fun EQ_18_25_26 () Int)
(declare-fun TYPEMODIFIERPRAGMA_29_28_26 () Int)
(declare-fun CONSTRUCTORINVOCATION_19_44_7 () Int)
(declare-fun NOT_18_56_26 () Int)
(declare-fun BOOLEANLIT_17_38_26 () Int)
(declare-fun DOSTMT_19_30_7 () Int)
(declare-fun ASSIGN_18_40_26 () Int)
(declare-fun FIELDACCESS_19_57_7 () Int)
(declare-fun ONDEMANDIMPORTDECL_19_16_7 () Int)
(declare-fun NE_18_24_26 () Int)
(assert (let ((?v_0 (array T_java_lang_String)) (?v_1 (array T_int))) (and (= (PO_LT T_javafe_ast_ConstructorInvocation T_javafe_ast_Stmt) true_term) (= T_javafe_ast_ConstructorInvocation (asChild T_javafe_ast_ConstructorInvocation T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_VariableAccess T_javafe_ast_Expr) true_term) (= T_javafe_ast_VariableAccess (asChild T_javafe_ast_VariableAccess T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_ImportDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_ImportDecl (asChild T_javafe_ast_ImportDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_TryCatchStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_TryCatchStmt (asChild T_javafe_ast_TryCatchStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_OperatorTags T_java_lang_Object) true_term) (= T_javafe_ast_OperatorTags (asChild T_javafe_ast_OperatorTags T_java_lang_Object)) (= (PO_LT T_javafe_ast_OperatorTags T_javafe_ast_GeneratedTags) true_term) (= (PO_LT T_javafe_ast_TagConstants T_javafe_ast_OperatorTags) true_term) (= T_javafe_ast_TagConstants (asChild T_javafe_ast_TagConstants T_javafe_ast_OperatorTags)) (= (PO_LT T_javafe_tc_FieldDeclVec T_java_lang_Object) true_term) (= T_javafe_tc_FieldDeclVec (asChild T_javafe_tc_FieldDeclVec T_java_lang_Object)) (= (PO_LT T_javafe_ast_BlockStmt T_javafe_ast_GenericBlockStmt) true_term) (= T_javafe_ast_BlockStmt (asChild T_javafe_ast_BlockStmt T_javafe_ast_GenericBlockStmt)) (= (PO_LT T_javafe_ast_RoutineDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_RoutineDecl (asChild T_javafe_ast_RoutineDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_RoutineDecl T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_javafe_ast_Stmt T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_Stmt (asChild T_javafe_ast_Stmt T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_Expr T_javafe_ast_VarInit) true_term) (= T_javafe_ast_Expr (asChild T_javafe_ast_Expr T_javafe_ast_VarInit)) (= (PO_LT T_javafe_ast_TypeDeclElem T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_ParenExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_ParenExpr (asChild T_javafe_ast_ParenExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_Type T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_Type (asChild T_javafe_ast_Type T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_EvalStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_EvalStmt (asChild T_javafe_ast_EvalStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_TypeObjectDesignator T_javafe_ast_ObjectDesignator) true_term) (= T_javafe_ast_TypeObjectDesignator (asChild T_javafe_ast_TypeObjectDesignator T_javafe_ast_ObjectDesignator)) (= (PO_LT T_java_lang_RuntimeException T_java_lang_Exception) true_term) (= T_java_lang_RuntimeException (asChild T_java_lang_RuntimeException T_java_lang_Exception)) (= (PO_LT T_javafe_ast_GeneratedTags T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_IfStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_IfStmt (asChild T_javafe_ast_IfStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_ArrayInit T_javafe_ast_VarInit) true_term) (= T_javafe_ast_ArrayInit (asChild T_javafe_ast_ArrayInit T_javafe_ast_VarInit)) (= (PO_LT T_java_lang_Exception T_java_lang_Throwable) true_term) (= T_java_lang_Exception (asChild T_java_lang_Exception T_java_lang_Throwable)) (= (PO_LT T_java_util_Map T_java_lang_Object) true_term) (= (PO_LT T_java_util_Map T_java_util_EscjavaKeyValue) true_term) (= (PO_LT T_java_lang_Long T_java_lang_Number) true_term) (= T_java_lang_Long (asChild T_java_lang_Long T_java_lang_Number)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_Long) true_term) (= ?t T_java_lang_Long))) (= (PO_LT T_java_lang_Long T_java_lang_Comparable) true_term) (= (PO_LT T_javafe_ast_CondExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_CondExpr (asChild T_javafe_ast_CondExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_util_Location T_java_lang_Object) true_term) (= T_javafe_util_Location (asChild T_javafe_util_Location T_java_lang_Object)) (= (PO_LT T_javafe_tc_MethodDeclVec T_java_lang_Object) true_term) (= T_javafe_tc_MethodDeclVec (asChild T_javafe_tc_MethodDeclVec T_java_lang_Object)) (= (PO_LT T_javafe_ast_VarDeclStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_VarDeclStmt (asChild T_javafe_ast_VarDeclStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_MethodDecl T_javafe_ast_RoutineDecl) true_term) (= T_javafe_ast_MethodDecl (asChild T_javafe_ast_MethodDecl T_javafe_ast_RoutineDecl)) (= (PO_LT T_javafe_ast_TypeName T_javafe_ast_Type) true_term) (= T_javafe_ast_TypeName (asChild T_javafe_ast_TypeName T_javafe_ast_Type)) (= (PO_LT T_javafe_ast_LiteralExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_LiteralExpr (asChild T_javafe_ast_LiteralExpr T_javafe_ast_Expr)) (= (PO_LT T_java_lang_Throwable T_java_lang_Object) true_term) (= T_java_lang_Throwable (asChild T_java_lang_Throwable T_java_lang_Object)) (= (PO_LT T_java_lang_Throwable T_java_io_Serializable) true_term) (= (PO_LT T_javafe_ast_ThrowStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_ThrowStmt (asChild T_javafe_ast_ThrowStmt T_javafe_ast_Stmt)) (= (PO_LT T_java_lang_Boolean T_java_lang_Object) true_term) (= T_java_lang_Boolean (asChild T_java_lang_Boolean T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_Boolean) true_term) (= ?t T_java_lang_Boolean))) (= (PO_LT T_java_lang_Boolean T_java_io_Serializable) true_term) (= (PO_LT T_java_io_Serializable T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_SkipStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_SkipStmt (asChild T_javafe_ast_SkipStmt T_javafe_ast_Stmt)) (= (PO_LT T_java_lang_Comparable T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_LocalVarDecl T_javafe_ast_GenericVarDecl) true_term) (= T_javafe_ast_LocalVarDecl (asChild T_javafe_ast_LocalVarDecl T_javafe_ast_GenericVarDecl)) (= (PO_LT T_javafe_ast_ObjectDesignator T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_ObjectDesignator (asChild T_javafe_ast_ObjectDesignator T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_CastExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_CastExpr (asChild T_javafe_ast_CastExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_WhileStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_WhileStmt (asChild T_javafe_ast_WhileStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_TypeDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_TypeDecl (asChild T_javafe_ast_TypeDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_TypeDecl T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_javafe_ast_MethodInvocation T_javafe_ast_Expr) true_term) (= T_javafe_ast_MethodInvocation (asChild T_javafe_ast_MethodInvocation T_javafe_ast_Expr)) (= (PO_LT T_java_lang_Cloneable T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_Identifier T_java_lang_Object) true_term) (= T_javafe_ast_Identifier (asChild T_javafe_ast_Identifier T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_javafe_ast_Identifier) true_term) (= ?t T_javafe_ast_Identifier))) (= (PO_LT T_javafe_ast_NewInstanceExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_NewInstanceExpr (asChild T_javafe_ast_NewInstanceExpr T_javafe_ast_Expr)) (= (PO_LT T_java_util_Hashtable T_java_util_Dictionary) true_term) (= T_java_util_Hashtable (asChild T_java_util_Hashtable T_java_util_Dictionary)) (= (PO_LT T_java_util_Hashtable T_java_util_Map) true_term) (= (PO_LT T_java_util_Hashtable T_java_lang_Cloneable) true_term) (= (PO_LT T_java_util_Hashtable T_java_io_Serializable) true_term) (= (PO_LT T_javafe_tc_Env T_java_lang_Object) true_term) (= T_javafe_tc_Env (asChild T_javafe_tc_Env T_java_lang_Object)) (= (PO_LT T_javafe_ast_SingleTypeImportDecl T_javafe_ast_ImportDecl) true_term) (= T_javafe_ast_SingleTypeImportDecl (asChild T_javafe_ast_SingleTypeImportDecl T_javafe_ast_ImportDecl)) (= (PO_LT T_javafe_ast_Name T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_Name (asChild T_javafe_ast_Name T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_CompilationUnit T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_CompilationUnit (asChild T_javafe_ast_CompilationUnit T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_BreakStmt T_javafe_ast_BranchStmt) true_term) (= T_javafe_ast_BreakStmt (asChild T_javafe_ast_BreakStmt T_javafe_ast_BranchStmt)) (= (PO_LT T_java_lang_Number T_java_lang_Object) true_term) (= T_java_lang_Number (asChild T_java_lang_Number T_java_lang_Object)) (= (PO_LT T_java_lang_Number T_java_io_Serializable) true_term) (= (PO_LT T_javafe_ast_VisitorArgResult T_java_lang_Object) true_term) (= T_javafe_ast_VisitorArgResult (asChild T_javafe_ast_VisitorArgResult T_java_lang_Object)) (= (PO_LT T_java_util_EscjavaKeyValue T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_GenericBlockStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_GenericBlockStmt (asChild T_javafe_ast_GenericBlockStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_AmbiguousVariableAccess T_javafe_ast_Expr) true_term) (= T_javafe_ast_AmbiguousVariableAccess (asChild T_javafe_ast_AmbiguousVariableAccess T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_FormalParaDecl T_javafe_ast_GenericVarDecl) true_term) (= T_javafe_ast_FormalParaDecl (asChild T_javafe_ast_FormalParaDecl T_javafe_ast_GenericVarDecl)) (= (PO_LT T_javafe_ast_TryFinallyStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_TryFinallyStmt (asChild T_javafe_ast_TryFinallyStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_SuperObjectDesignator T_javafe_ast_ObjectDesignator) true_term) (= T_javafe_ast_SuperObjectDesignator (asChild T_javafe_ast_SuperObjectDesignator T_javafe_ast_ObjectDesignator)) (= (PO_LT T_javafe_ast_UnaryExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_UnaryExpr (asChild T_javafe_ast_UnaryExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_InterfaceDecl T_javafe_ast_TypeDecl) true_term) (= T_javafe_ast_InterfaceDecl (asChild T_javafe_ast_InterfaceDecl T_javafe_ast_TypeDecl)) (= (PO_LT T_javafe_ast_SynchronizeStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_SynchronizeStmt (asChild T_javafe_ast_SynchronizeStmt T_javafe_ast_Stmt)) (= (PO_LT T_java_lang_IndexOutOfBoundsException T_java_lang_RuntimeException) true_term) (= T_java_lang_IndexOutOfBoundsException (asChild T_java_lang_IndexOutOfBoundsException T_java_lang_RuntimeException)) (= (PO_LT T_javafe_ast_LabelStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_LabelStmt (asChild T_javafe_ast_LabelStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_CompoundName T_javafe_ast_Name) true_term) (= T_javafe_ast_CompoundName (asChild T_javafe_ast_CompoundName T_javafe_ast_Name)) (= (PO_LT T_javafe_ast_CatchClause T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_CatchClause (asChild T_javafe_ast_CatchClause T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_FieldAccess T_javafe_ast_Expr) true_term) (= T_javafe_ast_FieldAccess (asChild T_javafe_ast_FieldAccess T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_IdentifierVec T_java_lang_Object) true_term) (= T_javafe_ast_IdentifierVec (asChild T_javafe_ast_IdentifierVec T_java_lang_Object)) (= (PO_LT T_java_lang_Integer T_java_lang_Number) true_term) (= T_java_lang_Integer (asChild T_java_lang_Integer T_java_lang_Number)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_Integer) true_term) (= ?t T_java_lang_Integer))) (= (PO_LT T_java_lang_Integer T_java_lang_Comparable) true_term) (= (PO_LT T_javafe_ast_ExprVec T_java_lang_Object) true_term) (= T_javafe_ast_ExprVec (asChild T_javafe_ast_ExprVec T_java_lang_Object)) (= (PO_LT T_javafe_tc_TagConstants T_javafe_parser_TagConstants) true_term) (= T_javafe_tc_TagConstants (asChild T_javafe_tc_TagConstants T_javafe_parser_TagConstants)) (= (PO_LT T_javafe_ast_ConstructorDecl T_javafe_ast_RoutineDecl) true_term) (= T_javafe_ast_ConstructorDecl (asChild T_javafe_ast_ConstructorDecl T_javafe_ast_RoutineDecl)) (= (PO_LT T_javafe_ast_SwitchStmt T_javafe_ast_GenericBlockStmt) true_term) (= T_javafe_ast_SwitchStmt (asChild T_javafe_ast_SwitchStmt T_javafe_ast_GenericBlockStmt)) (= (PO_LT T_javafe_parser_TagConstants T_javafe_ast_TagConstants) true_term) (= T_javafe_parser_TagConstants (asChild T_javafe_parser_TagConstants T_javafe_ast_TagConstants)) (= (PO_LT T_javafe_ast_ASTNode T_java_lang_Object) true_term) (= T_javafe_ast_ASTNode (asChild T_javafe_ast_ASTNode T_java_lang_Object)) (= (PO_LT T_javafe_ast_ASTNode T_java_lang_Cloneable) true_term) (= (PO_LT T_java_lang_Double T_java_lang_Number) true_term) (= T_java_lang_Double (asChild T_java_lang_Double T_java_lang_Number)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_Double) true_term) (= ?t T_java_lang_Double))) (= (PO_LT T_java_lang_Double T_java_lang_Comparable) true_term) (= (PO_LT T_javafe_ast_PrimitiveType T_javafe_ast_Type) true_term) (= T_javafe_ast_PrimitiveType (asChild T_javafe_ast_PrimitiveType T_javafe_ast_Type)) (= (PO_LT T_javafe_ast_ReturnStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_ReturnStmt (asChild T_javafe_ast_ReturnStmt T_javafe_ast_Stmt)) (= (PO_LT T_java_lang_Float T_java_lang_Number) true_term) (= T_java_lang_Float (asChild T_java_lang_Float T_java_lang_Number)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_Float) true_term) (= ?t T_java_lang_Float))) (= (PO_LT T_java_lang_Float T_java_lang_Comparable) true_term) (= (PO_LT T_javafe_ast_ThisExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_ThisExpr (asChild T_javafe_ast_ThisExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_VarInit T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_VarInit (asChild T_javafe_ast_VarInit T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_ExprObjectDesignator T_javafe_ast_ObjectDesignator) true_term) (= T_javafe_ast_ExprObjectDesignator (asChild T_javafe_ast_ExprObjectDesignator T_javafe_ast_ObjectDesignator)) (= (PO_LT T_java_util_Dictionary T_java_lang_Object) true_term) (= T_java_util_Dictionary (asChild T_java_util_Dictionary T_java_lang_Object)) (= (PO_LT T_java_util_Dictionary T_java_util_EscjavaKeyValue) true_term) (= (PO_LT T_javafe_ast_ForStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_ForStmt (asChild T_javafe_ast_ForStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_InstanceOfExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_InstanceOfExpr (asChild T_javafe_ast_InstanceOfExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_GenericVarDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_GenericVarDecl (asChild T_javafe_ast_GenericVarDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_OnDemandImportDecl T_javafe_ast_ImportDecl) true_term) (= T_javafe_ast_OnDemandImportDecl (asChild T_javafe_ast_OnDemandImportDecl T_javafe_ast_ImportDecl)) (= (PO_LT T_javafe_ast_ClassDeclStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_ClassDeclStmt (asChild T_javafe_ast_ClassDeclStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_tc_TypeSig T_javafe_ast_Type) true_term) (= T_javafe_tc_TypeSig (asChild T_javafe_tc_TypeSig T_javafe_ast_Type)) (= (PO_LT T_javafe_ast_InitBlock T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_InitBlock (asChild T_javafe_ast_InitBlock T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_InitBlock T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_javafe_ast_ArrayRefExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_ArrayRefExpr (asChild T_javafe_ast_ArrayRefExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_ArrayType T_javafe_ast_Type) true_term) (= T_javafe_ast_ArrayType (asChild T_javafe_ast_ArrayType T_javafe_ast_Type)) (= (PO_LT T_javafe_ast_BranchStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_BranchStmt (asChild T_javafe_ast_BranchStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_ASTDecoration T_java_lang_Object) true_term) (= T_javafe_ast_ASTDecoration (asChild T_javafe_ast_ASTDecoration T_java_lang_Object)) (= (PO_LT T_javafe_ast_VarInitVec T_java_lang_Object) true_term) (= T_javafe_ast_VarInitVec (asChild T_javafe_ast_VarInitVec T_java_lang_Object)) (= (PO_LT T_javafe_ast_Visitor T_java_lang_Object) true_term) (= T_javafe_ast_Visitor (asChild T_javafe_ast_Visitor T_java_lang_Object)) (= (PO_LT T_javafe_ast_SwitchLabel T_javafe_ast_Stmt) true_term) (= T_javafe_ast_SwitchLabel (asChild T_javafe_ast_SwitchLabel T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_FieldDecl T_javafe_ast_GenericVarDecl) true_term) (= T_javafe_ast_FieldDecl (asChild T_javafe_ast_FieldDecl T_javafe_ast_GenericVarDecl)) (= (PO_LT T_javafe_ast_FieldDecl T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_javafe_ast_BinaryExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_BinaryExpr (asChild T_javafe_ast_BinaryExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_ClassDecl T_javafe_ast_TypeDecl) true_term) (= T_javafe_ast_ClassDecl (asChild T_javafe_ast_ClassDecl T_javafe_ast_TypeDecl)) (= (PO_LT T_javafe_ast_ClassLiteral T_javafe_ast_Expr) true_term) (= T_javafe_ast_ClassLiteral (asChild T_javafe_ast_ClassLiteral T_javafe_ast_Expr)) (= (PO_LT T_java_lang_String T_java_lang_Object) true_term) (= T_java_lang_String (asChild T_java_lang_String T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_String) true_term) (= ?t T_java_lang_String))) (= (PO_LT T_java_lang_String T_java_io_Serializable) true_term) (= (PO_LT T_java_lang_String T_java_lang_Comparable) true_term) (= (PO_LT T_javafe_ast_DoStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_DoStmt (asChild T_javafe_ast_DoStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_ast_NewArrayExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_NewArrayExpr (asChild T_javafe_ast_NewArrayExpr T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_AmbiguousMethodInvocation T_javafe_ast_Expr) true_term) (= T_javafe_ast_AmbiguousMethodInvocation (asChild T_javafe_ast_AmbiguousMethodInvocation T_javafe_ast_Expr)) (= (PO_LT T_javafe_ast_ContinueStmt T_javafe_ast_BranchStmt) true_term) (= T_javafe_ast_ContinueStmt (asChild T_javafe_ast_ContinueStmt T_javafe_ast_BranchStmt)) (= (PO_LT T_javafe_ast_SimpleName T_javafe_ast_Name) true_term) (= T_javafe_ast_SimpleName (asChild T_javafe_ast_SimpleName T_javafe_ast_Name)) (and (= arrayType (+ DIST_ZERO_1 0)) (= T_boolean (+ DIST_ZERO_1 1)) (= T_char (+ DIST_ZERO_1 2)) (= T_byte (+ DIST_ZERO_1 3)) (= T_short (+ DIST_ZERO_1 4)) (= T_int (+ DIST_ZERO_1 5)) (= T_long (+ DIST_ZERO_1 6)) (= T_float (+ DIST_ZERO_1 7)) (= T_double (+ DIST_ZERO_1 8)) (= T__TYPE (+ DIST_ZERO_1 9)) (= T_javafe_ast_ConstructorInvocation (+ DIST_ZERO_1 10)) (= T_javafe_ast_VariableAccess (+ DIST_ZERO_1 11)) (= T_javafe_ast_ImportDecl (+ DIST_ZERO_1 12)) (= T_javafe_ast_TryCatchStmt (+ DIST_ZERO_1 13)) (= T_javafe_ast_OperatorTags (+ DIST_ZERO_1 14)) (= T_javafe_ast_TagConstants (+ DIST_ZERO_1 15)) (= T_javafe_tc_FieldDeclVec (+ DIST_ZERO_1 16)) (= T_javafe_ast_BlockStmt (+ DIST_ZERO_1 17)) (= T_javafe_ast_RoutineDecl (+ DIST_ZERO_1 18)) (= T_javafe_ast_Stmt (+ DIST_ZERO_1 19)) (= T_javafe_ast_Expr (+ DIST_ZERO_1 20)) (= T_javafe_ast_TypeDeclElem (+ DIST_ZERO_1 21)) (= T_javafe_ast_ParenExpr (+ DIST_ZERO_1 22)) (= T_javafe_ast_Type (+ DIST_ZERO_1 23)) (= T_javafe_ast_EvalStmt (+ DIST_ZERO_1 24)) (= T_javafe_ast_TypeObjectDesignator (+ DIST_ZERO_1 25)) (= T_java_lang_RuntimeException (+ DIST_ZERO_1 26)) (= T_javafe_ast_GeneratedTags (+ DIST_ZERO_1 27)) (= T_javafe_ast_IfStmt (+ DIST_ZERO_1 28)) (= T_javafe_ast_ArrayInit (+ DIST_ZERO_1 29)) (= T_java_lang_Exception (+ DIST_ZERO_1 30)) (= T_java_util_Map (+ DIST_ZERO_1 31)) (= T_java_lang_Long (+ DIST_ZERO_1 32)) (= T_javafe_ast_CondExpr (+ DIST_ZERO_1 33)) (= T_javafe_util_Location (+ DIST_ZERO_1 34)) (= T_javafe_tc_MethodDeclVec (+ DIST_ZERO_1 35)) (= T_javafe_ast_VarDeclStmt (+ DIST_ZERO_1 36)) (= T_javafe_ast_MethodDecl (+ DIST_ZERO_1 37)) (= T_javafe_ast_TypeName (+ DIST_ZERO_1 38)) (= T_javafe_ast_LiteralExpr (+ DIST_ZERO_1 39)) (= T_java_lang_Throwable (+ DIST_ZERO_1 40)) (= T_javafe_ast_ThrowStmt (+ DIST_ZERO_1 41)) (= T_java_lang_Boolean (+ DIST_ZERO_1 42)) (= T_java_io_Serializable (+ DIST_ZERO_1 43)) (= T_javafe_ast_SkipStmt (+ DIST_ZERO_1 44)) (= T_java_lang_Comparable (+ DIST_ZERO_1 45)) (= T_javafe_ast_LocalVarDecl (+ DIST_ZERO_1 46)) (= T_javafe_ast_ObjectDesignator (+ DIST_ZERO_1 47)) (= T_javafe_ast_CastExpr (+ DIST_ZERO_1 48)) (= T_javafe_ast_WhileStmt (+ DIST_ZERO_1 49)) (= T_javafe_ast_TypeDecl (+ DIST_ZERO_1 50)) (= T_javafe_ast_MethodInvocation (+ DIST_ZERO_1 51)) (= T_java_lang_Cloneable (+ DIST_ZERO_1 52)) (= T_javafe_ast_Identifier (+ DIST_ZERO_1 53)) (= T_javafe_ast_NewInstanceExpr (+ DIST_ZERO_1 54)) (= T_java_lang_Object (+ DIST_ZERO_1 55)) (= T_java_util_Hashtable (+ DIST_ZERO_1 56)) (= T_javafe_tc_Env (+ DIST_ZERO_1 57)) (= T_javafe_ast_SingleTypeImportDecl (+ DIST_ZERO_1 58)) (= T_javafe_ast_Name (+ DIST_ZERO_1 59)) (= T_javafe_ast_CompilationUnit (+ DIST_ZERO_1 60)) (= T_javafe_ast_BreakStmt (+ DIST_ZERO_1 61)) (= T_java_lang_Number (+ DIST_ZERO_1 62)) (= T_javafe_ast_VisitorArgResult (+ DIST_ZERO_1 63)) (= T_java_util_EscjavaKeyValue (+ DIST_ZERO_1 64)) (= T_javafe_ast_GenericBlockStmt (+ DIST_ZERO_1 65)) (= T_javafe_ast_AmbiguousVariableAccess (+ DIST_ZERO_1 66)) (= T_javafe_ast_FormalParaDecl (+ DIST_ZERO_1 67)) (= T_javafe_ast_TryFinallyStmt (+ DIST_ZERO_1 68)) (= T_javafe_ast_SuperObjectDesignator (+ DIST_ZERO_1 69)) (= T_javafe_ast_UnaryExpr (+ DIST_ZERO_1 70)) (= T_javafe_ast_InterfaceDecl (+ DIST_ZERO_1 71)) (= T_javafe_ast_SynchronizeStmt (+ DIST_ZERO_1 72)) (= T_java_lang_IndexOutOfBoundsException (+ DIST_ZERO_1 73)) (= T_javafe_ast_LabelStmt (+ DIST_ZERO_1 74)) (= T_javafe_ast_CompoundName (+ DIST_ZERO_1 75)) (= T_javafe_ast_CatchClause (+ DIST_ZERO_1 76)) (= T_javafe_ast_FieldAccess (+ DIST_ZERO_1 77)) (= T_javafe_ast_IdentifierVec (+ DIST_ZERO_1 78)) (= T_java_lang_Integer (+ DIST_ZERO_1 79)) (= T_javafe_ast_ExprVec (+ DIST_ZERO_1 80)) (= T_javafe_tc_TagConstants (+ DIST_ZERO_1 81)) (= T_javafe_ast_ConstructorDecl (+ DIST_ZERO_1 82)) (= T_javafe_ast_SwitchStmt (+ DIST_ZERO_1 83)) (= T_javafe_parser_TagConstants (+ DIST_ZERO_1 84)) (= T_javafe_ast_ASTNode (+ DIST_ZERO_1 85)) (= T_java_lang_Double (+ DIST_ZERO_1 86)) (= T_javafe_ast_PrimitiveType (+ DIST_ZERO_1 87)) (= T_javafe_ast_ReturnStmt (+ DIST_ZERO_1 88)) (= T_java_lang_Float (+ DIST_ZERO_1 89)) (= T_javafe_ast_ThisExpr (+ DIST_ZERO_1 90)) (= T_javafe_ast_VarInit (+ DIST_ZERO_1 91)) (= T_javafe_ast_ExprObjectDesignator (+ DIST_ZERO_1 92)) (= T_java_util_Dictionary (+ DIST_ZERO_1 93)) (= T_javafe_ast_ForStmt (+ DIST_ZERO_1 94)) (= T_javafe_ast_InstanceOfExpr (+ DIST_ZERO_1 95)) (= T_javafe_ast_GenericVarDecl (+ DIST_ZERO_1 96)) (= T_javafe_ast_OnDemandImportDecl (+ DIST_ZERO_1 97)) (= T_javafe_ast_ClassDeclStmt (+ DIST_ZERO_1 98)) (= T_javafe_tc_TypeSig (+ DIST_ZERO_1 99)) (= T_javafe_ast_InitBlock (+ DIST_ZERO_1 100)) (= T_javafe_ast_ArrayRefExpr (+ DIST_ZERO_1 101)) (= T_javafe_ast_ArrayType (+ DIST_ZERO_1 102)) (= T_javafe_ast_BranchStmt (+ DIST_ZERO_1 103)) (= T_javafe_ast_ASTDecoration (+ DIST_ZERO_1 104)) (= T_javafe_ast_VarInitVec (+ DIST_ZERO_1 105)) (= T_javafe_ast_Visitor (+ DIST_ZERO_1 106)) (= T_javafe_ast_SwitchLabel (+ DIST_ZERO_1 107)) (= T_javafe_ast_FieldDecl (+ DIST_ZERO_1 108)) (= T_javafe_ast_BinaryExpr (+ DIST_ZERO_1 109)) (= T_javafe_ast_ClassDecl (+ DIST_ZERO_1 110)) (= T_javafe_ast_ClassLiteral (+ DIST_ZERO_1 111)) (= T_java_lang_String (+ DIST_ZERO_1 112)) (= T_javafe_ast_DoStmt (+ DIST_ZERO_1 113)) (= T_javafe_ast_NewArrayExpr (+ DIST_ZERO_1 114)) (= T_javafe_ast_AmbiguousMethodInvocation (+ DIST_ZERO_1 115)) (= T_javafe_ast_ContinueStmt (+ DIST_ZERO_1 116)) (= T_javafe_ast_SimpleName (+ DIST_ZERO_1 117))) (= true_term (is TRYCATCHSTMT_19_43_7 T_int)) (= TRYCATCHSTMT_19_43_7 29) (= true_term (is UNARYSUB_18_55_26 T_int)) (= UNARYSUB_18_55_26 86) (= true_term (is TYPEDECLELEMPRAGMA_29_27_26 T_int)) (= TYPEDECLELEMPRAGMA_29_27_26 117) (= true_term (is SHORTTYPE_17_36_26 T_int)) (= SHORTTYPE_17_36_26 103) (= true_term (is WHILESTMT_19_29_7 T_int)) (= WHILESTMT_19_29_7 15) (= true_term (is STAR_18_37_26 T_int)) (= STAR_18_37_26 72) (= true_term (is VARIABLEACCESS_19_56_7 T_int)) (= VARIABLEACCESS_19_56_7 42) (= true_term (is SINGLETYPEIMPORTDECL_19_15_7 T_int)) (= SINGLETYPEIMPORTDECL_19_15_7 1) (= true_term (is BITAND_18_23_26 T_int)) (= BITAND_18_23_26 58) (= true_term (is TRYFINALLYSTMT_19_42_7 T_int)) (= TRYFINALLYSTMT_19_42_7 28) (= true_term (is UNARYADD_18_54_26 T_int)) (= UNARYADD_18_54_26 85) (= true_term (is BYTETYPE_17_35_26 T_int)) (= BYTETYPE_17_35_26 102) (= true_term (is CLASSDECLSTMT_19_28_7 T_int)) (= CLASSDECLSTMT_19_28_7 14) (= true_term (is MOD_18_36_26 T_int)) (= MOD_18_36_26 71) (= true_term (is STMTPRAGMA_29_26_26 T_int)) (= STMTPRAGMA_29_26_26 116) (= true_term (is AMBIGUOUSVARIABLEACCESS_19_55_7 T_int)) (= AMBIGUOUSVARIABLEACCESS_19_55_7 41) (= true_term (is COMPILATIONUNIT_19_14_7 T_int)) (= COMPILATIONUNIT_19_14_7 0) (= true_term (is BITXOR_18_22_26 T_int)) (= BITXOR_18_22_26 57) (= true_term (is SWITCHLABEL_19_41_7 T_int)) (= SWITCHLABEL_19_41_7 27) (= true_term (is ASGBITXOR_18_51_26 T_int)) (= ASGBITXOR_18_51_26 84) (= true_term (is punctuationStrings_29_134_22 ?v_0)) (not (= punctuationStrings_29_134_22 null)) (= (typeof punctuationStrings_29_134_22) ?v_0) (= (arrayLength punctuationStrings_29_134_22) 48) (= true_term (is NULLTYPE_17_34_26 T_int)) (= NULLTYPE_17_34_26 101) (= true_term (is VARDECLSTMT_19_27_7 T_int)) (= VARDECLSTMT_19_27_7 13) (= true_term (is DIV_18_35_26 T_int)) (= DIV_18_35_26 70) (= true_term (is otherStrings_29_193_30 ?v_0)) (not (= otherStrings_29_193_30 null)) (= (typeof otherStrings_29_193_30) ?v_0) (= (arrayLength otherStrings_29_193_30) 15) (= true_term (is PARENEXPR_19_54_7 T_int)) (= PARENEXPR_19_54_7 40) (= true_term (is BITOR_18_21_26 T_int)) (= BITOR_18_21_26 56) (= true_term (is MODIFIERPRAGMA_29_25_26 T_int)) (= MODIFIERPRAGMA_29_25_26 115) (= true_term (is noTokens_29_212_27 T_int)) (= true_term (is SKIPSTMT_19_40_7 T_int)) (= SKIPSTMT_19_40_7 26) (= true_term (is ASGBITOR_18_50_26 T_int)) (= ASGBITOR_18_50_26 83) (= true_term (is COMPOUNDNAME_19_67_7 T_int)) (= COMPOUNDNAME_19_67_7 53) (= true_term (is VOIDTYPE_17_33_26 T_int)) (= VOIDTYPE_17_33_26 100) (= true_term (is SWITCHSTMT_19_26_7 T_int)) (= SWITCHSTMT_19_26_7 12) (= true_term (is SUB_18_34_26 T_int)) (= SUB_18_34_26 69) (= true_term (is CASTEXPR_19_53_7 T_int)) (= CASTEXPR_19_53_7 39) (= true_term (is TYPESIG_28_6_28 T_int)) (= TYPESIG_28_6_28 184) (= true_term (is FORSTMT_19_39_7 T_int)) (= FORSTMT_19_39_7 25) (= true_term (is LEXICALPRAGMA_29_24_26 T_int)) (= LEXICALPRAGMA_29_24_26 114) (= true_term (is ASGBITAND_18_49_26 T_int)) (= ASGBITAND_18_49_26 82) (= true_term (is SIMPLENAME_19_66_7 T_int)) (= SIMPLENAME_19_66_7 52) (= true_term (is DOUBLETYPE_17_32_26 T_int)) (= DOUBLETYPE_17_32_26 99) (= true_term (is BLOCKSTMT_19_25_7 T_int)) (= BLOCKSTMT_19_25_7 11) (= true_term (is ADD_18_33_26 T_int)) (= ADD_18_33_26 68) (= true_term (is FIRST_KEYWORD_29_51_26 T_int)) (= FIRST_KEYWORD_29_51_26 133) (= true_term (is INSTANCEOFEXPR_19_52_7 T_int)) (= INSTANCEOFEXPR_19_52_7 38) (= true_term (is AND_18_20_26 T_int)) (= AND_18_20_26 55) (= true_term (is IFSTMT_19_38_7 T_int)) (= IFSTMT_19_38_7 24) (= true_term (is LAST_KEYWORD_29_103_26 T_int)) (= LAST_KEYWORD_29_103_26 183) (= true_term (is ASGURSHIFT_18_48_26 T_int)) (= ASGURSHIFT_18_48_26 81) (= true_term (is ARRAYTYPE_19_65_7 T_int)) (= ARRAYTYPE_19_65_7 51) (= true_term (is FORMALPARADECL_19_24_7 T_int)) (= FORMALPARADECL_19_24_7 10) (= true_term (is FLOATTYPE_17_31_26 T_int)) (= FLOATTYPE_17_31_26 98) (= true_term (is URSHIFT_18_32_26 T_int)) (= URSHIFT_18_32_26 67) (= true_term (is CONDEXPR_19_51_7 T_int)) (= CONDEXPR_19_51_7 37) (= true_term (is OR_18_19_26 T_int)) (= OR_18_19_26 54) (= true_term (is LABELSTMT_19_37_7 T_int)) (= LABELSTMT_19_37_7 23) (= true_term (is NULLLIT_17_45_26 T_int)) (= NULLLIT_17_45_26 111) (= true_term (is ASGRSHIFT_18_47_26 T_int)) (= ASGRSHIFT_18_47_26 80) (= true_term (is NULL_29_82_26 T_int)) (= NULL_29_82_26 163) (= true_term (is TYPENAME_19_64_7 T_int)) (= TYPENAME_19_64_7 50) (= true_term (is CHARTYPE_17_30_26 T_int)) (= CHARTYPE_17_30_26 97) (= true_term (is FIELDDECL_19_23_7 T_int)) (= FIELDDECL_19_23_7 9) (= true_term (is RSHIFT_18_31_26 T_int)) (= RSHIFT_18_31_26 66) (= true_term (is NEWARRAYEXPR_19_50_7 T_int)) (= NEWARRAYEXPR_19_50_7 36) (= true_term (is CONTINUESTMT_19_36_7 T_int)) (= CONTINUESTMT_19_36_7 22) (= true_term (is STRINGLIT_17_44_26 T_int)) (= STRINGLIT_17_44_26 110) (= true_term (is ASGLSHIFT_18_46_26 T_int)) (= ASGLSHIFT_18_46_26 79) (= true_term (is SUPEROBJECTDESIGNATOR_19_63_7 T_int)) (= SUPEROBJECTDESIGNATOR_19_63_7 49) (= true_term (is LONGTYPE_17_29_26 T_int)) (= LONGTYPE_17_29_26 96) (= true_term (is LOCALVARDECL_19_22_7 T_int)) (= LOCALVARDECL_19_22_7 8) (= true_term (is LSHIFT_18_30_26 T_int)) (= LSHIFT_18_30_26 65) (= true_term (is NEWINSTANCEEXPR_19_49_7 T_int)) (= NEWINSTANCEEXPR_19_49_7 35) (= true_term (is POSTFIXDEC_18_63_26 T_int)) (= POSTFIXDEC_18_63_26 92) (= true_term (is BREAKSTMT_19_35_7 T_int)) (= BREAKSTMT_19_35_7 21) (= true_term (is DOUBLELIT_17_43_26 T_int)) (= DOUBLELIT_17_43_26 109) (= true_term (is ASGSUB_18_45_26 T_int)) (= ASGSUB_18_45_26 78) (= true_term (is TYPEOBJECTDESIGNATOR_19_62_7 T_int)) (= TYPEOBJECTDESIGNATOR_19_62_7 48) (= true_term (is INTTYPE_17_28_26 T_int)) (= INTTYPE_17_28_26 95) (= true_term (is INITBLOCK_19_21_7 T_int)) (= INITBLOCK_19_21_7 7) (= true_term (is LT_18_29_26 T_int)) (= LT_18_29_26 64) (= true_term (is ARRAYREFEXPR_19_48_7 T_int)) (= ARRAYREFEXPR_19_48_7 34) (= true_term (is POSTFIXINC_18_62_26 T_int)) (= POSTFIXINC_18_62_26 91) (= true_term (is THROWSTMT_19_34_7 T_int)) (= THROWSTMT_19_34_7 20) (= true_term (is FLOATLIT_17_42_26 T_int)) (= FLOATLIT_17_42_26 108) (= true_term (is ASGADD_18_44_26 T_int)) (= ASGADD_18_44_26 77) (= true_term (is EXPROBJECTDESIGNATOR_19_61_7 T_int)) (= EXPROBJECTDESIGNATOR_19_61_7 47) (= true_term (is otherCodes_29_202_27 ?v_1)) (not (= otherCodes_29_202_27 null)) (= (typeof otherCodes_29_202_27) ?v_1) (= (arrayLength otherCodes_29_202_27) 15) (= true_term (is BOOLEANTYPE_17_27_26 T_int)) (= BOOLEANTYPE_17_27_26 94) (= true_term (is METHODDECL_19_20_7 T_int)) (= METHODDECL_19_20_7 6) (= true_term (is LE_18_28_26 T_int)) (= LE_18_28_26 63) (= true_term (is THISEXPR_19_47_7 T_int)) (= THISEXPR_19_47_7 33) (= true_term (is DEC_18_59_26 T_int)) (= DEC_18_59_26 90) (= true_term (is CHARLIT_17_41_26 T_int)) (= CHARLIT_17_41_26 107) (= true_term (is RETURNSTMT_19_33_7 T_int)) (= RETURNSTMT_19_33_7 19) (= true_term (is punctuationCodes_29_164_19 ?v_1)) (not (= punctuationCodes_29_164_19 null)) (= (typeof punctuationCodes_29_164_19) ?v_1) (= (arrayLength punctuationCodes_29_164_19) 48) (= true_term (is ASGREM_18_43_26 T_int)) (= ASGREM_18_43_26 76) (= true_term (is CLASSLITERAL_19_60_7 T_int)) (= CLASSLITERAL_19_60_7 46) (= true_term (is IDENT_17_25_26 T_int)) (= IDENT_17_25_26 93) (= true_term (is CONSTRUCTORDECL_19_19_7 T_int)) (= CONSTRUCTORDECL_19_19_7 5) (= true_term (is GT_18_27_26 T_int)) (= GT_18_27_26 62) (= true_term (is ARRAYINIT_19_46_7 T_int)) (= ARRAYINIT_19_46_7 32) (= true_term (is INC_18_58_26 T_int)) (= INC_18_58_26 89) (= true_term (is LONGLIT_17_40_26 T_int)) (= LONGLIT_17_40_26 106) (= true_term (is EVALSTMT_19_32_7 T_int)) (= EVALSTMT_19_32_7 18) (= true_term (is ASGDIV_18_42_26 T_int)) (= ASGDIV_18_42_26 75) (= true_term (is METHODINVOCATION_19_59_7 T_int)) (= METHODINVOCATION_19_59_7 45) (= true_term (is INTERFACEDECL_19_18_7 T_int)) (= INTERFACEDECL_19_18_7 4) (= true_term (is GE_18_26_26 T_int)) (= GE_18_26_26 61) (= true_term (is CATCHCLAUSE_19_45_7 T_int)) (= CATCHCLAUSE_19_45_7 31) (= true_term (is BITNOT_18_57_26 T_int)) (= BITNOT_18_57_26 88) (= true_term (is keywordStrings_29_181_30 ?v_0)) (not (= keywordStrings_29_181_30 null)) (= (typeof keywordStrings_29_181_30) ?v_0) (= (arrayLength keywordStrings_29_181_30) 51) (= true_term (is NULL_13_60_26 T_int)) (= NULL_13_60_26 0) (= true_term (is SYNCHRONIZESTMT_19_31_7 T_int)) (= SYNCHRONIZESTMT_19_31_7 17) (= true_term (is INTLIT_17_39_26 T_int)) (= INTLIT_17_39_26 105) (= true_term (is ASGMUL_18_41_26 T_int)) (= ASGMUL_18_41_26 74) (= true_term (is AMBIGUOUSMETHODINVOCATION_19_58_7 T_int)) (= AMBIGUOUSMETHODINVOCATION_19_58_7 44) (= true_term (is CLASSDECL_19_17_7 T_int)) (= CLASSDECL_19_17_7 3) (= true_term (is EQ_18_25_26 T_int)) (= EQ_18_25_26 60) (= true_term (is TYPEMODIFIERPRAGMA_29_28_26 T_int)) (= TYPEMODIFIERPRAGMA_29_28_26 118) (= true_term (is CONSTRUCTORINVOCATION_19_44_7 T_int)) (= CONSTRUCTORINVOCATION_19_44_7 30) (= true_term (is NOT_18_56_26 T_int)) (= NOT_18_56_26 87) (= true_term (is BOOLEANLIT_17_38_26 T_int)) (= BOOLEANLIT_17_38_26 104) (= true_term (is DOSTMT_19_30_7 T_int)) (= DOSTMT_19_30_7 16) (= true_term (is ASSIGN_18_40_26 T_int)) (= ASSIGN_18_40_26 73) (= true_term (is FIELDACCESS_19_57_7 T_int)) (= FIELDACCESS_19_57_7 43) (= true_term (is ONDEMANDIMPORTDECL_19_16_7 T_int)) (= ONDEMANDIMPORTDECL_19_16_7 2) (= true_term (is NE_18_24_26 T_int)) (= NE_18_24_26 59))))
(declare-fun locOpenBrace_pre_80_36_13 () Int)
(declare-fun locOpenBrace_80_36_13 () Int)
(declare-fun TRYCATCHSTMT_pre_19_43_7 () Int)
(declare-fun UNARYSUB_pre_18_55_26 () Int)
(declare-fun TYPEDECLELEMPRAGMA_pre_29_27_26 () Int)
(declare-fun SHORTTYPE_pre_17_36_26 () Int)
(declare-fun WHILESTMT_pre_19_29_7 () Int)
(declare-fun body_pre_80_34_19 () Int)
(declare-fun body_80_34_19 () Int)
(declare-fun STAR_pre_18_37_26 () Int)
(declare-fun elems_pre_18_34 () Int)
(declare-fun elems_18_34 () Int)
(declare-fun enclosingInstance_pre_122_25_14 () Int)
(declare-fun enclosingInstance_122_25_14 () Int)
(declare-fun loc_pre_110_18_13 () Int)
(declare-fun loc_110_18_13 () Int)
(declare-fun elements_pre_124_61_33 () Int)
(declare-fun elements_124_61_33 () Int)
(declare-fun loc_pre_122_49_13 () Int)
(declare-fun loc_122_49_13 () Int)
(declare-fun VARIABLEACCESS_pre_19_56_7 () Int)
(declare-fun SINGLETYPEIMPORTDECL_pre_19_15_7 () Int)
(declare-fun BITAND_pre_18_23_26 () Int)
(declare-fun locCloseBrace_pre_90_25_13 () Int)
(declare-fun locCloseBrace_90_25_13 () Int)
(declare-fun loc_pre_139_20_13 () Int)
(declare-fun loc_139_20_13 () Int)
(declare-fun TRYFINALLYSTMT_pre_19_42_7 () Int)
(declare-fun UNARYADD_pre_18_54_26 () Int)
(declare-fun locFirstSemi_pre_114_36_13 () Int)
(declare-fun locFirstSemi_114_36_13 () Int)
(declare-fun elemType_pre_138_18_28 () Int)
(declare-fun elemType_138_18_28 () Int)
(declare-fun BYTETYPE_pre_17_35_26 () Int)
(declare-fun CLASSDECLSTMT_pre_19_28_7 () Int)
(declare-fun MOD_pre_18_36_26 () Int)
(declare-fun STMTPRAGMA_pre_29_26_26 () Int)
(declare-fun op_pre_26_26_13 () Int)
(declare-fun op_26_26_13 () Int)
(declare-fun init_pre_123_35_19 () Int)
(declare-fun init_123_35_19 () Int)
(declare-fun AMBIGUOUSVARIABLEACCESS_pre_19_55_7 () Int)
(declare-fun COMPILATIONUNIT_pre_19_14_7 () Int)
(declare-fun BITXOR_pre_18_22_26 () Int)
(declare-fun locCloseParen_pre_127_24_13 () Int)
(declare-fun locCloseParen_127_24_13 () Int)
(declare-fun locKeyword_pre_119_45_13 () Int)
(declare-fun locKeyword_119_45_13 () Int)
(declare-fun SWITCHLABEL_pre_19_41_7 () Int)
(declare-fun ASGBITXOR_pre_18_51_26 () Int)
(declare-fun punctuationStrings_pre_29_134_22 () Int)
(declare-fun locOpenParen_pre_105_23_13 () Int)
(declare-fun locOpenParen_105_23_13 () Int)
(declare-fun tag_pre_27_30_13 () Int)
(declare-fun tag_27_30_13 () Int)
(declare-fun loc_pre_62_45_13 () Int)
(declare-fun loc_62_45_13 () Int)
(declare-fun loc_pre_93_18_13 () Int)
(declare-fun loc_93_18_13 () Int)
(declare-fun elements_pre_14_61_36 () Int)
(declare-fun elements_14_61_36 () Int)
(declare-fun NULLTYPE_pre_17_34_26 () Int)
(declare-fun VARDECLSTMT_pre_19_27_7 () Int)
(declare-fun DIV_pre_18_35_26 () Int)
(declare-fun locOpenParen_pre_128_18_13 () Int)
(declare-fun locOpenParen_128_18_13 () Int)
(declare-fun type_pre_126_18_28 () Int)
(declare-fun type_126_18_28 () Int)
(declare-fun count_pre_124_67_33 () Int)
(declare-fun count_124_67_33 () Int)
(declare-fun otherStrings_pre_29_193_30 () Int)
(declare-fun loc_pre_23_50_13 () Int)
(declare-fun loc_23_50_13 () Int)
(declare-fun PARENEXPR_pre_19_54_7 () Int)
(declare-fun loc_pre_83_29_13 () Int)
(declare-fun loc_83_29_13 () Int)
(declare-fun BITOR_pre_18_21_26 () Int)
(declare-fun loc_pre_100_18_13 () Int)
(declare-fun loc_100_18_13 () Int)
(declare-fun MODIFIERPRAGMA_pre_29_25_26 () Int)
(declare-fun noTokens_pre_29_212_27 () Int)
(declare-fun tag_pre_23_32_13 () Int)
(declare-fun tag_23_32_13 () Int)
(declare-fun SKIPSTMT_pre_19_40_7 () Int)
(declare-fun ASGBITOR_pre_18_50_26 () Int)
(declare-fun loc_pre_118_23_13 () Int)
(declare-fun loc_118_23_13 () Int)
(declare-fun superCall_pre_119_24_17 () Int)
(declare-fun superCall_119_24_17 () Int)
(declare-fun locQuestion_pre_125_22_13 () Int)
(declare-fun locQuestion_125_22_13 () Int)
(declare-fun COMPOUNDNAME_pre_19_67_7 () Int)
(declare-fun VOIDTYPE_pre_17_33_26 () Int)
(declare-fun SWITCHSTMT_pre_19_26_7 () Int)
(declare-fun SUB_pre_18_34_26 () Int)
(declare-fun locDot_pre_84_21_13 () Int)
(declare-fun locDot_84_21_13 () Int)
(declare-fun CASTEXPR_pre_19_53_7 () Int)
(declare-fun locSuper_pre_137_20_13 () Int)
(declare-fun locSuper_137_20_13 () Int)
(declare-fun TYPESIG_pre_28_6_28 () Int)
(declare-fun FORSTMT_pre_19_39_7 () Int)
(declare-fun count_pre_14_67_33 () Int)
(declare-fun count_14_67_33 () Int)
(declare-fun locOpenBrace_pre_90_22_13 () Int)
(declare-fun locOpenBrace_90_22_13 () Int)
(declare-fun LEXICALPRAGMA_pre_29_24_26 () Int)
(declare-fun ASGBITAND_pre_18_49_26 () Int)
(declare-fun locDot_pre_133_23_13 () Int)
(declare-fun locDot_133_23_13 () Int)
(declare-fun SIMPLENAME_pre_19_66_7 () Int)
(declare-fun DOUBLETYPE_pre_17_32_26 () Int)
(declare-fun BLOCKSTMT_pre_19_25_7 () Int)
(declare-fun locId_pre_112_20_13 () Int)
(declare-fun locId_112_20_13 () Int)
(declare-fun ADD_pre_18_33_26 () Int)
(declare-fun locId_pre_80_43_13 () Int)
(declare-fun locId_80_43_13 () Int)
(declare-fun FIRST_KEYWORD_pre_29_51_26 () Int)
(declare-fun INSTANCEOFEXPR_pre_19_52_7 () Int)
(declare-fun loc_pre_113_22_13 () Int)
(declare-fun loc_113_22_13 () Int)
(declare-fun AND_pre_18_20_26 () Int)
(declare-fun locId_pre_77_38_13 () Int)
(declare-fun locId_77_38_13 () Int)
(declare-fun IFSTMT_pre_19_38_7 () Int)
(declare-fun LAST_KEYWORD_pre_29_103_26 () Int)
(declare-fun ASGURSHIFT_pre_18_48_26 () Int)
(declare-fun locOpenParen_pre_127_21_13 () Int)
(declare-fun locOpenParen_127_21_13 () Int)
(declare-fun locDot_pre_119_41_13 () Int)
(declare-fun locDot_119_41_13 () Int)
(declare-fun loc_pre_114_33_13 () Int)
(declare-fun loc_114_33_13 () Int)
(declare-fun ARRAYTYPE_pre_19_65_7 () Int)
(declare-fun locFinally_pre_117_25_13 () Int)
(declare-fun locFinally_117_25_13 () Int)
(declare-fun FORMALPARADECL_pre_19_24_7 () Int)
(declare-fun FLOATTYPE_pre_17_31_26 () Int)
(declare-fun URSHIFT_pre_18_32_26 () Int)
(declare-fun locOpenParen_pre_132_28_13 () Int)
(declare-fun locOpenParen_132_28_13 () Int)
(declare-fun locOp_pre_25_43_13 () Int)
(declare-fun locOp_25_43_13 () Int)
(declare-fun value_pre_23_45_16 () Int)
(declare-fun value_23_45_16 () Int)
(declare-fun locId_pre_130_24_13 () Int)
(declare-fun locId_130_24_13 () Int)
(declare-fun CONDEXPR_pre_19_51_7 () Int)
(declare-fun elements_pre_140_61_39 () Int)
(declare-fun elements_140_61_39 () Int)
(declare-fun locCloseBrace_pre_24_13 () Int)
(declare-fun locCloseBrace_24_13 () Int)
(declare-fun OR_pre_18_19_26 () Int)
(declare-fun LABELSTMT_pre_19_37_7 () Int)
(declare-fun NULLLIT_pre_17_45_26 () Int)
(declare-fun ASGRSHIFT_pre_18_47_26 () Int)
(declare-fun locGuardOpenParen_pre_103_23_13 () Int)
(declare-fun locGuardOpenParen_103_23_13 () Int)
(declare-fun elements_pre_73_61_39 () Int)
(declare-fun elements_73_61_39 () Int)
(declare-fun loc_pre_108_18_13 () Int)
(declare-fun loc_108_18_13 () Int)
(declare-fun NULL_pre_29_82_26 () Int)
(declare-fun TYPENAME_pre_19_64_7 () Int)
(declare-fun CHARTYPE_pre_17_30_26 () Int)
(declare-fun FIELDDECL_pre_19_23_7 () Int)
(declare-fun RSHIFT_pre_18_31_26 () Int)
(declare-fun locCloseBrace_pre_62_54_13 () Int)
(declare-fun locCloseBrace_62_54_13 () Int)
(declare-fun loc_pre_105_20_13 () Int)
(declare-fun loc_105_20_13 () Int)
(declare-fun loc_pre_123_49_13 () Int)
(declare-fun loc_123_49_13 () Int)
(declare-fun loc_pre_104_20_13 () Int)
(declare-fun loc_104_20_13 () Int)
(declare-fun NEWARRAYEXPR_pre_19_50_7 () Int)
(declare-fun locType_pre_79_21_13 () Int)
(declare-fun locType_79_21_13 () Int)
(declare-fun type_pre_123_24_28 () Int)
(declare-fun type_123_24_28 () Int)
(declare-fun I_will_establish_invariants_afterwards_pre_5_236_34 () Int)
(declare-fun I_will_establish_invariants_afterwards_5_236_34 () Int)
(declare-fun CONTINUESTMT_pre_19_36_7 () Int)
(declare-fun STRINGLIT_pre_17_44_26 () Int)
(declare-fun ASGLSHIFT_pre_18_46_26 () Int)
(declare-fun SUPEROBJECTDESIGNATOR_pre_19_63_7 () Int)
(declare-fun LONGTYPE_pre_17_29_26 () Int)
(declare-fun LOCALVARDECL_pre_19_22_7 () Int)
(declare-fun LSHIFT_pre_18_30_26 () Int)
(declare-fun loc_pre_80_40_13 () Int)
(declare-fun loc_80_40_13 () Int)
(declare-fun loc_pre_120_22_13 () Int)
(declare-fun loc_120_22_13 () Int)
(declare-fun NEWINSTANCEEXPR_pre_19_49_7 () Int)
(declare-fun loc_pre_129_22_13 () Int)
(declare-fun loc_129_22_13 () Int)
(declare-fun locOpenBrackets_pre_123_65_29 () Int)
(declare-fun locOpenBrackets_123_65_29 () Int)
(declare-fun POSTFIXDEC_pre_18_63_26 () Int)
(declare-fun BREAKSTMT_pre_19_35_7 () Int)
(declare-fun type_pre_77_35_28 () Int)
(declare-fun type_77_35_28 () Int)
(declare-fun count_pre_140_67_33 () Int)
(declare-fun count_140_67_33 () Int)
(declare-fun DOUBLELIT_pre_17_43_26 () Int)
(declare-fun ASGSUB_pre_18_45_26 () Int)
(declare-fun ids_pre_141_19_37 () Int)
(declare-fun ids_141_19_37 () Int)
(declare-fun type_pre_127_18_28 () Int)
(declare-fun type_127_18_28 () Int)
(declare-fun TYPEOBJECTDESIGNATOR_pre_19_62_7 () Int)
(declare-fun count_pre_73_67_33 () Int)
(declare-fun count_73_67_33 () Int)
(declare-fun INTTYPE_pre_17_28_26 () Int)
(declare-fun INITBLOCK_pre_19_21_7 () Int)
(declare-fun LT_pre_18_29_26 () Int)
(declare-fun locId_pre_132_25_13 () Int)
(declare-fun locId_132_25_13 () Int)
(declare-fun type_pre_133_20_28 () Int)
(declare-fun type_133_20_28 () Int)
(declare-fun ARRAYREFEXPR_pre_19_48_7 () Int)
(declare-fun POSTFIXINC_pre_18_62_26 () Int)
(declare-fun loc_pre_63_30_13 () Int)
(declare-fun loc_63_30_13 () Int)
(declare-fun THROWSTMT_pre_19_34_7 () Int)
(declare-fun FLOATLIT_pre_17_42_26 () Int)
(declare-fun ASGADD_pre_18_44_26 () Int)
(declare-fun length_pre_81_50_25 () Int)
(declare-fun length_81_50_25 () Int)
(declare-fun enclosingInstance_pre_119_37_14 () Int)
(declare-fun enclosingInstance_119_37_14 () Int)
(declare-fun loc_pre_116_29_13 () Int)
(declare-fun loc_116_29_13 () Int)
(declare-fun loc_pre_117_22_13 () Int)
(declare-fun loc_117_22_13 () Int)
(declare-fun EXPROBJECTDESIGNATOR_pre_19_61_7 () Int)
(declare-fun otherCodes_pre_29_202_27 () Int)
(declare-fun BOOLEANTYPE_pre_17_27_26 () Int)
(declare-fun METHODDECL_pre_19_20_7 () Int)
(declare-fun LE_pre_18_28_26 () Int)
(declare-fun locOpenBrace_pre_21_13 () Int)
(declare-fun locOpenBrace_21_13 () Int)
(declare-fun locOpenBrace_pre_62_51_13 () Int)
(declare-fun locOpenBrace_62_51_13 () Int)
(declare-fun loc_pre_107_18_13 () Int)
(declare-fun loc_107_18_13 () Int)
(declare-fun dims_pre_123_45_31 () Int)
(declare-fun dims_123_45_31 () Int)
(declare-fun THISEXPR_pre_19_47_7 () Int)
(declare-fun DEC_pre_18_59_26 () Int)
(declare-fun locCloseBracket_pre_121_23_13 () Int)
(declare-fun locCloseBracket_121_23_13 () Int)
(declare-fun CHARLIT_pre_17_41_26 () Int)
(declare-fun RETURNSTMT_pre_19_33_7 () Int)
(declare-fun locOp_pre_26_32_13 () Int)
(declare-fun locOp_26_32_13 () Int)
(declare-fun punctuationCodes_pre_29_164_19 () Int)
(declare-fun ASGREM_pre_18_43_26 () Int)
(declare-fun CLASSLITERAL_pre_19_60_7 () Int)
(declare-fun IDENT_pre_17_25_26 () Int)
(declare-fun CONSTRUCTORDECL_pre_19_19_7 () Int)
(declare-fun locDot_pre_122_29_13 () Int)
(declare-fun locDot_122_29_13 () Int)
(declare-fun GT_pre_18_27_26 () Int)
(declare-fun locOpenBracket_pre_138_21_13 () Int)
(declare-fun locOpenBracket_138_21_13 () Int)
(declare-fun elements_pre_72_61_38 () Int)
(declare-fun elements_72_61_38 () Int)
(declare-fun ARRAYINIT_pre_19_46_7 () Int)
(declare-fun INC_pre_18_58_26 () Int)
(declare-fun owner_pre_8_35_28 () Int)
(declare-fun owner_8_35_28 () Int)
(declare-fun locIds_pre_141_25_29 () Int)
(declare-fun locIds_141_25_29 () Int)
(declare-fun loc_pre_103_20_13 () Int)
(declare-fun loc_103_20_13 () Int)
(declare-fun LONGLIT_pre_17_40_26 () Int)
(declare-fun EVALSTMT_pre_19_32_7 () Int)
(declare-fun ASGDIV_pre_18_42_26 () Int)
(declare-fun locOpenParen_pre_122_52_13 () Int)
(declare-fun locOpenParen_122_52_13 () Int)
(declare-fun METHODINVOCATION_pre_19_59_7 () Int)
(declare-fun tokenType_pre_78_90_8 () Int)
(declare-fun tokenType_78_90_8 () Int)
(declare-fun INTERFACEDECL_pre_19_18_7 () Int)
(declare-fun GE_pre_18_26_26 () Int)
(declare-fun locCloseParen_pre_128_21_13 () Int)
(declare-fun locCloseParen_128_21_13 () Int)
(declare-fun CATCHCLAUSE_pre_19_45_7 () Int)
(declare-fun BITNOT_pre_18_57_26 () Int)
(declare-fun keywordStrings_pre_29_181_30 () Int)
(declare-fun locOpenParen_pre_131_30_13 () Int)
(declare-fun locOpenParen_131_30_13 () Int)
(declare-fun NULL_pre_13_60_26 () Int)
(declare-fun SYNCHRONIZESTMT_pre_19_31_7 () Int)
(declare-fun INTLIT_pre_17_39_26 () Int)
(declare-fun ASGMUL_pre_18_41_26 () Int)
(declare-fun loc_pre_115_16_13 () Int)
(declare-fun loc_115_16_13 () Int)
(declare-fun AMBIGUOUSMETHODINVOCATION_pre_19_58_7 () Int)
(declare-fun CLASSDECL_pre_19_17_7 () Int)
(declare-fun EQ_pre_18_25_26 () Int)
(declare-fun locOpenParen_pre_119_48_13 () Int)
(declare-fun locOpenParen_119_48_13 () Int)
(declare-fun loc_pre_27_35_13 () Int)
(declare-fun loc_27_35_13 () Int)
(declare-fun TYPEMODIFIERPRAGMA_pre_29_28_26 () Int)
(declare-fun locId_pre_62_48_13 () Int)
(declare-fun locId_62_48_13 () Int)
(declare-fun CONSTRUCTORINVOCATION_pre_19_44_7 () Int)
(declare-fun count_pre_72_67_33 () Int)
(declare-fun count_72_67_33 () Int)
(declare-fun NOT_pre_18_56_26 () Int)
(declare-fun returnType_pre_79_18_28 () Int)
(declare-fun returnType_79_18_28 () Int)
(declare-fun locDots_pre_141_31_29 () Int)
(declare-fun locDots_141_31_29 () Int)
(declare-fun BOOLEANLIT_pre_17_38_26 () Int)
(declare-fun DOSTMT_pre_19_30_7 () Int)
(declare-fun ASSIGN_pre_18_40_26 () Int)
(declare-fun loc_pre_126_21_13 () Int)
(declare-fun loc_126_21_13 () Int)
(declare-fun op_pre_25_35_13 () Int)
(declare-fun op_25_35_13 () Int)
(declare-fun FIELDACCESS_pre_19_57_7 () Int)
(declare-fun syntax_pre_22_28_29 () Int)
(declare-fun syntax_22_28_29 () Int)
(declare-fun ONDEMANDIMPORTDECL_pre_19_16_7 () Int)
(declare-fun NE_pre_18_24_26 () Int)
(declare-fun locColon_pre_125_25_13 () Int)
(declare-fun locColon_125_25_13 () Int)
(declare-fun locOpenBracket_pre_121_20_13 () Int)
(declare-fun locOpenBracket_121_20_13 () Int)
(declare-fun elems_pre () Int)
(declare-fun elems () Int)
(declare-fun LS () Int)
(declare-fun alloc_pre () Int)
(declare-fun elems_91_56 () Int)
(declare-fun locOpenBrace_91_67 () Int)
(declare-fun locCloseBrace_91_85 () Int)
(declare-fun after_93_24_93_24 () Int)
(declare-fun RES_93_24_93_24 () Int)
(declare-fun EC_93_24_93_24 () Int)
(declare-fun ecReturn () Int)
(declare-fun elems_94_12 () Int)
(declare-fun locOpenBrace_95_12 () Int)
(declare-fun locCloseBrace_96_12 () Int)
(assert (let ((?v_0 (array T_java_lang_String)) (?v_1 (array T_int)) (?v_2 (= true_term true_term)) (?v_5 (< alloc after_93_24_93_24)) (?v_3 (not (= RES_93_24_93_24 null))) (?v_6 (not (= true_term (isAllocated RES_93_24_93_24 alloc)))) (?v_7 (= true_term (is RES_93_24_93_24 T_javafe_ast_ArrayInit))) (?v_8 (= true_term (isAllocated RES_93_24_93_24 after_93_24_93_24))) (?v_9 (= EC_93_24_93_24 ecReturn)) (?v_10 (= (S_select owner_8_35_28 RES_93_24_93_24) null)) (?v_11 (= (typeof RES_93_24_93_24) T_javafe_ast_ArrayInit))) (let ((?v_4 (not ?v_3)) (?v_12 (= elems_94_12 (S_store elems_18_34 RES_93_24_93_24 elems_91_56))) (?v_13 (= locOpenBrace_95_12 (S_store locOpenBrace_21_13 RES_93_24_93_24 locOpenBrace_91_67))) (?v_14 (= ecReturn ecReturn))) (let ((?v_15 (=> ?v_14 ?v_3))) (not (=> true (=> (and (= locOpenBrace_pre_80_36_13 locOpenBrace_80_36_13) (= locOpenBrace_80_36_13 (asField locOpenBrace_80_36_13 T_int)) (= TRYCATCHSTMT_pre_19_43_7 TRYCATCHSTMT_19_43_7) (= true_term (is TRYCATCHSTMT_19_43_7 T_int)) (= UNARYSUB_pre_18_55_26 UNARYSUB_18_55_26) (= true_term (is UNARYSUB_18_55_26 T_int)) (= TYPEDECLELEMPRAGMA_pre_29_27_26 TYPEDECLELEMPRAGMA_29_27_26) (= true_term (is TYPEDECLELEMPRAGMA_29_27_26 T_int)) (= SHORTTYPE_pre_17_36_26 SHORTTYPE_17_36_26) (= true_term (is SHORTTYPE_17_36_26 T_int)) (= WHILESTMT_pre_19_29_7 WHILESTMT_19_29_7) (= true_term (is WHILESTMT_19_29_7 T_int)) (= body_pre_80_34_19 body_80_34_19) (= body_80_34_19 (asField body_80_34_19 T_javafe_ast_BlockStmt)) (< (fClosedTime body_80_34_19) alloc) (= STAR_pre_18_37_26 STAR_18_37_26) (= true_term (is STAR_18_37_26 T_int)) (= elems_pre_18_34 elems_18_34) (= elems_18_34 (asField elems_18_34 T_javafe_ast_VarInitVec)) (< (fClosedTime elems_18_34) alloc) (forall ((?s Int)) (=> (not (= ?s null)) (not (= (S_select elems_18_34 ?s) null)))) (= enclosingInstance_pre_122_25_14 enclosingInstance_122_25_14) (= enclosingInstance_122_25_14 (asField enclosingInstance_122_25_14 T_javafe_ast_Expr)) (< (fClosedTime enclosingInstance_122_25_14) alloc) (= loc_pre_110_18_13 loc_110_18_13) (= loc_110_18_13 (asField loc_110_18_13 T_int)) (= elements_pre_124_61_33 elements_124_61_33) (= elements_124_61_33 (asField elements_124_61_33 (array T_javafe_ast_Expr))) (< (fClosedTime elements_124_61_33) alloc) (forall ((?s_1_ Int)) (=> (not (= ?s_1_ null)) (not (= (S_select elements_124_61_33 ?s_1_) null)))) (= loc_pre_122_49_13 loc_122_49_13) (= loc_122_49_13 (asField loc_122_49_13 T_int)) (= VARIABLEACCESS_pre_19_56_7 VARIABLEACCESS_19_56_7) (= true_term (is VARIABLEACCESS_19_56_7 T_int)) (= SINGLETYPEIMPORTDECL_pre_19_15_7 SINGLETYPEIMPORTDECL_19_15_7) (= true_term (is SINGLETYPEIMPORTDECL_19_15_7 T_int)) (= BITAND_pre_18_23_26 BITAND_18_23_26) (= true_term (is BITAND_18_23_26 T_int)) (= locCloseBrace_pre_90_25_13 locCloseBrace_90_25_13) (= locCloseBrace_90_25_13 (asField locCloseBrace_90_25_13 T_int)) (= loc_pre_139_20_13 loc_139_20_13) (= loc_139_20_13 (asField loc_139_20_13 T_int)) (= TRYFINALLYSTMT_pre_19_42_7 TRYFINALLYSTMT_19_42_7) (= true_term (is TRYFINALLYSTMT_19_42_7 T_int)) (= UNARYADD_pre_18_54_26 UNARYADD_18_54_26) (= true_term (is UNARYADD_18_54_26 T_int)) (= locFirstSemi_pre_114_36_13 locFirstSemi_114_36_13) (= locFirstSemi_114_36_13 (asField locFirstSemi_114_36_13 T_int)) (= elemType_pre_138_18_28 elemType_138_18_28) (= elemType_138_18_28 (asField elemType_138_18_28 T_javafe_ast_Type)) (< (fClosedTime elemType_138_18_28) alloc) (forall ((?s_2_ Int)) (=> (not (= ?s_2_ null)) (not (= (S_select elemType_138_18_28 ?s_2_) null)))) (= BYTETYPE_pre_17_35_26 BYTETYPE_17_35_26) (= true_term (is BYTETYPE_17_35_26 T_int)) (= CLASSDECLSTMT_pre_19_28_7 CLASSDECLSTMT_19_28_7) (= true_term (is CLASSDECLSTMT_19_28_7 T_int)) (= MOD_pre_18_36_26 MOD_18_36_26) (= true_term (is MOD_18_36_26 T_int)) (= STMTPRAGMA_pre_29_26_26 STMTPRAGMA_29_26_26) (= true_term (is STMTPRAGMA_29_26_26 T_int)) (= op_pre_26_26_13 op_26_26_13) (= op_26_26_13 (asField op_26_26_13 T_int)) (= init_pre_123_35_19 init_123_35_19) (= init_123_35_19 (asField init_123_35_19 T_javafe_ast_ArrayInit)) (< (fClosedTime init_123_35_19) alloc) (= AMBIGUOUSVARIABLEACCESS_pre_19_55_7 AMBIGUOUSVARIABLEACCESS_19_55_7) (= true_term (is AMBIGUOUSVARIABLEACCESS_19_55_7 T_int)) (= COMPILATIONUNIT_pre_19_14_7 COMPILATIONUNIT_19_14_7) (= true_term (is COMPILATIONUNIT_19_14_7 T_int)) (= BITXOR_pre_18_22_26 BITXOR_18_22_26) (= true_term (is BITXOR_18_22_26 T_int)) (= locCloseParen_pre_127_24_13 locCloseParen_127_24_13) (= locCloseParen_127_24_13 (asField locCloseParen_127_24_13 T_int)) (= locKeyword_pre_119_45_13 locKeyword_119_45_13) (= locKeyword_119_45_13 (asField locKeyword_119_45_13 T_int)) (= SWITCHLABEL_pre_19_41_7 SWITCHLABEL_19_41_7) (= true_term (is SWITCHLABEL_19_41_7 T_int)) (= ASGBITXOR_pre_18_51_26 ASGBITXOR_18_51_26) (= true_term (is ASGBITXOR_18_51_26 T_int)) (= punctuationStrings_pre_29_134_22 punctuationStrings_29_134_22) (= true_term (is punctuationStrings_29_134_22 ?v_0)) (= true_term (isAllocated punctuationStrings_29_134_22 alloc)) (= locOpenParen_pre_105_23_13 locOpenParen_105_23_13) (= locOpenParen_105_23_13 (asField locOpenParen_105_23_13 T_int)) (= tag_pre_27_30_13 tag_27_30_13) (= tag_27_30_13 (asField tag_27_30_13 T_int)) (= loc_pre_62_45_13 loc_62_45_13) (= loc_62_45_13 (asField loc_62_45_13 T_int)) (= loc_pre_93_18_13 loc_93_18_13) (= loc_93_18_13 (asField loc_93_18_13 T_int)) (= elements_pre_14_61_36 elements_14_61_36) (= elements_14_61_36 (asField elements_14_61_36 (array T_javafe_ast_VarInit))) (< (fClosedTime elements_14_61_36) alloc) (forall ((?s_3_ Int)) (=> (not (= ?s_3_ null)) (not (= (S_select elements_14_61_36 ?s_3_) null)))) (= NULLTYPE_pre_17_34_26 NULLTYPE_17_34_26) (= true_term (is NULLTYPE_17_34_26 T_int)) (= VARDECLSTMT_pre_19_27_7 VARDECLSTMT_19_27_7) (= true_term (is VARDECLSTMT_19_27_7 T_int)) (= DIV_pre_18_35_26 DIV_18_35_26) (= true_term (is DIV_18_35_26 T_int)) (= locOpenParen_pre_128_18_13 locOpenParen_128_18_13) (= locOpenParen_128_18_13 (asField locOpenParen_128_18_13 T_int)) (= type_pre_126_18_28 type_126_18_28) (= type_126_18_28 (asField type_126_18_28 T_javafe_ast_Type)) (< (fClosedTime type_126_18_28) alloc) (forall ((?s_4_ Int)) (=> (not (= ?s_4_ null)) (not (= (S_select type_126_18_28 ?s_4_) null)))) (= count_pre_124_67_33 count_124_67_33) (= count_124_67_33 (asField count_124_67_33 T_int)) (= otherStrings_pre_29_193_30 otherStrings_29_193_30) (= true_term (is otherStrings_29_193_30 ?v_0)) (= true_term (isAllocated otherStrings_29_193_30 alloc)) (= loc_pre_23_50_13 loc_23_50_13) (= loc_23_50_13 (asField loc_23_50_13 T_int)) (= PARENEXPR_pre_19_54_7 PARENEXPR_19_54_7) (= true_term (is PARENEXPR_19_54_7 T_int)) (= loc_pre_83_29_13 loc_83_29_13) (= loc_83_29_13 (asField loc_83_29_13 T_int)) (= BITOR_pre_18_21_26 BITOR_18_21_26) (= true_term (is BITOR_18_21_26 T_int)) (= loc_pre_100_18_13 loc_100_18_13) (= loc_100_18_13 (asField loc_100_18_13 T_int)) (= MODIFIERPRAGMA_pre_29_25_26 MODIFIERPRAGMA_29_25_26) (= true_term (is MODIFIERPRAGMA_29_25_26 T_int)) (= noTokens_pre_29_212_27 noTokens_29_212_27) (= true_term (is noTokens_29_212_27 T_int)) (= tag_pre_23_32_13 tag_23_32_13) (= tag_23_32_13 (asField tag_23_32_13 T_int)) (= SKIPSTMT_pre_19_40_7 SKIPSTMT_19_40_7) (= true_term (is SKIPSTMT_19_40_7 T_int)) (= ASGBITOR_pre_18_50_26 ASGBITOR_18_50_26) (= true_term (is ASGBITOR_18_50_26 T_int)) (= loc_pre_118_23_13 loc_118_23_13) (= loc_118_23_13 (asField loc_118_23_13 T_int)) (= superCall_pre_119_24_17 superCall_119_24_17) (= superCall_119_24_17 (asField superCall_119_24_17 T_boolean)) (= locQuestion_pre_125_22_13 locQuestion_125_22_13) (= locQuestion_125_22_13 (asField locQuestion_125_22_13 T_int)) (= COMPOUNDNAME_pre_19_67_7 COMPOUNDNAME_19_67_7) (= true_term (is COMPOUNDNAME_19_67_7 T_int)) (= VOIDTYPE_pre_17_33_26 VOIDTYPE_17_33_26) (= true_term (is VOIDTYPE_17_33_26 T_int)) (= SWITCHSTMT_pre_19_26_7 SWITCHSTMT_19_26_7) (= true_term (is SWITCHSTMT_19_26_7 T_int)) (= SUB_pre_18_34_26 SUB_18_34_26) (= true_term (is SUB_18_34_26 T_int)) (= locDot_pre_84_21_13 locDot_84_21_13) (= locDot_84_21_13 (asField locDot_84_21_13 T_int)) (= CASTEXPR_pre_19_53_7 CASTEXPR_19_53_7) (= true_term (is CASTEXPR_19_53_7 T_int)) (= locSuper_pre_137_20_13 locSuper_137_20_13) (= locSuper_137_20_13 (asField locSuper_137_20_13 T_int)) (= TYPESIG_pre_28_6_28 TYPESIG_28_6_28) (= true_term (is TYPESIG_28_6_28 T_int)) (= FORSTMT_pre_19_39_7 FORSTMT_19_39_7) (= true_term (is FORSTMT_19_39_7 T_int)) (= count_pre_14_67_33 count_14_67_33) (= count_14_67_33 (asField count_14_67_33 T_int)) (= locOpenBrace_pre_90_22_13 locOpenBrace_90_22_13) (= locOpenBrace_90_22_13 (asField locOpenBrace_90_22_13 T_int)) (= LEXICALPRAGMA_pre_29_24_26 LEXICALPRAGMA_29_24_26) (= true_term (is LEXICALPRAGMA_29_24_26 T_int)) (= ASGBITAND_pre_18_49_26 ASGBITAND_18_49_26) (= true_term (is ASGBITAND_18_49_26 T_int)) (= locDot_pre_133_23_13 locDot_133_23_13) (= locDot_133_23_13 (asField locDot_133_23_13 T_int)) (= SIMPLENAME_pre_19_66_7 SIMPLENAME_19_66_7) (= true_term (is SIMPLENAME_19_66_7 T_int)) (= DOUBLETYPE_pre_17_32_26 DOUBLETYPE_17_32_26) (= true_term (is DOUBLETYPE_17_32_26 T_int)) (= BLOCKSTMT_pre_19_25_7 BLOCKSTMT_19_25_7) (= true_term (is BLOCKSTMT_19_25_7 T_int)) (= locId_pre_112_20_13 locId_112_20_13) (= locId_112_20_13 (asField locId_112_20_13 T_int)) (= ADD_pre_18_33_26 ADD_18_33_26) (= true_term (is ADD_18_33_26 T_int)) (= locId_pre_80_43_13 locId_80_43_13) (= locId_80_43_13 (asField locId_80_43_13 T_int)) (= FIRST_KEYWORD_pre_29_51_26 FIRST_KEYWORD_29_51_26) (= true_term (is FIRST_KEYWORD_29_51_26 T_int)) (= INSTANCEOFEXPR_pre_19_52_7 INSTANCEOFEXPR_19_52_7) (= true_term (is INSTANCEOFEXPR_19_52_7 T_int)) (= loc_pre_113_22_13 loc_113_22_13) (= loc_113_22_13 (asField loc_113_22_13 T_int)) (= AND_pre_18_20_26 AND_18_20_26) (= true_term (is AND_18_20_26 T_int)) (= locId_pre_77_38_13 locId_77_38_13) (= locId_77_38_13 (asField locId_77_38_13 T_int)) (= IFSTMT_pre_19_38_7 IFSTMT_19_38_7) (= true_term (is IFSTMT_19_38_7 T_int)) (= LAST_KEYWORD_pre_29_103_26 LAST_KEYWORD_29_103_26) (= true_term (is LAST_KEYWORD_29_103_26 T_int)) (= ASGURSHIFT_pre_18_48_26 ASGURSHIFT_18_48_26) (= true_term (is ASGURSHIFT_18_48_26 T_int)) (= locOpenParen_pre_127_21_13 locOpenParen_127_21_13) (= locOpenParen_127_21_13 (asField locOpenParen_127_21_13 T_int)) (= locDot_pre_119_41_13 locDot_119_41_13) (= locDot_119_41_13 (asField locDot_119_41_13 T_int)) (= loc_pre_114_33_13 loc_114_33_13) (= loc_114_33_13 (asField loc_114_33_13 T_int)) (= ARRAYTYPE_pre_19_65_7 ARRAYTYPE_19_65_7) (= true_term (is ARRAYTYPE_19_65_7 T_int)) (= locFinally_pre_117_25_13 locFinally_117_25_13) (= locFinally_117_25_13 (asField locFinally_117_25_13 T_int)) (= FORMALPARADECL_pre_19_24_7 FORMALPARADECL_19_24_7) (= true_term (is FORMALPARADECL_19_24_7 T_int)) (= FLOATTYPE_pre_17_31_26 FLOATTYPE_17_31_26) (= true_term (is FLOATTYPE_17_31_26 T_int)) (= URSHIFT_pre_18_32_26 URSHIFT_18_32_26) (= true_term (is URSHIFT_18_32_26 T_int)) (= locOpenParen_pre_132_28_13 locOpenParen_132_28_13) (= locOpenParen_132_28_13 (asField locOpenParen_132_28_13 T_int)) (= locOp_pre_25_43_13 locOp_25_43_13) (= locOp_25_43_13 (asField locOp_25_43_13 T_int)) (= value_pre_23_45_16 value_23_45_16) (= value_23_45_16 (asField value_23_45_16 T_java_lang_Object)) (< (fClosedTime value_23_45_16) alloc) (= locId_pre_130_24_13 locId_130_24_13) (= locId_130_24_13 (asField locId_130_24_13 T_int)) (= CONDEXPR_pre_19_51_7 CONDEXPR_19_51_7) (= true_term (is CONDEXPR_19_51_7 T_int)) (= elements_pre_140_61_39 elements_140_61_39) (= elements_140_61_39 (asField elements_140_61_39 (array T_javafe_ast_Identifier))) (< (fClosedTime elements_140_61_39) alloc) (forall ((?s_5_ Int)) (=> (not (= ?s_5_ null)) (not (= (S_select elements_140_61_39 ?s_5_) null)))) (= locCloseBrace_pre_24_13 locCloseBrace_24_13) (= locCloseBrace_24_13 (asField locCloseBrace_24_13 T_int)) (= OR_pre_18_19_26 OR_18_19_26) (= true_term (is OR_18_19_26 T_int)) (= LABELSTMT_pre_19_37_7 LABELSTMT_19_37_7) (= true_term (is LABELSTMT_19_37_7 T_int)) (= NULLLIT_pre_17_45_26 NULLLIT_17_45_26) (= true_term (is NULLLIT_17_45_26 T_int)) (= ASGRSHIFT_pre_18_47_26 ASGRSHIFT_18_47_26) (= true_term (is ASGRSHIFT_18_47_26 T_int)) (= locGuardOpenParen_pre_103_23_13 locGuardOpenParen_103_23_13) (= locGuardOpenParen_103_23_13 (asField locGuardOpenParen_103_23_13 T_int)) (= elements_pre_73_61_39 elements_73_61_39) (= elements_73_61_39 (asField elements_73_61_39 (array T_javafe_ast_MethodDecl))) (< (fClosedTime elements_73_61_39) alloc) (forall ((?s_6_ Int)) (=> (not (= ?s_6_ null)) (not (= (S_select elements_73_61_39 ?s_6_) null)))) (= loc_pre_108_18_13 loc_108_18_13) (= loc_108_18_13 (asField loc_108_18_13 T_int)) (= NULL_pre_29_82_26 NULL_29_82_26) (= true_term (is NULL_29_82_26 T_int)) (= TYPENAME_pre_19_64_7 TYPENAME_19_64_7) (= true_term (is TYPENAME_19_64_7 T_int)) (= CHARTYPE_pre_17_30_26 CHARTYPE_17_30_26) (= true_term (is CHARTYPE_17_30_26 T_int)) (= FIELDDECL_pre_19_23_7 FIELDDECL_19_23_7) (= true_term (is FIELDDECL_19_23_7 T_int)) (= RSHIFT_pre_18_31_26 RSHIFT_18_31_26) (= true_term (is RSHIFT_18_31_26 T_int)) (= locCloseBrace_pre_62_54_13 locCloseBrace_62_54_13) (= locCloseBrace_62_54_13 (asField locCloseBrace_62_54_13 T_int)) (= loc_pre_105_20_13 loc_105_20_13) (= loc_105_20_13 (asField loc_105_20_13 T_int)) (= loc_pre_123_49_13 loc_123_49_13) (= loc_123_49_13 (asField loc_123_49_13 T_int)) (= loc_pre_104_20_13 loc_104_20_13) (= loc_104_20_13 (asField loc_104_20_13 T_int)) (= NEWARRAYEXPR_pre_19_50_7 NEWARRAYEXPR_19_50_7) (= true_term (is NEWARRAYEXPR_19_50_7 T_int)) (= locType_pre_79_21_13 locType_79_21_13) (= locType_79_21_13 (asField locType_79_21_13 T_int)) (= type_pre_123_24_28 type_123_24_28) (= type_123_24_28 (asField type_123_24_28 T_javafe_ast_Type)) (< (fClosedTime type_123_24_28) alloc) (forall ((?s_7_ Int)) (=> (not (= ?s_7_ null)) (not (= (S_select type_123_24_28 ?s_7_) null)))) (= I_will_establish_invariants_afterwards_pre_5_236_34 I_will_establish_invariants_afterwards_5_236_34) (= true_term (is I_will_establish_invariants_afterwards_5_236_34 T_boolean)) (= CONTINUESTMT_pre_19_36_7 CONTINUESTMT_19_36_7) (= true_term (is CONTINUESTMT_19_36_7 T_int)) (= STRINGLIT_pre_17_44_26 STRINGLIT_17_44_26) (= true_term (is STRINGLIT_17_44_26 T_int)) (= ASGLSHIFT_pre_18_46_26 ASGLSHIFT_18_46_26) (= true_term (is ASGLSHIFT_18_46_26 T_int)) (= SUPEROBJECTDESIGNATOR_pre_19_63_7 SUPEROBJECTDESIGNATOR_19_63_7) (= true_term (is SUPEROBJECTDESIGNATOR_19_63_7 T_int)) (= LONGTYPE_pre_17_29_26 LONGTYPE_17_29_26) (= true_term (is LONGTYPE_17_29_26 T_int)) (= LOCALVARDECL_pre_19_22_7 LOCALVARDECL_19_22_7) (= true_term (is LOCALVARDECL_19_22_7 T_int)) (= LSHIFT_pre_18_30_26 LSHIFT_18_30_26) (= true_term (is LSHIFT_18_30_26 T_int)) (= loc_pre_80_40_13 loc_80_40_13) (= loc_80_40_13 (asField loc_80_40_13 T_int)) (= loc_pre_120_22_13 loc_120_22_13) (= loc_120_22_13 (asField loc_120_22_13 T_int)) (= NEWINSTANCEEXPR_pre_19_49_7 NEWINSTANCEEXPR_19_49_7) (= true_term (is NEWINSTANCEEXPR_19_49_7 T_int)) (= loc_pre_129_22_13 loc_129_22_13) (= loc_129_22_13 (asField loc_129_22_13 T_int)) (= locOpenBrackets_pre_123_65_29 locOpenBrackets_123_65_29) (= locOpenBrackets_123_65_29 (asField locOpenBrackets_123_65_29 ?v_1)) (< (fClosedTime locOpenBrackets_123_65_29) alloc) (forall ((?s_8_ Int)) (=> (not (= ?s_8_ null)) (not (= (S_select locOpenBrackets_123_65_29 ?s_8_) null)))) (= POSTFIXDEC_pre_18_63_26 POSTFIXDEC_18_63_26) (= true_term (is POSTFIXDEC_18_63_26 T_int)) (= BREAKSTMT_pre_19_35_7 BREAKSTMT_19_35_7) (= true_term (is BREAKSTMT_19_35_7 T_int)) (= type_pre_77_35_28 type_77_35_28) (= type_77_35_28 (asField type_77_35_28 T_javafe_ast_Type)) (< (fClosedTime type_77_35_28) alloc) (forall ((?s_9_ Int)) (=> (not (= ?s_9_ null)) (not (= (S_select type_77_35_28 ?s_9_) null)))) (= count_pre_140_67_33 count_140_67_33) (= count_140_67_33 (asField count_140_67_33 T_int)) (= DOUBLELIT_pre_17_43_26 DOUBLELIT_17_43_26) (= true_term (is DOUBLELIT_17_43_26 T_int)) (= ASGSUB_pre_18_45_26 ASGSUB_18_45_26) (= true_term (is ASGSUB_18_45_26 T_int)) (= ids_pre_141_19_37 ids_141_19_37) (= ids_141_19_37 (asField ids_141_19_37 T_javafe_ast_IdentifierVec)) (< (fClosedTime ids_141_19_37) alloc) (forall ((?s_10_ Int)) (=> (not (= ?s_10_ null)) (not (= (S_select ids_141_19_37 ?s_10_) null)))) (= type_pre_127_18_28 type_127_18_28) (= type_127_18_28 (asField type_127_18_28 T_javafe_ast_Type)) (< (fClosedTime type_127_18_28) alloc) (forall ((?s_11_ Int)) (=> (not (= ?s_11_ null)) (not (= (S_select type_127_18_28 ?s_11_) null)))) (= TYPEOBJECTDESIGNATOR_pre_19_62_7 TYPEOBJECTDESIGNATOR_19_62_7) (= true_term (is TYPEOBJECTDESIGNATOR_19_62_7 T_int)) (= count_pre_73_67_33 count_73_67_33) (= count_73_67_33 (asField count_73_67_33 T_int)) (= INTTYPE_pre_17_28_26 INTTYPE_17_28_26) (= true_term (is INTTYPE_17_28_26 T_int)) (= INITBLOCK_pre_19_21_7 INITBLOCK_19_21_7) (= true_term (is INITBLOCK_19_21_7 T_int)) (= LT_pre_18_29_26 LT_18_29_26) (= true_term (is LT_18_29_26 T_int)) (= locId_pre_132_25_13 locId_132_25_13) (= locId_132_25_13 (asField locId_132_25_13 T_int)) (= type_pre_133_20_28 type_133_20_28) (= type_133_20_28 (asField type_133_20_28 T_javafe_ast_Type)) (< (fClosedTime type_133_20_28) alloc) (forall ((?s_12_ Int)) (=> (not (= ?s_12_ null)) (not (= (S_select type_133_20_28 ?s_12_) null)))) (= ARRAYREFEXPR_pre_19_48_7 ARRAYREFEXPR_19_48_7) (= true_term (is ARRAYREFEXPR_19_48_7 T_int)) (= POSTFIXINC_pre_18_62_26 POSTFIXINC_18_62_26) (= true_term (is POSTFIXINC_18_62_26 T_int)) (= loc_pre_63_30_13 loc_63_30_13) (= loc_63_30_13 (asField loc_63_30_13 T_int)) (= THROWSTMT_pre_19_34_7 THROWSTMT_19_34_7) (= true_term (is THROWSTMT_19_34_7 T_int)) (= FLOATLIT_pre_17_42_26 FLOATLIT_17_42_26) (= true_term (is FLOATLIT_17_42_26 T_int)) (= ASGADD_pre_18_44_26 ASGADD_18_44_26) (= true_term (is ASGADD_18_44_26 T_int)) (= length_pre_81_50_25 length_81_50_25) (= length_81_50_25 (asField length_81_50_25 T_int)) (= enclosingInstance_pre_119_37_14 enclosingInstance_119_37_14) (= enclosingInstance_119_37_14 (asField enclosingInstance_119_37_14 T_javafe_ast_Expr)) (< (fClosedTime enclosingInstance_119_37_14) alloc) (= loc_pre_116_29_13 loc_116_29_13) (= loc_116_29_13 (asField loc_116_29_13 T_int)) (= loc_pre_117_22_13 loc_117_22_13) (= loc_117_22_13 (asField loc_117_22_13 T_int)) (= EXPROBJECTDESIGNATOR_pre_19_61_7 EXPROBJECTDESIGNATOR_19_61_7) (= true_term (is EXPROBJECTDESIGNATOR_19_61_7 T_int)) (= otherCodes_pre_29_202_27 otherCodes_29_202_27) (= true_term (is otherCodes_29_202_27 ?v_1)) (= true_term (isAllocated otherCodes_29_202_27 alloc)) (= BOOLEANTYPE_pre_17_27_26 BOOLEANTYPE_17_27_26) (= true_term (is BOOLEANTYPE_17_27_26 T_int)) (= METHODDECL_pre_19_20_7 METHODDECL_19_20_7) (= true_term (is METHODDECL_19_20_7 T_int)) (= LE_pre_18_28_26 LE_18_28_26) (= true_term (is LE_18_28_26 T_int)) (= locOpenBrace_pre_21_13 locOpenBrace_21_13) (= locOpenBrace_21_13 (asField locOpenBrace_21_13 T_int)) (= locOpenBrace_pre_62_51_13 locOpenBrace_62_51_13) (= locOpenBrace_62_51_13 (asField locOpenBrace_62_51_13 T_int)) (= loc_pre_107_18_13 loc_107_18_13) (= loc_107_18_13 (asField loc_107_18_13 T_int)) (= dims_pre_123_45_31 dims_123_45_31) (= dims_123_45_31 (asField dims_123_45_31 T_javafe_ast_ExprVec)) (< (fClosedTime dims_123_45_31) alloc) (forall ((?s_13_ Int)) (=> (not (= ?s_13_ null)) (not (= (S_select dims_123_45_31 ?s_13_) null)))) (= THISEXPR_pre_19_47_7 THISEXPR_19_47_7) (= true_term (is THISEXPR_19_47_7 T_int)) (= DEC_pre_18_59_26 DEC_18_59_26) (= true_term (is DEC_18_59_26 T_int)) (= locCloseBracket_pre_121_23_13 locCloseBracket_121_23_13) (= locCloseBracket_121_23_13 (asField locCloseBracket_121_23_13 T_int)) (= CHARLIT_pre_17_41_26 CHARLIT_17_41_26) (= true_term (is CHARLIT_17_41_26 T_int)) (= RETURNSTMT_pre_19_33_7 RETURNSTMT_19_33_7) (= true_term (is RETURNSTMT_19_33_7 T_int)) (= locOp_pre_26_32_13 locOp_26_32_13) (= locOp_26_32_13 (asField locOp_26_32_13 T_int)) (= punctuationCodes_pre_29_164_19 punctuationCodes_29_164_19) (= true_term (is punctuationCodes_29_164_19 ?v_1)) (= true_term (isAllocated punctuationCodes_29_164_19 alloc)) (= ASGREM_pre_18_43_26 ASGREM_18_43_26) (= true_term (is ASGREM_18_43_26 T_int)) (= CLASSLITERAL_pre_19_60_7 CLASSLITERAL_19_60_7) (= true_term (is CLASSLITERAL_19_60_7 T_int)) (= IDENT_pre_17_25_26 IDENT_17_25_26) (= true_term (is IDENT_17_25_26 T_int)) (= CONSTRUCTORDECL_pre_19_19_7 CONSTRUCTORDECL_19_19_7) (= true_term (is CONSTRUCTORDECL_19_19_7 T_int)) (= locDot_pre_122_29_13 locDot_122_29_13) (= locDot_122_29_13 (asField locDot_122_29_13 T_int)) (= GT_pre_18_27_26 GT_18_27_26) (= true_term (is GT_18_27_26 T_int)) (= locOpenBracket_pre_138_21_13 locOpenBracket_138_21_13) (= locOpenBracket_138_21_13 (asField locOpenBracket_138_21_13 T_int)) (= elements_pre_72_61_38 elements_72_61_38) (= elements_72_61_38 (asField elements_72_61_38 (array T_javafe_ast_FieldDecl))) (< (fClosedTime elements_72_61_38) alloc) (forall ((?s_14_ Int)) (=> (not (= ?s_14_ null)) (not (= (S_select elements_72_61_38 ?s_14_) null)))) (= ARRAYINIT_pre_19_46_7 ARRAYINIT_19_46_7) (= true_term (is ARRAYINIT_19_46_7 T_int)) (= INC_pre_18_58_26 INC_18_58_26) (= true_term (is INC_18_58_26 T_int)) (= owner_pre_8_35_28 owner_8_35_28) (= owner_8_35_28 (asField owner_8_35_28 T_java_lang_Object)) (< (fClosedTime owner_8_35_28) alloc) (= locIds_pre_141_25_29 locIds_141_25_29) (= locIds_141_25_29 (asField locIds_141_25_29 ?v_1)) (< (fClosedTime locIds_141_25_29) alloc) (forall ((?s_15_ Int)) (=> (not (= ?s_15_ null)) (not (= (S_select locIds_141_25_29 ?s_15_) null)))) (= loc_pre_103_20_13 loc_103_20_13) (= loc_103_20_13 (asField loc_103_20_13 T_int)) (= LONGLIT_pre_17_40_26 LONGLIT_17_40_26) (= true_term (is LONGLIT_17_40_26 T_int)) (= EVALSTMT_pre_19_32_7 EVALSTMT_19_32_7) (= true_term (is EVALSTMT_19_32_7 T_int)) (= ASGDIV_pre_18_42_26 ASGDIV_18_42_26) (= true_term (is ASGDIV_18_42_26 T_int)) (= locOpenParen_pre_122_52_13 locOpenParen_122_52_13) (= locOpenParen_122_52_13 (asField locOpenParen_122_52_13 T_int)) (= METHODINVOCATION_pre_19_59_7 METHODINVOCATION_19_59_7) (= true_term (is METHODINVOCATION_19_59_7 T_int)) (= tokenType_pre_78_90_8 tokenType_78_90_8) (= tokenType_78_90_8 (asField tokenType_78_90_8 T_int)) (= INTERFACEDECL_pre_19_18_7 INTERFACEDECL_19_18_7) (= true_term (is INTERFACEDECL_19_18_7 T_int)) (= GE_pre_18_26_26 GE_18_26_26) (= true_term (is GE_18_26_26 T_int)) (= locCloseParen_pre_128_21_13 locCloseParen_128_21_13) (= locCloseParen_128_21_13 (asField locCloseParen_128_21_13 T_int)) (= CATCHCLAUSE_pre_19_45_7 CATCHCLAUSE_19_45_7) (= true_term (is CATCHCLAUSE_19_45_7 T_int)) (= BITNOT_pre_18_57_26 BITNOT_18_57_26) (= true_term (is BITNOT_18_57_26 T_int)) (= keywordStrings_pre_29_181_30 keywordStrings_29_181_30) (= true_term (is keywordStrings_29_181_30 ?v_0)) (= true_term (isAllocated keywordStrings_29_181_30 alloc)) (= locOpenParen_pre_131_30_13 locOpenParen_131_30_13) (= locOpenParen_131_30_13 (asField locOpenParen_131_30_13 T_int)) (= NULL_pre_13_60_26 NULL_13_60_26) (= true_term (is NULL_13_60_26 T_int)) (= SYNCHRONIZESTMT_pre_19_31_7 SYNCHRONIZESTMT_19_31_7) (= true_term (is SYNCHRONIZESTMT_19_31_7 T_int)) (= INTLIT_pre_17_39_26 INTLIT_17_39_26) (= true_term (is INTLIT_17_39_26 T_int)) (= ASGMUL_pre_18_41_26 ASGMUL_18_41_26) (= true_term (is ASGMUL_18_41_26 T_int)) (= loc_pre_115_16_13 loc_115_16_13) (= loc_115_16_13 (asField loc_115_16_13 T_int)) (= AMBIGUOUSMETHODINVOCATION_pre_19_58_7 AMBIGUOUSMETHODINVOCATION_19_58_7) (= true_term (is AMBIGUOUSMETHODINVOCATION_19_58_7 T_int)) (= CLASSDECL_pre_19_17_7 CLASSDECL_19_17_7) (= true_term (is CLASSDECL_19_17_7 T_int)) (= EQ_pre_18_25_26 EQ_18_25_26) (= true_term (is EQ_18_25_26 T_int)) (= locOpenParen_pre_119_48_13 locOpenParen_119_48_13) (= locOpenParen_119_48_13 (asField locOpenParen_119_48_13 T_int)) (= loc_pre_27_35_13 loc_27_35_13) (= loc_27_35_13 (asField loc_27_35_13 T_int)) (= TYPEMODIFIERPRAGMA_pre_29_28_26 TYPEMODIFIERPRAGMA_29_28_26) (= true_term (is TYPEMODIFIERPRAGMA_29_28_26 T_int)) (= locId_pre_62_48_13 locId_62_48_13) (= locId_62_48_13 (asField locId_62_48_13 T_int)) (= CONSTRUCTORINVOCATION_pre_19_44_7 CONSTRUCTORINVOCATION_19_44_7) (= true_term (is CONSTRUCTORINVOCATION_19_44_7 T_int)) (= count_pre_72_67_33 count_72_67_33) (= count_72_67_33 (asField count_72_67_33 T_int)) (= NOT_pre_18_56_26 NOT_18_56_26) (= true_term (is NOT_18_56_26 T_int)) (= returnType_pre_79_18_28 returnType_79_18_28) (= returnType_79_18_28 (asField returnType_79_18_28 T_javafe_ast_Type)) (< (fClosedTime returnType_79_18_28) alloc) (forall ((?s_16_ Int)) (=> (not (= ?s_16_ null)) (not (= (S_select returnType_79_18_28 ?s_16_) null)))) (= locDots_pre_141_31_29 locDots_141_31_29) (= locDots_141_31_29 (asField locDots_141_31_29 ?v_1)) (< (fClosedTime locDots_141_31_29) alloc) (forall ((?s_17_ Int)) (=> (not (= ?s_17_ null)) (not (= (S_select locDots_141_31_29 ?s_17_) null)))) (= BOOLEANLIT_pre_17_38_26 BOOLEANLIT_17_38_26) (= true_term (is BOOLEANLIT_17_38_26 T_int)) (= DOSTMT_pre_19_30_7 DOSTMT_19_30_7) (= true_term (is DOSTMT_19_30_7 T_int)) (= ASSIGN_pre_18_40_26 ASSIGN_18_40_26) (= true_term (is ASSIGN_18_40_26 T_int)) (= loc_pre_126_21_13 loc_126_21_13) (= loc_126_21_13 (asField loc_126_21_13 T_int)) (= op_pre_25_35_13 op_25_35_13) (= op_25_35_13 (asField op_25_35_13 T_int)) (= FIELDACCESS_pre_19_57_7 FIELDACCESS_19_57_7) (= true_term (is FIELDACCESS_19_57_7 T_int)) (= syntax_pre_22_28_29 syntax_22_28_29) (= syntax_22_28_29 (asField syntax_22_28_29 T_boolean)) (= ONDEMANDIMPORTDECL_pre_19_16_7 ONDEMANDIMPORTDECL_19_16_7) (= true_term (is ONDEMANDIMPORTDECL_19_16_7 T_int)) (= NE_pre_18_24_26 NE_18_24_26) (= true_term (is NE_18_24_26 T_int)) (= locColon_pre_125_25_13 locColon_125_25_13) (= locColon_125_25_13 (asField locColon_125_25_13 T_int)) (= locOpenBracket_pre_121_20_13 locOpenBracket_121_20_13) (= locOpenBracket_121_20_13 (asField locOpenBracket_121_20_13 T_int)) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= true_term (is elems_91_56 T_javafe_ast_VarInitVec)) (= true_term (isAllocated elems_91_56 alloc)) (not (= elems_91_56 null)) (= true_term (is locOpenBrace_91_67 T_int)) (= true_term (is locCloseBrace_91_85 T_int)) (not (= locOpenBrace_91_67 NULL_13_60_26)) (not (= locCloseBrace_91_85 NULL_13_60_26)) (forall ((?brokenObj Int)) (=> (and (= true_term (is ?brokenObj T_javafe_ast_ArrayInit)) (not (= ?brokenObj null))) (not (= (S_select locOpenBrace_21_13 ?brokenObj) NULL_13_60_26)))) (forall ((?brokenObj_1_ Int)) (=> (and (= true_term (is ?brokenObj_1_ T_javafe_ast_ArrayInit)) (not (= ?brokenObj_1_ null))) (not (= (S_select locCloseBrace_24_13 ?brokenObj_1_) NULL_13_60_26)))) (or (not ?v_2) (and ?v_2 ?v_5 ?v_3 ?v_6 ?v_7 ?v_8 ?v_9 ?v_10 ?v_11 (or ?v_4 (and ?v_3 ?v_12 (or ?v_4 (and ?v_3 ?v_13 ?v_4))))) (and ?v_2 ?v_5 ?v_3 ?v_6 ?v_7 ?v_8 ?v_9 ?v_10 ?v_11 ?v_3 ?v_12 ?v_3 ?v_13 ?v_3 (= locCloseBrace_96_12 (S_store locCloseBrace_24_13 RES_93_24_93_24 locCloseBrace_91_85)) ?v_2 (or (not ?v_14) (and ?v_14 (or (not ?v_15) (and ?v_15 (or (not (forall ((?brokenObj Int)) (=> (and (= true_term (is ?brokenObj T_javafe_ast_ArrayInit)) (= true_term (isAllocated ?brokenObj after_93_24_93_24)) (not (= ?brokenObj null))) (not (= (S_select locOpenBrace_95_12 ?brokenObj) NULL_13_60_26))))) (not (forall ((?brokenObj_1_ Int)) (=> (and (= true_term (is ?brokenObj_1_ T_javafe_ast_ArrayInit)) (= true_term (isAllocated ?brokenObj_1_ after_93_24_93_24)) (not (= ?brokenObj_1_ null))) (not (= (S_select locCloseBrace_96_12 ?brokenObj_1_) NULL_13_60_26)))))))))))))))))))))
(check-sat)
(exit)