(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_VarInitVec () Int)
(declare-fun T_javafe_ast_WhileStmt () Int)
(declare-fun T_javafe_ast_Stmt () Int)
(declare-fun T_javafe_ast_StmtVec () Int)
(declare-fun T_javafe_ast_ExprVec () Int)
(declare-fun T_javafe_ast_CastExpr () Int)
(declare-fun T_javafe_ast_Expr () Int)
(declare-fun T_javafe_ast_AmbiguousMethodInvocation () Int)
(declare-fun T_javafe_ast_TypeDecl () Int)
(declare-fun T_javafe_ast_ASTNode () Int)
(declare-fun T_javafe_ast_TypeDeclElem () Int)
(declare-fun T_java_lang_Throwable () Int)
(declare-fun T_java_io_Serializable () Int)
(declare-fun T_javafe_ast_LiteralExpr () Int)
(declare-fun T_javafe_ast_ImportDecl () Int)
(declare-fun T_javafe_ast_TryFinallyStmt () Int)
(declare-fun T_javafe_ast_InterfaceDecl () Int)
(declare-fun T_java_lang_RuntimeException () Int)
(declare-fun T_java_lang_Exception () Int)
(declare-fun T_javafe_ast_VariableAccess () Int)
(declare-fun T_javafe_tc_Types () Int)
(declare-fun T_javafe_ast_ThrowStmt () Int)
(declare-fun T_javafe_ast_PrimitiveType () Int)
(declare-fun T_javafe_ast_Type () Int)
(declare-fun T_javafe_tc_PrepTypeDeclaration () Int)
(declare-fun T_javafe_ast_ConstructorInvocation () Int)
(declare-fun T_javafe_ast_SwitchStmt () Int)
(declare-fun T_javafe_ast_GenericBlockStmt () Int)
(declare-fun T_javafe_ast_FormalParaDecl () Int)
(declare-fun T_javafe_ast_GenericVarDecl () Int)
(declare-fun T_javafe_tc_TagConstants () Int)
(declare-fun T_javafe_parser_TagConstants () Int)
(declare-fun T_java_util_EscjavaKeyValue () Int)
(declare-fun T_javafe_ast_CompilationUnit () Int)
(declare-fun T_javafe_ast_VarInit () Int)
(declare-fun T_java_lang_Integer () Int)
(declare-fun T_java_lang_Number () Int)
(declare-fun T_java_lang_Comparable () Int)
(declare-fun T_javafe_ast_ModifierPragmaVec () Int)
(declare-fun T_javafe_ast_TypeObjectDesignator () Int)
(declare-fun T_javafe_ast_ObjectDesignator () Int)
(declare-fun T_javafe_ast_CompoundName () Int)
(declare-fun T_javafe_ast_Name () Int)
(declare-fun T_javafe_ast_TryCatchStmt () Int)
(declare-fun T_javafe_ast_Modifiers () Int)
(declare-fun T_javafe_tc_FlowInsensitiveChecks () Int)
(declare-fun T_javafe_ast_TypeModifierPragma () Int)
(declare-fun T_javafe_ast_TypeNameVec () Int)
(declare-fun T_javafe_ast_ContinueStmt () Int)
(declare-fun T_javafe_ast_BranchStmt () Int)
(declare-fun T_javafe_ast_UnaryExpr () Int)
(declare-fun T_javafe_ast_NewInstanceExpr () Int)
(declare-fun T_javafe_ast_IfStmt () Int)
(declare-fun T_javafe_ast_TagConstants () Int)
(declare-fun T_javafe_ast_OperatorTags () Int)
(declare-fun T_javafe_ast_MethodInvocation () Int)
(declare-fun T_javafe_util_ErrorSet () Int)
(declare-fun T_javafe_ast_IdentifierVec () Int)
(declare-fun T_javafe_ast_RoutineDecl () Int)
(declare-fun T_javafe_ast_SimpleName () Int)
(declare-fun T_javafe_ast_TypeDeclElemPragma () Int)
(declare-fun T_javafe_tc_TypeSig () Int)
(declare-fun T_javafe_ast_SwitchLabel () Int)
(declare-fun T_javafe_ast_SkipStmt () Int)
(declare-fun T_javafe_tc_FieldDeclVec () Int)
(declare-fun T_javafe_tc_TypeSigVec () Int)
(declare-fun T_javafe_ast_ParenExpr () Int)
(declare-fun T_javafe_tc_Env () Int)
(declare-fun T_javafe_tc_EnvForLocalType () Int)
(declare-fun T_javafe_ast_ArrayInit () Int)
(declare-fun T_javafe_tc_LookupException () Int)
(declare-fun T_java_lang_Double () Int)
(declare-fun T_javafe_ast_GeneratedTags () Int)
(declare-fun T_javafe_ast_TypeName () Int)
(declare-fun T_javafe_ast_LocalVarDecl () Int)
(declare-fun T_javafe_util_Set () Int)
(declare-fun T_javafe_tc_MethodDeclVec () Int)
(declare-fun T_javafe_ast_ModifierPragma () Int)
(declare-fun T_javafe_ast_ReturnStmt () Int)
(declare-fun T_javafe_ast_FieldAccess () Int)
(declare-fun T_javafe_ast_BlockStmt () Int)
(declare-fun T_javafe_ast_Identifier () Int)
(declare-fun T_javafe_ast_OnDemandImportDecl () Int)
(declare-fun T_java_util_Map () Int)
(declare-fun T_javafe_util_Location () Int)
(declare-fun T_java_lang_ClassCastException () Int)
(declare-fun T_javafe_ast_InstanceOfExpr () Int)
(declare-fun T_javafe_ast_ThisExpr () Int)
(declare-fun T_javafe_ast_ClassDeclStmt () Int)
(declare-fun T_java_util_Dictionary () Int)
(declare-fun T_java_lang_Float () Int)
(declare-fun T_javafe_ast_InitBlock () Int)
(declare-fun T_javafe_tc_EnvForCU () Int)
(declare-fun T_javafe_ast_ClassDecl () Int)
(declare-fun T_javafe_ast_DoStmt () Int)
(declare-fun T_javafe_ast_BreakStmt () Int)
(declare-fun T_javafe_ast_ClassLiteral () Int)
(declare-fun T_javafe_ast_ConstructorDecl () Int)
(declare-fun T_javafe_tc_ConstantExpr () Int)
(declare-fun T_javafe_ast_BinaryExpr () Int)
(declare-fun T_javafe_ast_CatchClause () Int)
(declare-fun T_javafe_ast_ArrayRefExpr () Int)
(declare-fun T_javafe_ast_VarDeclStmt () Int)
(declare-fun T_java_util_Hashtable () Int)
(declare-fun T_javafe_ast_ArrayType () Int)
(declare-fun T_javafe_tc_EnvForLocals () Int)
(declare-fun T_javafe_ast_LabelStmt () Int)
(declare-fun T_javafe_util_Assert () Int)
(declare-fun T_javafe_ast_TypeDeclElemVec () Int)
(declare-fun T_javafe_ast_ExprObjectDesignator () Int)
(declare-fun T_javafe_ast_ASTDecoration () Int)
(declare-fun T_java_lang_Boolean () Int)
(declare-fun T_javafe_ast_CondExpr () Int)
(declare-fun T_javafe_ast_SingleTypeImportDecl () Int)
(declare-fun T_javafe_ast_FormalParaDeclVec () Int)
(declare-fun T_javafe_ast_AmbiguousVariableAccess () Int)
(declare-fun T_javafe_ast_SuperObjectDesignator () Int)
(declare-fun T_javafe_ast_MethodDecl () Int)
(declare-fun T_javafe_ast_EvalStmt () Int)
(declare-fun T_javafe_ast_SynchronizeStmt () Int)
(declare-fun T_javafe_util_StackVector () Int)
(declare-fun T_javafe_ast_ForStmt () Int)
(declare-fun T_javafe_ast_TypeModifierPragmaVec () Int)
(declare-fun T_javafe_ast_CatchClauseVec () Int)
(declare-fun T_javafe_ast_NewArrayExpr () Int)
(declare-fun T_javafe_ast_PrettyPrint () Int)
(declare-fun T_javafe_ast_FieldDecl () Int)
(declare-fun T_javafe_tc_EnvForTypeSig () Int)
(declare-fun T_java_lang_Long () Int)
(declare-fun T_javafe_ast_StmtPragma () Int)
(declare-fun DIST_ZERO_1 () Int)
(declare-fun T__TYPE () Int)
(declare-fun EQ_29_25_26 () Int)
(declare-fun ACC_FINAL_31_23_26 () Int)
(declare-fun RETURNSTMT_30_33_7 () Int)
(declare-fun NOT_29_56_26 () Int)
(declare-fun CLASSLITERAL_30_60_7 () Int)
(declare-fun ACC_STATIC_31_22_26 () Int)
(declare-fun NE_29_24_26 () Int)
(declare-fun EVALSTMT_30_32_7 () Int)
(declare-fun UNARYSUB_29_55_26 () Int)
(declare-fun METHODINVOCATION_30_59_7 () Int)
(declare-fun BITAND_29_23_26 () Int)
(declare-fun SYNCHRONIZESTMT_30_31_7 () Int)
(declare-fun UNARYADD_29_54_26 () Int)
(declare-fun AMBIGUOUSMETHODINVOCATION_30_58_7 () Int)
(declare-fun otherCodes_27_202_27 () Int)
(declare-fun BITXOR_29_22_26 () Int)
(declare-fun DOSTMT_30_30_7 () Int)
(declare-fun ASGBITXOR_29_51_26 () Int)
(declare-fun FIELDACCESS_30_57_7 () Int)
(declare-fun punctuationStrings_27_134_22 () Int)
(declare-fun CHECKED_5_776_28 () Int)
(declare-fun BITOR_29_21_26 () Int)
(declare-fun WHILESTMT_30_29_7 () Int)
(declare-fun ASGBITOR_29_50_26 () Int)
(declare-fun PREPPED_5_775_28 () Int)
(declare-fun VARIABLEACCESS_30_56_7 () Int)
(declare-fun CLASSDECLSTMT_30_28_7 () Int)
(declare-fun ASGBITAND_29_49_26 () Int)
(declare-fun AMBIGUOUSVARIABLEACCESS_30_55_7 () Int)
(declare-fun AND_29_20_26 () Int)
(declare-fun VARDECLSTMT_30_27_7 () Int)
(declare-fun ASGURSHIFT_29_48_26 () Int)
(declare-fun PARENEXPR_30_54_7 () Int)
(declare-fun NULLLIT_28_45_26 () Int)
(declare-fun PARSED_5_772_28 () Int)
(declare-fun OR_29_19_26 () Int)
(declare-fun SWITCHSTMT_30_26_7 () Int)
(declare-fun ASGRSHIFT_29_47_26 () Int)
(declare-fun CASTEXPR_30_53_7 () Int)
(declare-fun LAST_KEYWORD_27_103_26 () Int)
(declare-fun STRINGLIT_28_44_26 () Int)
(declare-fun BLOCKSTMT_30_25_7 () Int)
(declare-fun NULL_27_82_26 () Int)
(declare-fun ASGLSHIFT_29_46_26 () Int)
(declare-fun INSTANCEOFEXPR_30_52_7 () Int)
(declare-fun DOUBLELIT_28_43_26 () Int)
(declare-fun FORMALPARADECL_30_24_7 () Int)
(declare-fun map_5_301_35 () Int)
(declare-fun ASGSUB_29_45_26 () Int)
(declare-fun CONDEXPR_30_51_7 () Int)
(declare-fun otherStrings_27_193_30 () Int)
(declare-fun FLOATLIT_28_42_26 () Int)
(declare-fun FIELDDECL_30_23_7 () Int)
(declare-fun ASGADD_29_44_26 () Int)
(declare-fun NEWARRAYEXPR_30_50_7 () Int)
(declare-fun CHARLIT_28_41_26 () Int)
(declare-fun LOCALVARDECL_30_22_7 () Int)
(declare-fun whereDecoration_20_597_41 () Int)
(declare-fun ASGREM_29_43_26 () Int)
(declare-fun NEWINSTANCEEXPR_30_49_7 () Int)
(declare-fun LONGLIT_28_40_26 () Int)
(declare-fun INITBLOCK_30_21_7 () Int)
(declare-fun ASGDIV_29_42_26 () Int)
(declare-fun ARRAYREFEXPR_30_48_7 () Int)
(declare-fun INTLIT_28_39_26 () Int)
(declare-fun METHODDECL_30_20_7 () Int)
(declare-fun ASGMUL_29_41_26 () Int)
(declare-fun THISEXPR_30_47_7 () Int)
(declare-fun BOOLEANLIT_28_38_26 () Int)
(declare-fun CONSTRUCTORDECL_30_19_7 () Int)
(declare-fun ASSIGN_29_40_26 () Int)
(declare-fun TYPEMODIFIERPRAGMA_27_28_26 () Int)
(declare-fun ARRAYINIT_30_46_7 () Int)
(declare-fun SHORTTYPE_28_36_26 () Int)
(declare-fun INTERFACEDECL_30_18_7 () Int)
(declare-fun TYPESIG_26_6_28 () Int)
(declare-fun STAR_29_37_26 () Int)
(declare-fun CATCHCLAUSE_30_45_7 () Int)
(declare-fun NOTACCESSIBLE_86_13_26 () Int)
(declare-fun TYPEDECLELEMPRAGMA_27_27_26 () Int)
(declare-fun BYTETYPE_28_35_26 () Int)
(declare-fun CLASSDECL_30_17_7 () Int)
(declare-fun MOD_29_36_26 () Int)
(declare-fun BADTYPECOMBO_86_12_26 () Int)
(declare-fun CONSTRUCTORINVOCATION_30_44_7 () Int)
(declare-fun NULLTYPE_28_34_26 () Int)
(declare-fun STMTPRAGMA_27_26_26 () Int)
(declare-fun ONDEMANDIMPORTDECL_30_16_7 () Int)
(declare-fun DIV_29_35_26 () Int)
(declare-fun TRYCATCHSTMT_30_43_7 () Int)
(declare-fun VOIDTYPE_28_33_26 () Int)
(declare-fun SINGLETYPEIMPORTDECL_30_15_7 () Int)
(declare-fun SUB_29_34_26 () Int)
(declare-fun AMBIGUOUS_86_11_26 () Int)
(declare-fun MODIFIERPRAGMA_27_25_26 () Int)
(declare-fun TRYFINALLYSTMT_30_42_7 () Int)
(declare-fun DOUBLETYPE_28_32_26 () Int)
(declare-fun NOTFOUND_86_10_26 () Int)
(declare-fun COMPILATIONUNIT_30_14_7 () Int)
(declare-fun ADD_29_33_26 () Int)
(declare-fun FIRST_KEYWORD_27_51_26 () Int)
(declare-fun SWITCHLABEL_30_41_7 () Int)
(declare-fun LEXICALPRAGMA_27_24_26 () Int)
(declare-fun FLOATTYPE_28_31_26 () Int)
(declare-fun URSHIFT_29_32_26 () Int)
(declare-fun SKIPSTMT_30_40_7 () Int)
(declare-fun COMPOUNDNAME_30_67_7 () Int)
(declare-fun CHARTYPE_28_30_26 () Int)
(declare-fun RSHIFT_29_31_26 () Int)
(declare-fun FORSTMT_30_39_7 () Int)
(declare-fun SIMPLENAME_30_66_7 () Int)
(declare-fun LONGTYPE_28_29_26 () Int)
(declare-fun LSHIFT_29_30_26 () Int)
(declare-fun IFSTMT_30_38_7 () Int)
(declare-fun POSTFIXDEC_29_63_26 () Int)
(declare-fun ARRAYTYPE_30_65_7 () Int)
(declare-fun INTTYPE_28_28_26 () Int)
(declare-fun LT_29_29_26 () Int)
(declare-fun LABELSTMT_30_37_7 () Int)
(declare-fun POSTFIXINC_29_62_26 () Int)
(declare-fun noTokens_27_212_27 () Int)
(declare-fun TYPENAME_30_64_7 () Int)
(declare-fun BOOLEANTYPE_28_27_26 () Int)
(declare-fun LE_29_28_26 () Int)
(declare-fun CONTINUESTMT_30_36_7 () Int)
(declare-fun punctuationCodes_27_164_19 () Int)
(declare-fun DEC_29_59_26 () Int)
(declare-fun SUPEROBJECTDESIGNATOR_30_63_7 () Int)
(declare-fun IDENT_28_25_26 () Int)
(declare-fun GT_29_27_26 () Int)
(declare-fun BREAKSTMT_30_35_7 () Int)
(declare-fun INC_29_58_26 () Int)
(declare-fun TYPEOBJECTDESIGNATOR_30_62_7 () Int)
(declare-fun sigDecoration_5_104_38 () Int)
(declare-fun GE_29_26_26 () Int)
(declare-fun keywordStrings_27_181_30 () Int)
(declare-fun THROWSTMT_30_34_7 () Int)
(declare-fun NULL_44_60_26 () Int)
(declare-fun BITNOT_29_57_26 () Int)
(declare-fun EXPROBJECTDESIGNATOR_30_61_7 () Int)
(assert (let ((?v_0 (array T_int)) (?v_1 (array T_java_lang_String))) (and (= (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_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_StmtVec T_java_lang_Object) true_term) (= T_javafe_ast_StmtVec (asChild T_javafe_ast_StmtVec T_java_lang_Object)) (= (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_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_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_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_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_LiteralExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_LiteralExpr (asChild T_javafe_ast_LiteralExpr 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_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_InterfaceDecl T_javafe_ast_TypeDecl) true_term) (= T_javafe_ast_InterfaceDecl (asChild T_javafe_ast_InterfaceDecl T_javafe_ast_TypeDecl)) (= (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_VariableAccess T_javafe_ast_Expr) true_term) (= T_javafe_ast_VariableAccess (asChild T_javafe_ast_VariableAccess T_javafe_ast_Expr)) (= (PO_LT T_javafe_tc_Types T_java_lang_Object) true_term) (= T_javafe_tc_Types (asChild T_javafe_tc_Types T_java_lang_Object)) (= (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_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_tc_PrepTypeDeclaration T_java_lang_Object) true_term) (= T_javafe_tc_PrepTypeDeclaration (asChild T_javafe_tc_PrepTypeDeclaration T_java_lang_Object)) (= (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_SwitchStmt T_javafe_ast_GenericBlockStmt) true_term) (= T_javafe_ast_SwitchStmt (asChild T_javafe_ast_SwitchStmt T_javafe_ast_GenericBlockStmt)) (= (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_tc_TagConstants T_javafe_parser_TagConstants) true_term) (= T_javafe_tc_TagConstants (asChild T_javafe_tc_TagConstants T_javafe_parser_TagConstants)) (= (PO_LT T_java_util_EscjavaKeyValue T_java_lang_Object) true_term) (= (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_Expr T_javafe_ast_VarInit) true_term) (= T_javafe_ast_Expr (asChild T_javafe_ast_Expr T_javafe_ast_VarInit)) (= (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_ModifierPragmaVec T_java_lang_Object) true_term) (= T_javafe_ast_ModifierPragmaVec (asChild T_javafe_ast_ModifierPragmaVec T_java_lang_Object)) (= (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_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_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_Modifiers T_java_lang_Object) true_term) (= T_javafe_ast_Modifiers (asChild T_javafe_ast_Modifiers T_java_lang_Object)) (= (PO_LT T_javafe_tc_FlowInsensitiveChecks T_java_lang_Object) true_term) (= T_javafe_tc_FlowInsensitiveChecks (asChild T_javafe_tc_FlowInsensitiveChecks T_java_lang_Object)) (= (PO_LT T_javafe_ast_TypeModifierPragma T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_TypeModifierPragma (asChild T_javafe_ast_TypeModifierPragma T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_TypeNameVec T_java_lang_Object) true_term) (= T_javafe_ast_TypeNameVec (asChild T_javafe_ast_TypeNameVec T_java_lang_Object)) (= (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_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_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_NewInstanceExpr T_javafe_ast_Expr) true_term) (= T_javafe_ast_NewInstanceExpr (asChild T_javafe_ast_NewInstanceExpr T_javafe_ast_Expr)) (= (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_TypeDeclElem T_java_lang_Object) 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_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_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_util_ErrorSet T_java_lang_Object) true_term) (= T_javafe_util_ErrorSet (asChild T_javafe_util_ErrorSet T_java_lang_Object)) (= (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_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_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_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_SimpleName T_javafe_ast_Name) true_term) (= T_javafe_ast_SimpleName (asChild T_javafe_ast_SimpleName T_javafe_ast_Name)) (= (PO_LT T_javafe_ast_TypeDeclElemPragma T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_TypeDeclElemPragma (asChild T_javafe_ast_TypeDeclElemPragma T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_TypeDeclElemPragma T_javafe_ast_TypeDeclElem) true_term) (= (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_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_SkipStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_SkipStmt (asChild T_javafe_ast_SkipStmt T_javafe_ast_Stmt)) (= (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_tc_TypeSigVec T_java_lang_Object) true_term) (= T_javafe_tc_TypeSigVec (asChild T_javafe_tc_TypeSigVec T_java_lang_Object)) (= (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_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_BranchStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_BranchStmt (asChild T_javafe_ast_BranchStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_tc_EnvForLocalType T_javafe_tc_Env) true_term) (= T_javafe_tc_EnvForLocalType (asChild T_javafe_tc_EnvForLocalType T_javafe_tc_Env)) (= (PO_LT T_javafe_tc_EnvForLocalType T_java_lang_Cloneable) true_term) (= (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_javafe_tc_LookupException T_java_lang_Exception) true_term) (= T_javafe_tc_LookupException (asChild T_javafe_tc_LookupException T_java_lang_Exception)) (= (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_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_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_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_LocalVarDecl T_javafe_ast_GenericVarDecl) true_term) (= T_javafe_ast_LocalVarDecl (asChild T_javafe_ast_LocalVarDecl T_javafe_ast_GenericVarDecl)) (= (PO_LT T_javafe_util_Set T_java_lang_Object) true_term) (= T_javafe_util_Set (asChild T_javafe_util_Set T_java_lang_Object)) (= (PO_LT T_javafe_util_Set T_java_lang_Cloneable) true_term) (= (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_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_ModifierPragma T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_ModifierPragma (asChild T_javafe_ast_ModifierPragma T_javafe_ast_ASTNode)) (= (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_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_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_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_OnDemandImportDecl T_javafe_ast_ImportDecl) true_term) (= T_javafe_ast_OnDemandImportDecl (asChild T_javafe_ast_OnDemandImportDecl T_javafe_ast_ImportDecl)) (= (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_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_java_lang_Comparable T_java_lang_Object) true_term) (= (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_java_lang_ClassCastException T_java_lang_RuntimeException) true_term) (= T_java_lang_ClassCastException (asChild T_java_lang_ClassCastException T_java_lang_RuntimeException)) (= (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_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_ClassDeclStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_ClassDeclStmt (asChild T_javafe_ast_ClassDeclStmt T_javafe_ast_Stmt)) (= (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_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_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_tc_EnvForCU T_javafe_tc_Env) true_term) (= T_javafe_tc_EnvForCU (asChild T_javafe_tc_EnvForCU T_javafe_tc_Env)) (= (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_DoStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_DoStmt (asChild T_javafe_ast_DoStmt T_javafe_ast_Stmt)) (= (PO_LT T_java_io_Serializable T_java_lang_Object) true_term) (= (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_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_Cloneable T_java_lang_Object) true_term) (= (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_tc_ConstantExpr T_java_lang_Object) true_term) (= T_javafe_tc_ConstantExpr (asChild T_javafe_tc_ConstantExpr T_java_lang_Object)) (= (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_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_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_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_VarDeclStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_VarDeclStmt (asChild T_javafe_ast_VarDeclStmt T_javafe_ast_Stmt)) (= (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_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_tc_EnvForLocals T_javafe_tc_Env) true_term) (= T_javafe_tc_EnvForLocals (asChild T_javafe_tc_EnvForLocals T_javafe_tc_Env)) (= (PO_LT T_javafe_tc_EnvForLocals T_java_lang_Cloneable) true_term) (= (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_GeneratedTags T_java_lang_Object) true_term) (= (PO_LT T_javafe_util_Assert T_java_lang_Object) true_term) (= T_javafe_util_Assert (asChild T_javafe_util_Assert T_java_lang_Object)) (= (PO_LT T_javafe_ast_TypeDeclElemVec T_java_lang_Object) true_term) (= T_javafe_ast_TypeDeclElemVec (asChild T_javafe_ast_TypeDeclElemVec T_java_lang_Object)) (= (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_ExprObjectDesignator T_javafe_ast_ObjectDesignator) true_term) (= T_javafe_ast_ExprObjectDesignator (asChild T_javafe_ast_ExprObjectDesignator T_javafe_ast_ObjectDesignator)) (= (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_ASTDecoration T_java_lang_Object) true_term) (= T_javafe_ast_ASTDecoration (asChild T_javafe_ast_ASTDecoration T_java_lang_Object)) (= (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_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_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_FormalParaDeclVec T_java_lang_Object) true_term) (= T_javafe_ast_FormalParaDeclVec (asChild T_javafe_ast_FormalParaDeclVec T_java_lang_Object)) (= (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_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_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_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_SynchronizeStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_SynchronizeStmt (asChild T_javafe_ast_SynchronizeStmt T_javafe_ast_Stmt)) (= (PO_LT T_javafe_util_StackVector T_java_lang_Object) true_term) (= T_javafe_util_StackVector (asChild T_javafe_util_StackVector T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_javafe_util_StackVector) true_term) (= ?t T_javafe_util_StackVector))) (= (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_TypeModifierPragmaVec T_java_lang_Object) true_term) (= T_javafe_ast_TypeModifierPragmaVec (asChild T_javafe_ast_TypeModifierPragmaVec T_java_lang_Object)) (= (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_CatchClauseVec T_java_lang_Object) true_term) (= T_javafe_ast_CatchClauseVec (asChild T_javafe_ast_CatchClauseVec T_java_lang_Object)) (= (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_PrettyPrint T_java_lang_Object) true_term) (= T_javafe_ast_PrettyPrint (asChild T_javafe_ast_PrettyPrint T_java_lang_Object)) (= (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_tc_EnvForTypeSig T_javafe_tc_Env) true_term) (= T_javafe_tc_EnvForTypeSig (asChild T_javafe_tc_EnvForTypeSig T_javafe_tc_Env)) (= (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_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_StmtPragma T_javafe_ast_Stmt) true_term) (= T_javafe_ast_StmtPragma (asChild T_javafe_ast_StmtPragma T_javafe_ast_Stmt)) (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_VarInitVec (+ DIST_ZERO_1 10)) (= T_javafe_ast_WhileStmt (+ DIST_ZERO_1 11)) (= T_javafe_ast_StmtVec (+ DIST_ZERO_1 12)) (= T_javafe_ast_ExprVec (+ DIST_ZERO_1 13)) (= T_javafe_ast_CastExpr (+ DIST_ZERO_1 14)) (= T_javafe_ast_AmbiguousMethodInvocation (+ DIST_ZERO_1 15)) (= T_javafe_ast_TypeDecl (+ DIST_ZERO_1 16)) (= T_java_lang_Throwable (+ DIST_ZERO_1 17)) (= T_javafe_ast_LiteralExpr (+ DIST_ZERO_1 18)) (= T_javafe_ast_ImportDecl (+ DIST_ZERO_1 19)) (= T_javafe_ast_TryFinallyStmt (+ DIST_ZERO_1 20)) (= T_javafe_ast_InterfaceDecl (+ DIST_ZERO_1 21)) (= T_java_lang_RuntimeException (+ DIST_ZERO_1 22)) (= T_javafe_ast_VariableAccess (+ DIST_ZERO_1 23)) (= T_javafe_tc_Types (+ DIST_ZERO_1 24)) (= T_javafe_ast_ThrowStmt (+ DIST_ZERO_1 25)) (= T_javafe_ast_PrimitiveType (+ DIST_ZERO_1 26)) (= T_javafe_tc_PrepTypeDeclaration (+ DIST_ZERO_1 27)) (= T_javafe_ast_ConstructorInvocation (+ DIST_ZERO_1 28)) (= T_javafe_ast_SwitchStmt (+ DIST_ZERO_1 29)) (= T_javafe_ast_FormalParaDecl (+ DIST_ZERO_1 30)) (= T_javafe_tc_TagConstants (+ DIST_ZERO_1 31)) (= T_java_util_EscjavaKeyValue (+ DIST_ZERO_1 32)) (= T_javafe_ast_CompilationUnit (+ DIST_ZERO_1 33)) (= T_javafe_ast_Expr (+ DIST_ZERO_1 34)) (= T_java_lang_Integer (+ DIST_ZERO_1 35)) (= T_javafe_ast_ModifierPragmaVec (+ DIST_ZERO_1 36)) (= T_javafe_ast_TypeObjectDesignator (+ DIST_ZERO_1 37)) (= T_javafe_ast_CompoundName (+ DIST_ZERO_1 38)) (= T_javafe_ast_TryCatchStmt (+ DIST_ZERO_1 39)) (= T_javafe_ast_Modifiers (+ DIST_ZERO_1 40)) (= T_javafe_tc_FlowInsensitiveChecks (+ DIST_ZERO_1 41)) (= T_javafe_ast_TypeModifierPragma (+ DIST_ZERO_1 42)) (= T_javafe_ast_TypeNameVec (+ DIST_ZERO_1 43)) (= T_javafe_ast_GenericVarDecl (+ DIST_ZERO_1 44)) (= T_javafe_ast_ContinueStmt (+ DIST_ZERO_1 45)) (= T_javafe_ast_UnaryExpr (+ DIST_ZERO_1 46)) (= T_javafe_ast_NewInstanceExpr (+ DIST_ZERO_1 47)) (= T_javafe_ast_IfStmt (+ DIST_ZERO_1 48)) (= T_javafe_ast_TypeDeclElem (+ DIST_ZERO_1 49)) (= T_javafe_ast_TagConstants (+ DIST_ZERO_1 50)) (= T_javafe_ast_MethodInvocation (+ DIST_ZERO_1 51)) (= T_java_lang_String (+ DIST_ZERO_1 52)) (= T_javafe_util_ErrorSet (+ DIST_ZERO_1 53)) (= T_javafe_parser_TagConstants (+ DIST_ZERO_1 54)) (= T_java_lang_Exception (+ DIST_ZERO_1 55)) (= T_javafe_ast_IdentifierVec (+ DIST_ZERO_1 56)) (= T_javafe_ast_RoutineDecl (+ DIST_ZERO_1 57)) (= T_javafe_ast_SimpleName (+ DIST_ZERO_1 58)) (= T_javafe_ast_TypeDeclElemPragma (+ DIST_ZERO_1 59)) (= T_javafe_tc_TypeSig (+ DIST_ZERO_1 60)) (= T_javafe_ast_SwitchLabel (+ DIST_ZERO_1 61)) (= T_javafe_ast_SkipStmt (+ DIST_ZERO_1 62)) (= T_javafe_tc_FieldDeclVec (+ DIST_ZERO_1 63)) (= T_javafe_tc_TypeSigVec (+ DIST_ZERO_1 64)) (= T_javafe_ast_ParenExpr (+ DIST_ZERO_1 65)) (= T_javafe_tc_Env (+ DIST_ZERO_1 66)) (= T_javafe_ast_BranchStmt (+ DIST_ZERO_1 67)) (= T_javafe_tc_EnvForLocalType (+ DIST_ZERO_1 68)) (= T_javafe_ast_ArrayInit (+ DIST_ZERO_1 69)) (= T_javafe_tc_LookupException (+ DIST_ZERO_1 70)) (= T_java_lang_Double (+ DIST_ZERO_1 71)) (= T_javafe_ast_OperatorTags (+ DIST_ZERO_1 72)) (= T_javafe_ast_VarInit (+ DIST_ZERO_1 73)) (= T_javafe_ast_TypeName (+ DIST_ZERO_1 74)) (= T_javafe_ast_LocalVarDecl (+ DIST_ZERO_1 75)) (= T_javafe_util_Set (+ DIST_ZERO_1 76)) (= T_javafe_ast_ASTNode (+ DIST_ZERO_1 77)) (= T_javafe_tc_MethodDeclVec (+ DIST_ZERO_1 78)) (= T_javafe_ast_ModifierPragma (+ DIST_ZERO_1 79)) (= T_javafe_ast_ReturnStmt (+ DIST_ZERO_1 80)) (= T_javafe_ast_FieldAccess (+ DIST_ZERO_1 81)) (= T_javafe_ast_BlockStmt (+ DIST_ZERO_1 82)) (= T_javafe_ast_Identifier (+ DIST_ZERO_1 83)) (= T_javafe_ast_OnDemandImportDecl (+ DIST_ZERO_1 84)) (= T_java_util_Map (+ DIST_ZERO_1 85)) (= T_javafe_ast_ObjectDesignator (+ DIST_ZERO_1 86)) (= T_java_lang_Comparable (+ DIST_ZERO_1 87)) (= T_javafe_util_Location (+ DIST_ZERO_1 88)) (= T_java_lang_ClassCastException (+ DIST_ZERO_1 89)) (= T_javafe_ast_InstanceOfExpr (+ DIST_ZERO_1 90)) (= T_javafe_ast_ThisExpr (+ DIST_ZERO_1 91)) (= T_javafe_ast_ClassDeclStmt (+ DIST_ZERO_1 92)) (= T_java_util_Dictionary (+ DIST_ZERO_1 93)) (= T_java_lang_Float (+ DIST_ZERO_1 94)) (= T_javafe_ast_InitBlock (+ DIST_ZERO_1 95)) (= T_javafe_tc_EnvForCU (+ DIST_ZERO_1 96)) (= T_javafe_ast_ClassDecl (+ DIST_ZERO_1 97)) (= T_javafe_ast_DoStmt (+ DIST_ZERO_1 98)) (= T_java_io_Serializable (+ DIST_ZERO_1 99)) (= T_javafe_ast_BreakStmt (+ DIST_ZERO_1 100)) (= T_java_lang_Object (+ DIST_ZERO_1 101)) (= T_javafe_ast_ClassLiteral (+ DIST_ZERO_1 102)) (= T_java_lang_Cloneable (+ DIST_ZERO_1 103)) (= T_javafe_ast_ConstructorDecl (+ DIST_ZERO_1 104)) (= T_javafe_tc_ConstantExpr (+ DIST_ZERO_1 105)) (= T_javafe_ast_BinaryExpr (+ DIST_ZERO_1 106)) (= T_javafe_ast_Name (+ DIST_ZERO_1 107)) (= T_javafe_ast_CatchClause (+ DIST_ZERO_1 108)) (= T_javafe_ast_ArrayRefExpr (+ DIST_ZERO_1 109)) (= T_javafe_ast_VarDeclStmt (+ DIST_ZERO_1 110)) (= T_java_util_Hashtable (+ DIST_ZERO_1 111)) (= T_javafe_ast_ArrayType (+ DIST_ZERO_1 112)) (= T_javafe_tc_EnvForLocals (+ DIST_ZERO_1 113)) (= T_javafe_ast_LabelStmt (+ DIST_ZERO_1 114)) (= T_javafe_ast_GeneratedTags (+ DIST_ZERO_1 115)) (= T_javafe_util_Assert (+ DIST_ZERO_1 116)) (= T_javafe_ast_TypeDeclElemVec (+ DIST_ZERO_1 117)) (= T_javafe_ast_Stmt (+ DIST_ZERO_1 118)) (= T_javafe_ast_ExprObjectDesignator (+ DIST_ZERO_1 119)) (= T_javafe_ast_GenericBlockStmt (+ DIST_ZERO_1 120)) (= T_javafe_ast_ASTDecoration (+ DIST_ZERO_1 121)) (= T_java_lang_Boolean (+ DIST_ZERO_1 122)) (= T_javafe_ast_CondExpr (+ DIST_ZERO_1 123)) (= T_javafe_ast_SingleTypeImportDecl (+ DIST_ZERO_1 124)) (= T_javafe_ast_FormalParaDeclVec (+ DIST_ZERO_1 125)) (= T_javafe_ast_AmbiguousVariableAccess (+ DIST_ZERO_1 126)) (= T_javafe_ast_SuperObjectDesignator (+ DIST_ZERO_1 127)) (= T_javafe_ast_MethodDecl (+ DIST_ZERO_1 128)) (= T_javafe_ast_EvalStmt (+ DIST_ZERO_1 129)) (= T_javafe_ast_SynchronizeStmt (+ DIST_ZERO_1 130)) (= T_javafe_util_StackVector (+ DIST_ZERO_1 131)) (= T_javafe_ast_ForStmt (+ DIST_ZERO_1 132)) (= T_javafe_ast_TypeModifierPragmaVec (+ DIST_ZERO_1 133)) (= T_javafe_ast_Type (+ DIST_ZERO_1 134)) (= T_javafe_ast_CatchClauseVec (+ DIST_ZERO_1 135)) (= T_javafe_ast_NewArrayExpr (+ DIST_ZERO_1 136)) (= T_javafe_ast_PrettyPrint (+ DIST_ZERO_1 137)) (= T_javafe_ast_FieldDecl (+ DIST_ZERO_1 138)) (= T_javafe_tc_EnvForTypeSig (+ DIST_ZERO_1 139)) (= T_java_lang_Long (+ DIST_ZERO_1 140)) (= T_java_lang_Number (+ DIST_ZERO_1 141)) (= T_javafe_ast_StmtPragma (+ DIST_ZERO_1 142))) (= true_term (is EQ_29_25_26 T_int)) (= EQ_29_25_26 60) (= true_term (is ACC_FINAL_31_23_26 T_int)) (= ACC_FINAL_31_23_26 16) (= true_term (is RETURNSTMT_30_33_7 T_int)) (= RETURNSTMT_30_33_7 19) (= true_term (is NOT_29_56_26 T_int)) (= NOT_29_56_26 87) (= true_term (is CLASSLITERAL_30_60_7 T_int)) (= CLASSLITERAL_30_60_7 46) (= true_term (is ACC_STATIC_31_22_26 T_int)) (= ACC_STATIC_31_22_26 8) (= true_term (is NE_29_24_26 T_int)) (= NE_29_24_26 59) (= true_term (is EVALSTMT_30_32_7 T_int)) (= EVALSTMT_30_32_7 18) (= true_term (is UNARYSUB_29_55_26 T_int)) (= UNARYSUB_29_55_26 86) (= true_term (is METHODINVOCATION_30_59_7 T_int)) (= METHODINVOCATION_30_59_7 45) (= true_term (is BITAND_29_23_26 T_int)) (= BITAND_29_23_26 58) (= true_term (is SYNCHRONIZESTMT_30_31_7 T_int)) (= SYNCHRONIZESTMT_30_31_7 17) (= true_term (is UNARYADD_29_54_26 T_int)) (= UNARYADD_29_54_26 85) (= true_term (is AMBIGUOUSMETHODINVOCATION_30_58_7 T_int)) (= AMBIGUOUSMETHODINVOCATION_30_58_7 44) (= true_term (is otherCodes_27_202_27 ?v_0)) (not (= otherCodes_27_202_27 null)) (= (typeof otherCodes_27_202_27) ?v_0) (= (arrayLength otherCodes_27_202_27) 15) (= true_term (is BITXOR_29_22_26 T_int)) (= BITXOR_29_22_26 57) (= true_term (is DOSTMT_30_30_7 T_int)) (= DOSTMT_30_30_7 16) (= true_term (is ASGBITXOR_29_51_26 T_int)) (= ASGBITXOR_29_51_26 84) (= true_term (is FIELDACCESS_30_57_7 T_int)) (= FIELDACCESS_30_57_7 43) (= true_term (is punctuationStrings_27_134_22 ?v_1)) (not (= punctuationStrings_27_134_22 null)) (= (typeof punctuationStrings_27_134_22) ?v_1) (= (arrayLength punctuationStrings_27_134_22) 48) (= true_term (is CHECKED_5_776_28 T_int)) (= CHECKED_5_776_28 6) (= true_term (is BITOR_29_21_26 T_int)) (= BITOR_29_21_26 56) (= true_term (is WHILESTMT_30_29_7 T_int)) (= WHILESTMT_30_29_7 15) (= true_term (is ASGBITOR_29_50_26 T_int)) (= ASGBITOR_29_50_26 83) (= true_term (is PREPPED_5_775_28 T_int)) (= PREPPED_5_775_28 5) (= true_term (is VARIABLEACCESS_30_56_7 T_int)) (= VARIABLEACCESS_30_56_7 42) (= true_term (is CLASSDECLSTMT_30_28_7 T_int)) (= CLASSDECLSTMT_30_28_7 14) (= true_term (is ASGBITAND_29_49_26 T_int)) (= ASGBITAND_29_49_26 82) (= true_term (is AMBIGUOUSVARIABLEACCESS_30_55_7 T_int)) (= AMBIGUOUSVARIABLEACCESS_30_55_7 41) (= true_term (is AND_29_20_26 T_int)) (= AND_29_20_26 55) (= true_term (is VARDECLSTMT_30_27_7 T_int)) (= VARDECLSTMT_30_27_7 13) (= true_term (is ASGURSHIFT_29_48_26 T_int)) (= ASGURSHIFT_29_48_26 81) (= true_term (is PARENEXPR_30_54_7 T_int)) (= PARENEXPR_30_54_7 40) (= true_term (is NULLLIT_28_45_26 T_int)) (= NULLLIT_28_45_26 111) (= true_term (is PARSED_5_772_28 T_int)) (= PARSED_5_772_28 2) (= true_term (is OR_29_19_26 T_int)) (= OR_29_19_26 54) (= true_term (is SWITCHSTMT_30_26_7 T_int)) (= SWITCHSTMT_30_26_7 12) (= true_term (is ASGRSHIFT_29_47_26 T_int)) (= ASGRSHIFT_29_47_26 80) (= true_term (is CASTEXPR_30_53_7 T_int)) (= CASTEXPR_30_53_7 39) (= true_term (is LAST_KEYWORD_27_103_26 T_int)) (= LAST_KEYWORD_27_103_26 183) (= true_term (is STRINGLIT_28_44_26 T_int)) (= STRINGLIT_28_44_26 110) (= true_term (is BLOCKSTMT_30_25_7 T_int)) (= BLOCKSTMT_30_25_7 11) (= true_term (is NULL_27_82_26 T_int)) (= NULL_27_82_26 163) (= true_term (is ASGLSHIFT_29_46_26 T_int)) (= ASGLSHIFT_29_46_26 79) (= true_term (is INSTANCEOFEXPR_30_52_7 T_int)) (= INSTANCEOFEXPR_30_52_7 38) (= true_term (is DOUBLELIT_28_43_26 T_int)) (= DOUBLELIT_28_43_26 109) (= true_term (is FORMALPARADECL_30_24_7 T_int)) (= FORMALPARADECL_30_24_7 10) (= true_term (is map_5_301_35 T_java_util_Hashtable)) (not (= map_5_301_35 null)) (= (typeof map_5_301_35) T_java_util_Hashtable) (= true_term (is ASGSUB_29_45_26 T_int)) (= ASGSUB_29_45_26 78) (= true_term (is CONDEXPR_30_51_7 T_int)) (= CONDEXPR_30_51_7 37) (= true_term (is otherStrings_27_193_30 ?v_1)) (not (= otherStrings_27_193_30 null)) (= (typeof otherStrings_27_193_30) ?v_1) (= (arrayLength otherStrings_27_193_30) 15) (= true_term (is FLOATLIT_28_42_26 T_int)) (= FLOATLIT_28_42_26 108) (= true_term (is FIELDDECL_30_23_7 T_int)) (= FIELDDECL_30_23_7 9) (= true_term (is ASGADD_29_44_26 T_int)) (= ASGADD_29_44_26 77) (= true_term (is NEWARRAYEXPR_30_50_7 T_int)) (= NEWARRAYEXPR_30_50_7 36) (= true_term (is CHARLIT_28_41_26 T_int)) (= CHARLIT_28_41_26 107) (= true_term (is LOCALVARDECL_30_22_7 T_int)) (= LOCALVARDECL_30_22_7 8) (= true_term (is whereDecoration_20_597_41 T_javafe_ast_ASTDecoration)) (not (= whereDecoration_20_597_41 null)) (= (typeof whereDecoration_20_597_41) T_javafe_ast_ASTDecoration) (= true_term (is ASGREM_29_43_26 T_int)) (= ASGREM_29_43_26 76) (= true_term (is NEWINSTANCEEXPR_30_49_7 T_int)) (= NEWINSTANCEEXPR_30_49_7 35) (= true_term (is LONGLIT_28_40_26 T_int)) (= LONGLIT_28_40_26 106) (= true_term (is INITBLOCK_30_21_7 T_int)) (= INITBLOCK_30_21_7 7) (= true_term (is ASGDIV_29_42_26 T_int)) (= ASGDIV_29_42_26 75) (= true_term (is ARRAYREFEXPR_30_48_7 T_int)) (= ARRAYREFEXPR_30_48_7 34) (= true_term (is INTLIT_28_39_26 T_int)) (= INTLIT_28_39_26 105) (= true_term (is METHODDECL_30_20_7 T_int)) (= METHODDECL_30_20_7 6) (= true_term (is ASGMUL_29_41_26 T_int)) (= ASGMUL_29_41_26 74) (= true_term (is THISEXPR_30_47_7 T_int)) (= THISEXPR_30_47_7 33) (= true_term (is BOOLEANLIT_28_38_26 T_int)) (= BOOLEANLIT_28_38_26 104) (= true_term (is CONSTRUCTORDECL_30_19_7 T_int)) (= CONSTRUCTORDECL_30_19_7 5) (= true_term (is ASSIGN_29_40_26 T_int)) (= ASSIGN_29_40_26 73) (= true_term (is TYPEMODIFIERPRAGMA_27_28_26 T_int)) (= TYPEMODIFIERPRAGMA_27_28_26 118) (= true_term (is ARRAYINIT_30_46_7 T_int)) (= ARRAYINIT_30_46_7 32) (= true_term (is SHORTTYPE_28_36_26 T_int)) (= SHORTTYPE_28_36_26 103) (= true_term (is INTERFACEDECL_30_18_7 T_int)) (= INTERFACEDECL_30_18_7 4) (= true_term (is TYPESIG_26_6_28 T_int)) (= TYPESIG_26_6_28 184) (= true_term (is STAR_29_37_26 T_int)) (= STAR_29_37_26 72) (= true_term (is CATCHCLAUSE_30_45_7 T_int)) (= CATCHCLAUSE_30_45_7 31) (= true_term (is NOTACCESSIBLE_86_13_26 T_int)) (= NOTACCESSIBLE_86_13_26 3) (= true_term (is TYPEDECLELEMPRAGMA_27_27_26 T_int)) (= TYPEDECLELEMPRAGMA_27_27_26 117) (= true_term (is BYTETYPE_28_35_26 T_int)) (= BYTETYPE_28_35_26 102) (= true_term (is CLASSDECL_30_17_7 T_int)) (= CLASSDECL_30_17_7 3) (= true_term (is MOD_29_36_26 T_int)) (= MOD_29_36_26 71) (= true_term (is BADTYPECOMBO_86_12_26 T_int)) (= BADTYPECOMBO_86_12_26 2) (= true_term (is CONSTRUCTORINVOCATION_30_44_7 T_int)) (= CONSTRUCTORINVOCATION_30_44_7 30) (= true_term (is NULLTYPE_28_34_26 T_int)) (= NULLTYPE_28_34_26 101) (= true_term (is STMTPRAGMA_27_26_26 T_int)) (= STMTPRAGMA_27_26_26 116) (= true_term (is ONDEMANDIMPORTDECL_30_16_7 T_int)) (= ONDEMANDIMPORTDECL_30_16_7 2) (= true_term (is DIV_29_35_26 T_int)) (= DIV_29_35_26 70) (= true_term (is TRYCATCHSTMT_30_43_7 T_int)) (= TRYCATCHSTMT_30_43_7 29) (= true_term (is VOIDTYPE_28_33_26 T_int)) (= VOIDTYPE_28_33_26 100) (= true_term (is SINGLETYPEIMPORTDECL_30_15_7 T_int)) (= SINGLETYPEIMPORTDECL_30_15_7 1) (= true_term (is SUB_29_34_26 T_int)) (= SUB_29_34_26 69) (= true_term (is AMBIGUOUS_86_11_26 T_int)) (= AMBIGUOUS_86_11_26 1) (= true_term (is MODIFIERPRAGMA_27_25_26 T_int)) (= MODIFIERPRAGMA_27_25_26 115) (= true_term (is TRYFINALLYSTMT_30_42_7 T_int)) (= TRYFINALLYSTMT_30_42_7 28) (= true_term (is DOUBLETYPE_28_32_26 T_int)) (= DOUBLETYPE_28_32_26 99) (= true_term (is NOTFOUND_86_10_26 T_int)) (= NOTFOUND_86_10_26 0) (= true_term (is COMPILATIONUNIT_30_14_7 T_int)) (= COMPILATIONUNIT_30_14_7 0) (= true_term (is ADD_29_33_26 T_int)) (= ADD_29_33_26 68) (= true_term (is FIRST_KEYWORD_27_51_26 T_int)) (= FIRST_KEYWORD_27_51_26 133) (= true_term (is SWITCHLABEL_30_41_7 T_int)) (= SWITCHLABEL_30_41_7 27) (= true_term (is LEXICALPRAGMA_27_24_26 T_int)) (= LEXICALPRAGMA_27_24_26 114) (= true_term (is FLOATTYPE_28_31_26 T_int)) (= FLOATTYPE_28_31_26 98) (= true_term (is URSHIFT_29_32_26 T_int)) (= URSHIFT_29_32_26 67) (= true_term (is SKIPSTMT_30_40_7 T_int)) (= SKIPSTMT_30_40_7 26) (= true_term (is COMPOUNDNAME_30_67_7 T_int)) (= COMPOUNDNAME_30_67_7 53) (= true_term (is CHARTYPE_28_30_26 T_int)) (= CHARTYPE_28_30_26 97) (= true_term (is RSHIFT_29_31_26 T_int)) (= RSHIFT_29_31_26 66) (= true_term (is FORSTMT_30_39_7 T_int)) (= FORSTMT_30_39_7 25) (= true_term (is SIMPLENAME_30_66_7 T_int)) (= SIMPLENAME_30_66_7 52) (= true_term (is LONGTYPE_28_29_26 T_int)) (= LONGTYPE_28_29_26 96) (= true_term (is LSHIFT_29_30_26 T_int)) (= LSHIFT_29_30_26 65) (= true_term (is IFSTMT_30_38_7 T_int)) (= IFSTMT_30_38_7 24) (= true_term (is POSTFIXDEC_29_63_26 T_int)) (= POSTFIXDEC_29_63_26 92) (= true_term (is ARRAYTYPE_30_65_7 T_int)) (= ARRAYTYPE_30_65_7 51) (= true_term (is INTTYPE_28_28_26 T_int)) (= INTTYPE_28_28_26 95) (= true_term (is LT_29_29_26 T_int)) (= LT_29_29_26 64) (= true_term (is LABELSTMT_30_37_7 T_int)) (= LABELSTMT_30_37_7 23) (= true_term (is POSTFIXINC_29_62_26 T_int)) (= POSTFIXINC_29_62_26 91) (= true_term (is noTokens_27_212_27 T_int)) (= true_term (is TYPENAME_30_64_7 T_int)) (= TYPENAME_30_64_7 50) (= true_term (is BOOLEANTYPE_28_27_26 T_int)) (= BOOLEANTYPE_28_27_26 94) (= true_term (is LE_29_28_26 T_int)) (= LE_29_28_26 63) (= true_term (is CONTINUESTMT_30_36_7 T_int)) (= CONTINUESTMT_30_36_7 22) (= true_term (is punctuationCodes_27_164_19 ?v_0)) (not (= punctuationCodes_27_164_19 null)) (= (typeof punctuationCodes_27_164_19) ?v_0) (= (arrayLength punctuationCodes_27_164_19) 48) (= true_term (is DEC_29_59_26 T_int)) (= DEC_29_59_26 90) (= true_term (is SUPEROBJECTDESIGNATOR_30_63_7 T_int)) (= SUPEROBJECTDESIGNATOR_30_63_7 49) (= true_term (is IDENT_28_25_26 T_int)) (= IDENT_28_25_26 93) (= true_term (is GT_29_27_26 T_int)) (= GT_29_27_26 62) (= true_term (is BREAKSTMT_30_35_7 T_int)) (= BREAKSTMT_30_35_7 21) (= true_term (is INC_29_58_26 T_int)) (= INC_29_58_26 89) (= true_term (is TYPEOBJECTDESIGNATOR_30_62_7 T_int)) (= TYPEOBJECTDESIGNATOR_30_62_7 48) (= true_term (is sigDecoration_5_104_38 T_javafe_ast_ASTDecoration)) (not (= sigDecoration_5_104_38 null)) (= (typeof sigDecoration_5_104_38) T_javafe_ast_ASTDecoration) (= true_term (is GE_29_26_26 T_int)) (= GE_29_26_26 61) (= true_term (is keywordStrings_27_181_30 ?v_1)) (not (= keywordStrings_27_181_30 null)) (= (typeof keywordStrings_27_181_30) ?v_1) (= (arrayLength keywordStrings_27_181_30) 51) (= true_term (is THROWSTMT_30_34_7 T_int)) (= THROWSTMT_30_34_7 20) (= true_term (is NULL_44_60_26 T_int)) (= NULL_44_60_26 0) (= true_term (is BITNOT_29_57_26 T_int)) (= BITNOT_29_57_26 88) (= true_term (is EXPROBJECTDESIGNATOR_30_61_7 T_int)) (= EXPROBJECTDESIGNATOR_30_61_7 47))))
(declare-fun EQ_pre_29_25_26 () Int)
(declare-fun tmodifiers_pre_7_30_33 () Int)
(declare-fun tmodifiers_7_30_33 () Int)
(declare-fun ACC_FINAL_pre_31_23_26 () Int)
(declare-fun RETURNSTMT_pre_30_33_7 () Int)
(declare-fun expr_pre_78_15_28 () Int)
(declare-fun expr_78_15_28 () Int)
(declare-fun expr_pre_81_15_28 () Int)
(declare-fun expr_81_15_28 () Int)
(declare-fun NOT_pre_29_56_26 () Int)
(declare-fun loc_pre_164_16_13 () Int)
(declare-fun loc_164_16_13 () Int)
(declare-fun ids_pre_167_19_37 () Int)
(declare-fun ids_167_19_37 () Int)
(declare-fun locOpenBracket_pre_89_21_13 () Int)
(declare-fun locOpenBracket_89_21_13 () Int)
(declare-fun locOpenParen_pre_42_48_13 () Int)
(declare-fun locOpenParen_42_48_13 () Int)
(declare-fun name_pre_107_20_28 () Int)
(declare-fun name_107_20_28 () Int)
(declare-fun CLASSLITERAL_pre_30_60_7 () Int)
(declare-fun ACC_STATIC_pre_31_22_26 () Int)
(declare-fun elements_pre_45_61_37 () Int)
(declare-fun elements_45_61_37 () Int)
(declare-fun state_pre_5_787_15 () Int)
(declare-fun state_5_787_15 () Int)
(declare-fun id_pre_33_15_34 () Int)
(declare-fun id_33_15_34 () Int)
(declare-fun stmt_pre_73_17_28 () Int)
(declare-fun stmt_73_17_28 () Int)
(declare-fun locCloseBrace_pre_18_54_13 () Int)
(declare-fun locCloseBrace_18_54_13 () Int)
(declare-fun NE_pre_29_24_26 () Int)
(declare-fun loc_pre_74_33_13 () Int)
(declare-fun loc_74_33_13 () Int)
(declare-fun EVALSTMT_pre_30_32_7 () Int)
(declare-fun syntax_pre_7_28_29 () Int)
(declare-fun syntax_7_28_29 () Int)
(declare-fun sig_pre_48_39 () Int)
(declare-fun sig_48_39 () Int)
(declare-fun UNARYSUB_pre_29_55_26 () Int)
(declare-fun METHODINVOCATION_pre_30_59_7 () Int)
(declare-fun loc_pre_165_20_13 () Int)
(declare-fun loc_165_20_13 () Int)
(declare-fun type_pre_23_35_28 () Int)
(declare-fun type_23_35_28 () Int)
(declare-fun nullType_pre_38_131_4 () Int)
(declare-fun nullType_38_131_4 () Int)
(declare-fun BITAND_pre_29_23_26 () Int)
(declare-fun SYNCHRONIZESTMT_pre_30_31_7 () Int)
(declare-fun parent_pre_52_18_18 () Int)
(declare-fun parent_52_18_18 () Int)
(declare-fun UNARYADD_pre_29_54_26 () Int)
(declare-fun AMBIGUOUSMETHODINVOCATION_pre_30_58_7 () Int)
(declare-fun label_pre_73_15_34 () Int)
(declare-fun label_73_15_34 () Int)
(declare-fun otherCodes_pre_27_202_27 () Int)
(declare-fun BITXOR_pre_29_22_26 () Int)
(declare-fun loc_pre_80_20_13 () Int)
(declare-fun loc_80_20_13 () Int)
(declare-fun DOSTMT_pre_30_30_7 () Int)
(declare-fun loc_pre_112_22_13 () Int)
(declare-fun loc_112_22_13 () Int)
(declare-fun type_pre_99_24_28 () Int)
(declare-fun type_99_24_28 () Int)
(declare-fun ASGBITXOR_pre_29_51_26 () Int)
(declare-fun FIELDACCESS_pre_30_57_7 () Int)
(declare-fun locKeyword_pre_42_45_13 () Int)
(declare-fun locKeyword_42_45_13 () Int)
(declare-fun punctuationStrings_pre_27_134_22 () Int)
(declare-fun length_pre_98_50_25 () Int)
(declare-fun length_98_50_25 () Int)
(declare-fun loc_pre_39_35_13 () Int)
(declare-fun loc_39_35_13 () Int)
(declare-fun CHECKED_pre_5_776_28 () Int)
(declare-fun locCloseBracket_pre_94_23_13 () Int)
(declare-fun locCloseBracket_94_23_13 () Int)
(declare-fun BITOR_pre_29_21_26 () Int)
(declare-fun loc_pre_85_22_13 () Int)
(declare-fun loc_85_22_13 () Int)
(declare-fun count_pre_166_67_33 () Int)
(declare-fun count_166_67_33 () Int)
(declare-fun body_pre_74_30_28 () Int)
(declare-fun body_74_30_28 () Int)
(declare-fun WHILESTMT_pre_30_29_7 () Int)
(declare-fun count_pre_90_67_33 () Int)
(declare-fun count_90_67_33 () Int)
(declare-fun permitsNullValue_pre_64_31_27 () Int)
(declare-fun permitsNullValue_64_31_27 () Int)
(declare-fun locOpenBrace_pre_18_51_13 () Int)
(declare-fun locOpenBrace_18_51_13 () Int)
(declare-fun ASGBITOR_pre_29_50_26 () Int)
(declare-fun fieldSeq_pre_48_162_38 () Int)
(declare-fun fieldSeq_48_162_38 () Int)
(declare-fun PREPPED_pre_5_775_28 () Int)
(declare-fun VARIABLEACCESS_pre_30_56_7 () Int)
(declare-fun elemType_pre_89_18_28 () Int)
(declare-fun elemType_89_18_28 () Int)
(declare-fun locDots_pre_167_31_29 () Int)
(declare-fun locDots_167_31_29 () Int)
(declare-fun count_pre_122_67_33 () Int)
(declare-fun count_122_67_33 () Int)
(declare-fun CLASSDECLSTMT_pre_30_28_7 () Int)
(declare-fun locOpenBrackets_pre_99_65_29 () Int)
(declare-fun locOpenBrackets_99_65_29 () Int)
(declare-fun decl_pre_95_55_25 () Int)
(declare-fun decl_95_55_25 () Int)
(declare-fun charType_pre_38_127_4 () Int)
(declare-fun charType_38_127_4 () Int)
(declare-fun ASGBITAND_pre_29_49_26 () Int)
(declare-fun elements_pre_24_61_43 () Int)
(declare-fun elements_24_61_43 () Int)
(declare-fun locOpenBrace_pre_32_36_13 () Int)
(declare-fun locOpenBrace_32_36_13 () Int)
(declare-fun AMBIGUOUSVARIABLEACCESS_pre_30_55_7 () Int)
(declare-fun decl_pre_59_35_37 () Int)
(declare-fun decl_59_35_37 () Int)
(declare-fun id_pre_23_32_34 () Int)
(declare-fun id_23_32_34 () Int)
(declare-fun locDot_pre_108_21_13 () Int)
(declare-fun locDot_108_21_13 () Int)
(declare-fun locCloseParen_pre_102_24_13 () Int)
(declare-fun locCloseParen_102_24_13 () Int)
(declare-fun locOpenParen_pre_95_52_13 () Int)
(declare-fun locOpenParen_95_52_13 () Int)
(declare-fun body_pre_32_34_19 () Int)
(declare-fun body_32_34_19 () Int)
(declare-fun stmt_pre_80_17_33 () Int)
(declare-fun stmt_80_17_33 () Int)
(declare-fun forUpdate_pre_74_28_31 () Int)
(declare-fun forUpdate_74_28_31 () Int)
(declare-fun loc_pre_76_20_13 () Int)
(declare-fun loc_76_20_13 () Int)
(declare-fun AND_pre_29_20_26 () Int)
(declare-fun VARDECLSTMT_pre_30_27_7 () Int)
(declare-fun id_pre_112_19_34 () Int)
(declare-fun id_112_19_34 () Int)
(declare-fun ASGURSHIFT_pre_29_48_26 () Int)
(declare-fun elements_pre_123_61_39 () Int)
(declare-fun elements_123_61_39 () Int)
(declare-fun PARENEXPR_pre_30_54_7 () Int)
(declare-fun locDot_pre_42_41_13 () Int)
(declare-fun locDot_42_41_13 () Int)
(declare-fun raises_pre_32_32_35 () Int)
(declare-fun raises_32_32_35 () Int)
(declare-fun typeDecoration_pre_1853_31 () Int)
(declare-fun typeDecoration_1853_31 () Int)
(declare-fun elementType_pre_64_26_25 () Int)
(declare-fun elementType_64_26_25 () Int)
(declare-fun tag_pre_39_30_13 () Int)
(declare-fun tag_39_30_13 () Int)
(declare-fun NULLLIT_pre_28_45_26 () Int)
(declare-fun body_pre_85_19_33 () Int)
(declare-fun body_85_19_33 () Int)
(declare-fun PARSED_pre_5_772_28 () Int)
(declare-fun OR_pre_29_19_26 () Int)
(declare-fun SWITCHSTMT_pre_30_26_7 () Int)
(declare-fun locOpenBracket_pre_94_20_13 () Int)
(declare-fun locOpenBracket_94_20_13 () Int)
(declare-fun ASGRSHIFT_pre_29_47_26 () Int)
(declare-fun decl_pre_91_28_19 () Int)
(declare-fun decl_91_28_19 () Int)
(declare-fun locId_pre_18_48_13 () Int)
(declare-fun locId_18_48_13 () Int)
(declare-fun CASTEXPR_pre_30_53_7 () Int)
(declare-fun LAST_KEYWORD_pre_27_103_26 () Int)
(declare-fun elements_pre_43_61_33 () Int)
(declare-fun elements_43_61_33 () Int)
(declare-fun pmodifiers_pre_23_30_27 () Int)
(declare-fun pmodifiers_23_30_27 () Int)
(declare-fun expr_pre_80_15_28 () Int)
(declare-fun expr_80_15_28 () Int)
(declare-fun test_pre_74_26_28 () Int)
(declare-fun test_74_26_28 () Int)
(declare-fun STRINGLIT_pre_28_44_26 () Int)
(declare-fun locColon_pre_100_25_13 () Int)
(declare-fun locColon_100_25_13 () Int)
(declare-fun BLOCKSTMT_pre_30_25_7 () Int)
(declare-fun inst_pre_48_25_52 () Int)
(declare-fun inst_48_25_52 () Int)
(declare-fun NULL_pre_27_82_26 () Int)
(declare-fun ASGLSHIFT_pre_29_46_26 () Int)
(declare-fun modifiers_pre_23_28_13 () Int)
(declare-fun modifiers_23_28_13 () Int)
(declare-fun INSTANCEOFEXPR_pre_30_52_7 () Int)
(declare-fun args_pre_32_30_41 () Int)
(declare-fun args_32_30_41 () Int)
(declare-fun tokenType_pre_58_90_8 () Int)
(declare-fun tokenType_58_90_8 () Int)
(declare-fun longType_pre_38_123_4 () Int)
(declare-fun longType_38_123_4 () Int)
(declare-fun elements_pre_16_61_33 () Int)
(declare-fun elements_16_61_33 () Int)
(declare-fun superClass_pre_57_15_18 () Int)
(declare-fun superClass_57_15_18 () Int)
(declare-fun arg_pre_85_17_38 () Int)
(declare-fun arg_85_17_38 () Int)
(declare-fun DOUBLELIT_pre_28_43_26 () Int)
(declare-fun stmt_pre_76_17_28 () Int)
(declare-fun stmt_76_17_28 () Int)
(declare-fun loc_pre_95_49_13 () Int)
(declare-fun loc_95_49_13 () Int)
(declare-fun FORMALPARADECL_pre_30_24_7 () Int)
(declare-fun map_pre_5_301_35 () Int)
(declare-fun locOpenParen_pre_102_21_13 () Int)
(declare-fun locOpenParen_102_21_13 () Int)
(declare-fun locDot_pre_103_23_13 () Int)
(declare-fun locDot_103_23_13 () Int)
(declare-fun ASGSUB_pre_29_45_26 () Int)
(declare-fun permitsNullKey_pre_64_21_27 () Int)
(declare-fun permitsNullKey_64_21_27 () Int)
(declare-fun elements_pre_21_61_41 () Int)
(declare-fun elements_21_61_41 () Int)
(declare-fun CONDEXPR_pre_30_51_7 () Int)
(declare-fun decl_pre_111_34_20 () Int)
(declare-fun decl_111_34_20 () Int)
(declare-fun otherStrings_pre_27_193_30 () Int)
(declare-fun elements_pre_153_72_21 () Int)
(declare-fun elements_153_72_21 () Int)
(declare-fun loc_pre_66_29_13 () Int)
(declare-fun loc_66_29_13 () Int)
(declare-fun forInit_pre_74_24_31 () Int)
(declare-fun forInit_74_24_31 () Int)
(declare-fun FLOATLIT_pre_28_42_26 () Int)
(declare-fun locGuardOpenParen_pre_75_23_13 () Int)
(declare-fun locGuardOpenParen_75_23_13 () Int)
(declare-fun loc_pre_101_21_13 () Int)
(declare-fun loc_101_21_13 () Int)
(declare-fun FIELDDECL_pre_30_23_7 () Int)
(declare-fun count_pre_118_67_33 () Int)
(declare-fun count_118_67_33 () Int)
(declare-fun decorationType_pre_115_48_27 () Int)
(declare-fun decorationType_115_48_27 () Int)
(declare-fun ASGADD_pre_29_44_26 () Int)
(declare-fun index_pre_94_17_28 () Int)
(declare-fun index_94_17_28 () Int)
(declare-fun loc_pre_18_45_13 () Int)
(declare-fun loc_18_45_13 () Int)
(declare-fun enclosingEnv_pre_5_52_36 () Int)
(declare-fun enclosingEnv_5_52_36 () Int)
(declare-fun NEWARRAYEXPR_pre_30_50_7 () Int)
(declare-fun enclosingInstance_pre_42_37_14 () Int)
(declare-fun enclosingInstance_42_37_14 () Int)
(declare-fun elements_pre_84_61_40 () Int)
(declare-fun elements_84_61_40 () Int)
(declare-fun dontAddImplicitConstructorInvocations_pre_23_26 () Int)
(declare-fun dontAddImplicitConstructorInvocations_23_26 () Int)
(declare-fun locId_pre_91_24_13 () Int)
(declare-fun locId_91_24_13 () Int)
(declare-fun CHARLIT_pre_28_41_26 () Int)
(declare-fun expr_pre_76_15_28 () Int)
(declare-fun expr_76_15_28 () Int)
(declare-fun LOCALVARDECL_pre_30_22_7 () Int)
(declare-fun enclosingLabels_pre_77_22 () Int)
(declare-fun enclosingLabels_77_22 () Int)
(declare-fun whereDecoration_pre_20_597_41 () Int)
(declare-fun ASGREM_pre_29_43_26 () Int)
(declare-fun locQuestion_pre_100_22_13 () Int)
(declare-fun locQuestion_100_22_13 () Int)
(declare-fun pmodifiers_pre_32_26_27 () Int)
(declare-fun pmodifiers_32_26_27 () Int)
(declare-fun NEWINSTANCEEXPR_pre_30_49_7 () Int)
(declare-fun loc_pre_92_29_13 () Int)
(declare-fun loc_92_29_13 () Int)
(declare-fun LONGLIT_pre_28_40_26 () Int)
(declare-fun overridesDecoration_pre_48_154_45 () Int)
(declare-fun overridesDecoration_48_154_45 () Int)
(declare-fun modifiers_pre_32_24_13 () Int)
(declare-fun modifiers_32_24_13 () Int)
(declare-fun anonDecl_pre_95_45_19 () Int)
(declare-fun anonDecl_95_45_19 () Int)
(declare-fun keyType_pre_64_16_25 () Int)
(declare-fun keyType_64_16_25 () Int)
(declare-fun INITBLOCK_pre_30_21_7 () Int)
(declare-fun loc_pre_83_23_13 () Int)
(declare-fun loc_83_23_13 () Int)
(declare-fun floatType_pre_38_119_4 () Int)
(declare-fun floatType_38_119_4 () Int)
(declare-fun type_pre_102_18_28 () Int)
(declare-fun type_102_18_28 () Int)
(declare-fun array_pre_94_15_28 () Int)
(declare-fun array_94_15_28 () Int)
(declare-fun ASGDIV_pre_29_42_26 () Int)
(declare-fun ARRAYREFEXPR_pre_30_48_7 () Int)
(declare-fun expr_pre_66_26_14 () Int)
(declare-fun expr_66_26_14 () Int)
(declare-fun type_pre_109_27_28 () Int)
(declare-fun type_109_27_28 () Int)
(declare-fun locCloseBrace_pre_40_25_13 () Int)
(declare-fun locCloseBrace_40_25_13 () Int)
(declare-fun INTLIT_pre_28_39_26 () Int)
(declare-fun type_pre_101_18_28 () Int)
(declare-fun type_101_18_28 () Int)
(declare-fun METHODDECL_pre_30_20_7 () Int)
(declare-fun args_pre_111_30_31 () Int)
(declare-fun args_111_30_31 () Int)
(declare-fun ht_pre_155_33_36 () Int)
(declare-fun ht_155_33_36 () Int)
(declare-fun ASGMUL_pre_29_41_26 () Int)
(declare-fun typeEnv_pre_20_323_32 () Int)
(declare-fun typeEnv_20_323_32 () Int)
(declare-fun elems_pre_18_41_39 () Int)
(declare-fun elems_18_41_39 () Int)
(declare-fun lengthFieldDecl_pre_38_917_40 () Int)
(declare-fun lengthFieldDecl_38_917_40 () Int)
(declare-fun THISEXPR_pre_30_47_7 () Int)
(declare-fun parent_pre_32_21_18 () Int)
(declare-fun parent_32_21_18 () Int)
(declare-fun count_pre_47_67_33 () Int)
(declare-fun count_47_67_33 () Int)
(declare-fun locFinally_pre_82_25_13 () Int)
(declare-fun locFinally_82_25_13 () Int)
(declare-fun count_pre_15_67_33 () Int)
(declare-fun count_15_67_33 () Int)
(declare-fun loc_pre_60_18_13 () Int)
(declare-fun loc_60_18_13 () Int)
(declare-fun type_pre_103_20_28 () Int)
(declare-fun type_103_20_28 () Int)
(declare-fun id_pre_91_21_34 () Int)
(declare-fun id_91_21_34 () Int)
(declare-fun BOOLEANLIT_pre_28_38_26 () Int)
(declare-fun loc_pre_72_18_13 () Int)
(declare-fun loc_72_18_13 () Int)
(declare-fun CONSTRUCTORDECL_pre_30_19_7 () Int)
(declare-fun ASSIGN_pre_29_40_26 () Int)
(declare-fun TYPEMODIFIERPRAGMA_pre_27_28_26 () Int)
(declare-fun ARRAYINIT_pre_30_46_7 () Int)
(declare-fun els_pre_100_19_28 () Int)
(declare-fun els_100_19_28 () Int)
(declare-fun member_pre_5_44_39 () Int)
(declare-fun member_5_44_39 () Int)
(declare-fun args_pre_95_34_31 () Int)
(declare-fun args_95_34_31 () Int)
(declare-fun classPrefix_pre_92_25_14 () Int)
(declare-fun classPrefix_92_25_14 () Int)
(declare-fun loc_pre_75_20_13 () Int)
(declare-fun loc_75_20_13 () Int)
(declare-fun SHORTTYPE_pre_28_36_26 () Int)
(declare-fun locOpenParen_pre_111_28_13 () Int)
(declare-fun locOpenParen_111_28_13 () Int)
(declare-fun INTERFACEDECL_pre_30_18_7 () Int)
(declare-fun inst_pre_93_29_44 () Int)
(declare-fun inst_93_29_44 () Int)
(declare-fun init_pre_22_20_17 () Int)
(declare-fun init_22_20_17 () Int)
(declare-fun TYPESIG_pre_26_6_28 () Int)
(declare-fun STAR_pre_29_37_26 () Int)
(declare-fun locCloseParen_pre_106_21_13 () Int)
(declare-fun locCloseParen_106_21_13 () Int)
(declare-fun allowedExceptions_pre_74_25 () Int)
(declare-fun allowedExceptions_74_25 () Int)
(declare-fun CATCHCLAUSE_pre_30_45_7 () Int)
(declare-fun elements_pre_166_61_39 () Int)
(declare-fun elements_166_61_39 () Int)
(declare-fun elements_pre_90_61_36 () Int)
(declare-fun elements_90_61_36 () Int)
(declare-fun methods_pre_5_883_26 () Int)
(declare-fun methods_5_883_26 () Int)
(declare-fun NOTACCESSIBLE_pre_86_13_26 () Int)
(declare-fun TYPEDECLELEMPRAGMA_pre_27_27_26 () Int)
(declare-fun od_pre_91_19_40 () Int)
(declare-fun od_91_19_40 () Int)
(declare-fun doubleType_pre_38_115_4 () Int)
(declare-fun doubleType_38_115_4 () Int)
(declare-fun parent_pre_22_18_18 () Int)
(declare-fun parent_22_18_18 () Int)
(declare-fun locOpenBrace_pre_40_22_13 () Int)
(declare-fun locOpenBrace_40_22_13 () Int)
(declare-fun BYTETYPE_pre_28_35_26 () Int)
(declare-fun CLASSDECL_pre_30_17_7 () Int)
(declare-fun expr_pre_102_15_28 () Int)
(declare-fun expr_102_15_28 () Int)
(declare-fun MOD_pre_29_36_26 () Int)
(declare-fun constructorSeq_pre_48_171_38 () Int)
(declare-fun constructorSeq_48_171_38 () Int)
(declare-fun BADTYPECOMBO_pre_86_12_26 () Int)
(declare-fun thn_pre_100_17_28 () Int)
(declare-fun thn_100_17_28 () Int)
(declare-fun CONSTRUCTORINVOCATION_pre_30_44_7 () Int)
(declare-fun superInterfaces_pre_18_34_35 () Int)
(declare-fun superInterfaces_18_34_35 () Int)
(declare-fun elements_pre_122_61_38 () Int)
(declare-fun elements_122_61_38 () Int)
(declare-fun catchClauses_pre_83_20_38 () Int)
(declare-fun catchClauses_83_20_38 () Int)
(declare-fun locIds_pre_167_25_29 () Int)
(declare-fun locIds_167_25_29 () Int)
(declare-fun count_pre_45_67_33 () Int)
(declare-fun count_45_67_33 () Int)
(declare-fun type_pre_95_32_32 () Int)
(declare-fun type_95_32_32 () Int)
(declare-fun locOp_pre_104_43_13 () Int)
(declare-fun locOp_104_43_13 () Int)
(declare-fun expr_pre_60_15_28 () Int)
(declare-fun expr_60_15_28 () Int)
(declare-fun loc_pre_82_22_13 () Int)
(declare-fun loc_82_22_13 () Int)
(declare-fun loc_pre_99_49_13 () Int)
(declare-fun loc_99_49_13 () Int)
(declare-fun expr_pre_113_22_28 () Int)
(declare-fun expr_113_22_28 () Int)
(declare-fun NULLTYPE_pre_28_34_26 () Int)
(declare-fun expr_pre_101_15_28 () Int)
(declare-fun expr_101_15_28 () Int)
(declare-fun label_pre_72_15_20 () Int)
(declare-fun label_72_15_20 () Int)
(declare-fun STMTPRAGMA_pre_27_26_26 () Int)
(declare-fun ONDEMANDIMPORTDECL_pre_30_16_7 () Int)
(declare-fun locOp_pre_105_32_13 () Int)
(declare-fun locOp_105_32_13 () Int)
(declare-fun DIV_pre_29_35_26 () Int)
(declare-fun TRYCATCHSTMT_pre_30_43_7 () Int)
(declare-fun currentStackBottom_pre_153_87_33 () Int)
(declare-fun currentStackBottom_153_87_33 () Int)
(declare-fun superCall_pre_42_24_17 () Int)
(declare-fun superCall_42_24_17 () Int)
(declare-fun stmt_pre_75_17_28 () Int)
(declare-fun stmt_75_17_28 () Int)
(declare-fun simpleName_pre_5_37_38 () Int)
(declare-fun simpleName_5_37_38 () Int)
(declare-fun VOIDTYPE_pre_28_33_26 () Int)
(declare-fun SINGLETYPEIMPORTDECL_pre_30_15_7 () Int)
(declare-fun locId_pre_111_25_13 () Int)
(declare-fun locId_111_25_13 () Int)
(declare-fun locSuper_pre_114_20_13 () Int)
(declare-fun locSuper_114_20_13 () Int)
(declare-fun SUB_pre_29_34_26 () Int)
(declare-fun AMBIGUOUS_pre_86_11_26 () Int)
(declare-fun MODIFIERPRAGMA_pre_27_25_26 () Int)
(declare-fun test_pre_100_15_28 () Int)
(declare-fun test_100_15_28 () Int)
(declare-fun locCloseBrace_pre_88_24_13 () Int)
(declare-fun locCloseBrace_88_24_13 () Int)
(declare-fun TRYFINALLYSTMT_pre_30_42_7 () Int)
(declare-fun locDot_pre_95_29_13 () Int)
(declare-fun locDot_95_29_13 () Int)
(declare-fun decl_pre_50_38_43 () Int)
(declare-fun decl_50_38_43 () Int)
(declare-fun id_pre_18_32_34 () Int)
(declare-fun id_18_32_34 () Int)
(declare-fun tryClause_pre_83_18_28 () Int)
(declare-fun tryClause_83_18_28 () Int)
(declare-fun stmts_pre_40_19_31 () Int)
(declare-fun stmts_40_19_31 () Int)
(declare-fun loc_pre_79_22_13 () Int)
(declare-fun loc_79_22_13 () Int)
(declare-fun DOUBLETYPE_pre_28_32_26 () Int)
(declare-fun NOTFOUND_pre_86_10_26 () Int)
(declare-fun COMPILATIONUNIT_pre_30_14_7 () Int)
(declare-fun loc_pre_77_18_13 () Int)
(declare-fun loc_77_18_13 () Int)
(declare-fun ADD_pre_29_33_26 () Int)
(declare-fun intType_pre_38_111_4 () Int)
(declare-fun intType_38_111_4 () Int)
(declare-fun FIRST_KEYWORD_pre_27_51_26 () Int)
(declare-fun locType_pre_33_21_13 () Int)
(declare-fun locType_33_21_13 () Int)
(declare-fun SWITCHLABEL_pre_30_41_7 () Int)
(declare-fun LEXICALPRAGMA_pre_27_24_26 () Int)
(declare-fun enclosingType_pre_5_32_39 () Int)
(declare-fun enclosingType_5_32_39 () Int)
(declare-fun reason_pre_86_8_13 () Int)
(declare-fun reason_86_8_13 () Int)
(declare-fun right_pre_104_40_28 () Int)
(declare-fun right_104_40_28 () Int)
(declare-fun expr_pre_75_15_28 () Int)
(declare-fun expr_75_15_28 () Int)
(declare-fun locOpenParen_pre_106_18_13 () Int)
(declare-fun locOpenParen_106_18_13 () Int)
(declare-fun finallyClause_pre_82_19_28 () Int)
(declare-fun finallyClause_82_19_28 () Int)
(declare-fun dims_pre_99_45_31 () Int)
(declare-fun dims_99_45_31 () Int)
(declare-fun FLOATTYPE_pre_28_31_26 () Int)
(declare-fun expr_pre_105_29_28 () Int)
(declare-fun expr_105_29_28 () Int)
(declare-fun returnType_pre_68_19 () Int)
(declare-fun returnType_68_19 () Int)
(declare-fun URSHIFT_pre_29_32_26 () Int)
(declare-fun locOpenParen_pre_110_30_13 () Int)
(declare-fun locOpenParen_110_30_13 () Int)
(declare-fun SKIPSTMT_pre_30_40_7 () Int)
(declare-fun decl_pre_56_15_33 () Int)
(declare-fun decl_56_15_33 () Int)
(declare-fun pmodifiers_pre_18_30_27 () Int)
(declare-fun pmodifiers_18_30_27 () Int)
(declare-fun COMPOUNDNAME_pre_30_67_7 () Int)
(declare-fun fields_pre_5_875_27 () Int)
(declare-fun fields_5_875_27 () Int)
(declare-fun CHARTYPE_pre_28_30_26 () Int)
(declare-fun count_pre_24_67_33 () Int)
(declare-fun count_24_67_33 () Int)
(declare-fun init_pre_55_19_17 () Int)
(declare-fun init_55_19_17 () Int)
(declare-fun RSHIFT_pre_29_31_26 () Int)
(declare-fun modifiers_pre_18_28_13 () Int)
(declare-fun modifiers_18_28_13 () Int)
(declare-fun CU_pre_5_71_30 () Int)
(declare-fun CU_5_71_30 () Int)
(declare-fun FORSTMT_pre_30_39_7 () Int)
(declare-fun locOpenBrace_pre_88_21_13 () Int)
(declare-fun locOpenBrace_88_21_13 () Int)
(declare-fun tag_pre_124_32_13 () Int)
(declare-fun tag_124_32_13 () Int)
(declare-fun left_pre_104_38_28 () Int)
(declare-fun left_104_38_28 () Int)
(declare-fun elements_pre_118_61_47 () Int)
(declare-fun elements_118_61_47 () Int)
(declare-fun leftToRight_pre_65_22 () Int)
(declare-fun leftToRight_65_22 () Int)
(declare-fun specOnly_pre_18_26_17 () Int)
(declare-fun specOnly_18_26_17 () Int)
(declare-fun id_pre_111_20_34 () Int)
(declare-fun id_111_20_34 () Int)
(declare-fun SIMPLENAME_pre_30_66_7 () Int)
(declare-fun lenId_pre_38_914_30 () Int)
(declare-fun lenId_38_914_30 () Int)
(declare-fun tryClause_pre_82_17_28 () Int)
(declare-fun tryClause_82_17_28 () Int)
(declare-fun LONGTYPE_pre_28_29_26 () Int)
(declare-fun els_pre_79_19_28 () Int)
(declare-fun els_79_19_28 () Int)
(declare-fun hasParent_pre_19_149_30 () Int)
(declare-fun hasParent_19_149_30 () Int)
(declare-fun op_pre_105_26_13 () Int)
(declare-fun op_105_26_13 () Int)
(declare-fun count_pre_123_67_33 () Int)
(declare-fun count_123_67_33 () Int)
(declare-fun expr_pre_77_15_14 () Int)
(declare-fun expr_77_15_14 () Int)
(declare-fun shortType_pre_38_139_4 () Int)
(declare-fun shortType_38_139_4 () Int)
(declare-fun LSHIFT_pre_29_30_26 () Int)
(declare-fun enclosingInstance_pre_95_25_14 () Int)
(declare-fun enclosingInstance_95_25_14 () Int)
(declare-fun IFSTMT_pre_30_38_7 () Int)
(declare-fun POSTFIXDEC_pre_29_63_26 () Int)
(declare-fun loc_pre_160_18_13 () Int)
(declare-fun loc_160_18_13 () Int)
(declare-fun booleanType_pre_38_107_4 () Int)
(declare-fun booleanType_38_107_4 () Int)
(declare-fun ARRAYTYPE_pre_30_65_7 () Int)
(declare-fun expr_pre_106_15_28 () Int)
(declare-fun expr_106_15_28 () Int)
(declare-fun loc_pre_124_50_13 () Int)
(declare-fun loc_124_50_13 () Int)
(declare-fun INTTYPE_pre_28_28_26 () Int)
(declare-fun LT_pre_29_29_26 () Int)
(declare-fun block_pre_51_28_33 () Int)
(declare-fun block_51_28_33 () Int)
(declare-fun LABELSTMT_pre_30_37_7 () Int)
(declare-fun count_pre_43_67_33 () Int)
(declare-fun count_43_67_33 () Int)
(declare-fun POSTFIXINC_pre_29_62_26 () Int)
(declare-fun op_pre_104_35_13 () Int)
(declare-fun op_104_35_13 () Int)
(declare-fun locId_pre_32_43_13 () Int)
(declare-fun locId_32_43_13 () Int)
(declare-fun noTokens_pre_27_212_27 () Int)
(declare-fun od_pre_111_18_40 () Int)
(declare-fun od_111_18_40 () Int)
(declare-fun TYPENAME_pre_30_64_7 () Int)
(declare-fun thn_pre_79_17_28 () Int)
(declare-fun thn_79_17_28 () Int)
(declare-fun BOOLEANTYPE_pre_28_27_26 () Int)
(declare-fun owner_pre_4_35_28 () Int)
(declare-fun owner_4_35_28 () Int)
(declare-fun methodSeq_pre_48_167_38 () Int)
(declare-fun methodSeq_48_167_38 () Int)
(declare-fun returnType_pre_33_18_28 () Int)
(declare-fun returnType_33_18_28 () Int)
(declare-fun loc_pre_121_30_13 () Int)
(declare-fun loc_121_30_13 () Int)
(declare-fun LE_pre_29_28_26 () Int)
(declare-fun CONTINUESTMT_pre_30_36_7 () Int)
(declare-fun loc_pre_78_18_13 () Int)
(declare-fun loc_78_18_13 () Int)
(declare-fun punctuationCodes_pre_27_164_19 () Int)
(declare-fun elems_pre_88_18_34 () Int)
(declare-fun elems_88_18_34 () Int)
(declare-fun DEC_pre_29_59_26 () Int)
(declare-fun rootSEnv_pre_54_45 () Int)
(declare-fun rootSEnv_54_45 () Int)
(declare-fun count_pre_16_67_33 () Int)
(declare-fun count_16_67_33 () Int)
(declare-fun locFirstSemi_pre_74_36_13 () Int)
(declare-fun locFirstSemi_74_36_13 () Int)
(declare-fun SUPEROBJECTDESIGNATOR_pre_30_63_7 () Int)
(declare-fun IDENT_pre_28_25_26 () Int)
(declare-fun parent_pre_18_59_18 () Int)
(declare-fun parent_18_59_18 () Int)
(declare-fun elements_pre_47_61_43 () Int)
(declare-fun elements_47_61_43 () Int)
(declare-fun branchDecoration_pre_1898_31 () Int)
(declare-fun branchDecoration_1898_31 () Int)
(declare-fun decl_pre_42_54_25 () Int)
(declare-fun decl_42_54_25 () Int)
(declare-fun locId_pre_73_20_13 () Int)
(declare-fun locId_73_20_13 () Int)
(declare-fun name_pre_46_18_28 () Int)
(declare-fun name_46_18_28 () Int)
(declare-fun count_pre_21_67_33 () Int)
(declare-fun count_21_67_33 () Int)
(declare-fun GT_pre_29_27_26 () Int)
(declare-fun decl_pre_54_15_36 () Int)
(declare-fun decl_54_15_36 () Int)
(declare-fun elementType_pre_155_22_27 () Int)
(declare-fun elementType_155_22_27 () Int)
(declare-fun elements_pre_15_61_36 () Int)
(declare-fun elements_15_61_36 () Int)
(declare-fun BREAKSTMT_pre_30_35_7 () Int)
(declare-fun INC_pre_29_58_26 () Int)
(declare-fun init_pre_99_35_19 () Int)
(declare-fun init_99_35_19 () Int)
(declare-fun byteType_pre_38_135_4 () Int)
(declare-fun byteType_38_135_4 () Int)
(declare-fun args_pre_42_51_31 () Int)
(declare-fun args_42_51_31 () Int)
(declare-fun TYPEOBJECTDESIGNATOR_pre_30_62_7 () Int)
(declare-fun sigDecoration_pre_5_104_38 () Int)
(declare-fun expr_pre_79_15_28 () Int)
(declare-fun expr_79_15_28 () Int)
(declare-fun value_pre_124_45_16 () Int)
(declare-fun value_124_45_16 () Int)
(declare-fun elementCount_pre_153_79_33 () Int)
(declare-fun elementCount_153_79_33 () Int)
(declare-fun locOpenParen_pre_80_23_13 () Int)
(declare-fun locOpenParen_80_23_13 () Int)
(declare-fun modifiers_pre_51_24_13 () Int)
(declare-fun modifiers_51_24_13 () Int)
(declare-fun elementType_pre_153_43_27 () Int)
(declare-fun elementType_153_43_27 () Int)
(declare-fun locId_pre_23_38_13 () Int)
(declare-fun locId_23_38_13 () Int)
(declare-fun decl_pre_112_26_38 () Int)
(declare-fun decl_112_26_38 () Int)
(declare-fun GE_pre_29_26_26 () Int)
(declare-fun voidType_pre_38_103_4 () Int)
(declare-fun voidType_38_103_4 () Int)
(declare-fun keywordStrings_pre_27_181_30 () Int)
(declare-fun myTypeDecl_pre_5_63_40 () Int)
(declare-fun myTypeDecl_5_63_40 () Int)
(declare-fun THROWSTMT_pre_30_34_7 () Int)
(declare-fun NULL_pre_44_60_26 () Int)
(declare-fun parent_pre_51_22_18 () Int)
(declare-fun parent_51_22_18 () Int)
(declare-fun count_pre_84_67_33 () Int)
(declare-fun count_84_67_33 () Int)
(declare-fun rootIEnv_pre_51_45 () Int)
(declare-fun rootIEnv_51_45 () Int)
(declare-fun BITNOT_pre_29_57_26 () Int)
(declare-fun loc_pre_32_40_13 () Int)
(declare-fun loc_32_40_13 () Int)
(declare-fun EXPROBJECTDESIGNATOR_pre_30_61_7 () Int)
(declare-fun elems_pre () Int)
(declare-fun elems () Int)
(declare-fun LS () Int)
(declare-fun alloc_pre () Int)
(declare-fun this () Int)
(declare-fun leftExpr_1535_39 () Int)
(declare-fun rightExpr_1535_54 () Int)
(declare-fun RES_1536_24_1536_24 () Int)
(declare-fun EC_1536_24_1536_24 () Int)
(declare-fun ecReturn () Int)
(declare-fun RES_1537_18_1537_18 () Int)
(declare-fun EC_1537_18_1537_18 () Int)
(declare-fun RES_1543_11_1543_11 () Int)
(declare-fun EC_1543_11_1543_11 () Int)
(declare-fun RES_1550_11_1550_11 () Int)
(declare-fun EC_1550_11_1550_11 () Int)
(declare-fun RES_1551_14_1551_14 () Int)
(declare-fun EC_1551_14_1551_14 () Int)
(declare-fun RES () Int)
(declare-fun EC () Int)
(declare-fun tmp1_cand_1551_5 () Int)
(declare-fun RES_1557_15_1557_15 () Int)
(declare-fun EC_1557_15_1557_15 () Int)
(declare-fun RES_1558_14_1558_14 () Int)
(declare-fun EC_1558_14_1558_14 () Int)
(declare-fun RES_1_ () Int)
(declare-fun tmp2_cand_1557_52 () Int)
(declare-fun EC_1_ () Int)
(declare-fun RES_1560_15_1560_15 () Int)
(declare-fun EC_1560_15_1560_15 () Int)
(declare-fun RES_1561_14_1561_14 () Int)
(declare-fun EC_1561_14_1561_14 () Int)
(declare-fun RES_2_ () Int)
(declare-fun EC_2_ () Int)
(declare-fun tmp5_cand_1560_53 () Int)
(declare-fun RES_1570_16_1570_16 () Int)
(declare-fun EC_1570_16_1570_16 () Int)
(declare-fun RES_3_ () Int)
(declare-fun tmp10_cor_1570_53 () Int)
(declare-fun EC_3_ () Int)
(declare-fun RES_1571_10_1571_10 () Int)
(declare-fun EC_1571_10_1571_10 () Int)
(declare-fun RES_4_ () Int)
(declare-fun EC_4_ () Int)
(declare-fun tmp9_cor_1571_48 () Int)
(declare-fun RES_1572_10_1572_10 () Int)
(declare-fun EC_1572_10_1572_10 () Int)
(declare-fun RES_1574_35_1574_35 () Int)
(declare-fun EC_1574_35_1574_35 () Int)
(declare-fun t_1574_2_1574_2_67_16_71 () Int)
(declare-fun RES_1574_2_1574_2 () Int)
(declare-fun EC_1574_2_1574_2 () Int)
(declare-fun RES_5_ () Int)
(declare-fun tmp8_cand_1573_2 () Int)
(declare-fun EC_5_ () Int)
(declare-fun RES_1577_16_1577_16 () Int)
(declare-fun EC_1577_16_1577_16 () Int)
(declare-fun RES_6_ () Int)
(declare-fun EC_6_ () Int)
(declare-fun tmp17_cor_1577_54 () Int)
(declare-fun RES_1578_10_1578_10 () Int)
(declare-fun EC_1578_10_1578_10 () Int)
(declare-fun RES_7_ () Int)
(declare-fun tmp16_cor_1578_49 () Int)
(declare-fun EC_7_ () Int)
(declare-fun RES_1579_10_1579_10 () Int)
(declare-fun EC_1579_10_1579_10 () Int)
(declare-fun RES_1581_35_1581_35 () Int)
(declare-fun EC_1581_35_1581_35 () Int)
(declare-fun t_1581_2_1581_2_67_16_71 () Int)
(declare-fun RES_1599_11_1599_11 () Int)
(declare-fun EC_1599_11_1599_11 () Int)
(declare-fun RES_1600_11_1600_11 () Int)
(declare-fun EC_1600_11_1600_11 () Int)
(declare-fun RES_8_ () Int)
(declare-fun EC_8_ () Int)
(declare-fun tmp23_cand_1599_48 () Int)
(declare-fun RES_1602_11_1602_11 () Int)
(declare-fun EC_1602_11_1602_11 () Int)
(declare-fun RES_1603_11_1603_11 () Int)
(declare-fun EC_1603_11_1603_11 () Int)
(declare-fun RES_9_ () Int)
(declare-fun EC_9_ () Int)
(declare-fun tmp25_cand_1602_49 () Int)
(declare-fun RES_1615_11_1615_11 () Int)
(declare-fun EC_1615_11_1615_11 () Int)
(declare-fun RES_1616_14_1616_14 () Int)
(declare-fun EC_1616_14_1616_14 () Int)
(declare-fun RES_10_ () Int)
(declare-fun EC_10_ () Int)
(declare-fun tmp27_cand_1616_5 () Int)
(declare-fun RES_1617_9_1617_9 () Int)
(declare-fun EC_1617_9_1617_9 () Int)
(declare-fun RES_11_ () Int)
(declare-fun RES_1581_2_1581_2 () Int)
(declare-fun EC_1581_2_1581_2 () Int)
(declare-fun RES_12_ () Int)
(declare-fun EC_11_ () Int)
(declare-fun tmp15_cand_1580_2 () Int)
(declare-fun RES_1591_18_1591_18 () Int)
(declare-fun EC_1591_18_1591_18 () Int)
(declare-fun RES_1619_9_1619_9 () Int)
(declare-fun EC_1619_9_1619_9 () Int)
(declare-fun EC_12_ () Int)
(assert (let ((?v_0 (array T_int)) (?v_1 (array T_java_lang_String)) (?v_64 (= true_term (is nullType_38_131_4 T_javafe_ast_PrimitiveType))) (?v_38 (= true_term (is charType_38_127_4 T_javafe_ast_PrimitiveType))) (?v_20 (= true_term (is shortType_38_139_4 T_javafe_ast_PrimitiveType))) (?v_15 (= true_term (is byteType_38_135_4 T_javafe_ast_PrimitiveType))) (?v_2 (not (= leftExpr_1535_39 null))) (?v_4 (not (= rightExpr_1535_54 null))) (?v_12 (not (= byteType_38_135_4 null))) (?v_17 (not (= shortType_38_139_4 null))) (?v_34 (not (= charType_38_127_4 null))) (?v_62 (not (= nullType_38_131_4 null)))) (let ((?v_59 (not ?v_2)) (?v_70 (= true_term (is RES_1536_24_1536_24 T_javafe_ast_Type))) (?v_71 (= true_term (isAllocated RES_1536_24_1536_24 alloc))) (?v_3 (= EC_1536_24_1536_24 ecReturn)) (?v_6 (not (= RES_1536_24_1536_24 null)))) (let ((?v_72 (=> ?v_3 ?v_6)) (?v_39 (not ?v_4)) (?v_73 (= true_term (is RES_1537_18_1537_18 T_javafe_ast_Type))) (?v_74 (= true_term (isAllocated RES_1537_18_1537_18 alloc))) (?v_5 (= EC_1537_18_1537_18 ecReturn)) (?v_7 (not (= RES_1537_18_1537_18 null)))) (let ((?v_75 (=> ?v_5 ?v_7)) (?v_76 (= true_term (is RES_1543_11_1543_11 T_boolean))) (?v_8 (= EC_1543_11_1543_11 ecReturn)) (?v_9 (= true_term RES_1543_11_1543_11)) (?v_40 (= true_term (is RES_1536_24_1536_24 T_javafe_ast_PrimitiveType)))) (let ((?v_14 (and ?v_40 ?v_6)) (?v_60 (= true_term (is RES_1537_18_1537_18 T_javafe_ast_PrimitiveType)))) (let ((?v_19 (and ?v_60 ?v_7))) (let ((?v_77 (=> (and ?v_8 ?v_9) (= ?v_14 ?v_19))) (?v_78 (not ?v_9)) (?v_11 (= true_term true_term)) (?v_79 (= true_term (is RES_1550_11_1550_11 T_boolean))) (?v_80 (= EC_1550_11_1550_11 ecReturn)) (?v_10 (= true_term RES_1550_11_1550_11))) (let ((?v_81 (or (and ?v_10 (= true_term (is RES_1551_14_1551_14 T_boolean)) (= EC_1551_14_1551_14 ecReturn) (= RES RES_1551_14_1551_14) (= EC EC_1551_14_1551_14) (= tmp1_cand_1551_5 RES_1551_14_1551_14)) (and (not ?v_10) ?v_11 (= RES RES_1550_11_1550_11) (= EC EC_1550_11_1550_11) (= tmp1_cand_1551_5 false_term)))) (?v_61 (= true_term tmp1_cand_1551_5)) (?v_26 (not (and ?v_6 ?v_12))) (?v_82 (= true_term (is RES_1557_15_1557_15 T_boolean))) (?v_13 (= EC_1557_15_1557_15 ecReturn)) (?v_16 (= true_term RES_1557_15_1557_15)) (?v_22 (and ?v_15 ?v_12))) (let ((?v_28 (= ?v_14 ?v_22))) (let ((?v_83 (=> (and ?v_13 ?v_16) ?v_28)) (?v_51 (not (and ?v_7 ?v_17))) (?v_18 (= EC_1558_14_1558_14 ecReturn)) (?v_25 (and ?v_20 ?v_17))) (let ((?v_54 (= ?v_19 ?v_25))) (let ((?v_84 (or (and ?v_16 (= true_term (is RES_1558_14_1558_14 T_boolean)) ?v_18 (=> (and ?v_18 (= true_term RES_1558_14_1558_14)) ?v_54) (= RES_1_ RES_1558_14_1558_14) (= tmp2_cand_1557_52 RES_1558_14_1558_14) (= EC_1_ EC_1558_14_1558_14)) (and (not ?v_16) ?v_11 (= RES_1_ RES_1557_15_1557_15) (= tmp2_cand_1557_52 false_term) (= EC_1_ EC_1557_15_1557_15)))) (?v_85 (= true_term tmp2_cand_1557_52))) (let ((?v_86 (not ?v_85)) (?v_47 (not (and ?v_7 ?v_12))) (?v_87 (= true_term (is RES_1560_15_1560_15 T_boolean))) (?v_21 (= EC_1560_15_1560_15 ecReturn)) (?v_23 (= true_term RES_1560_15_1560_15)) (?v_49 (= ?v_19 ?v_22))) (let ((?v_88 (=> (and ?v_21 ?v_23) ?v_49)) (?v_30 (not (and ?v_6 ?v_17))) (?v_24 (= EC_1561_14_1561_14 ecReturn)) (?v_33 (= ?v_14 ?v_25))) (let ((?v_89 (or (and ?v_23 (= true_term (is RES_1561_14_1561_14 T_boolean)) ?v_24 (=> (and ?v_24 (= true_term RES_1561_14_1561_14)) ?v_33) (= RES_2_ RES_1561_14_1561_14) (= EC_2_ EC_1561_14_1561_14) (= tmp5_cand_1560_53 RES_1561_14_1561_14)) (and (not ?v_23) ?v_11 (= RES_2_ RES_1560_15_1560_15) (= EC_2_ EC_1560_15_1560_15) (= tmp5_cand_1560_53 false_term)))) (?v_90 (= true_term tmp5_cand_1560_53))) (let ((?v_92 (not ?v_90)) (?v_93 (= true_term (is RES_1570_16_1570_16 T_boolean))) (?v_27 (= EC_1570_16_1570_16 ecReturn)) (?v_29 (= true_term RES_1570_16_1570_16))) (let ((?v_94 (=> (and ?v_27 ?v_29) ?v_28)) (?v_31 (not ?v_29)) (?v_32 (= EC_1571_10_1571_10 ecReturn))) (let ((?v_95 (or (and ?v_29 ?v_11 (= RES_3_ RES_1570_16_1570_16) (= tmp10_cor_1570_53 true_term) (= EC_3_ EC_1570_16_1570_16)) (and ?v_31 (= true_term (is RES_1571_10_1571_10 T_boolean)) ?v_32 (=> (and ?v_32 (= true_term RES_1571_10_1571_10)) ?v_33) (= RES_3_ RES_1571_10_1571_10) (= tmp10_cor_1570_53 RES_1571_10_1571_10) (= EC_3_ EC_1571_10_1571_10)))) (?v_35 (= true_term tmp10_cor_1570_53))) (let ((?v_36 (not ?v_35)) (?v_37 (= EC_1572_10_1572_10 ecReturn)) (?v_58 (and ?v_38 ?v_34))) (let ((?v_96 (or (and ?v_35 ?v_11 (= RES_4_ RES_3_) (= EC_4_ EC_3_) (= tmp9_cor_1571_48 true_term)) (and ?v_36 (= true_term (is RES_1572_10_1572_10 T_boolean)) ?v_37 (=> (and ?v_37 (= true_term RES_1572_10_1572_10)) (= ?v_14 ?v_58)) (= RES_4_ RES_1572_10_1572_10) (= EC_4_ EC_1572_10_1572_10) (= tmp9_cor_1571_48 RES_1572_10_1572_10)))) (?v_41 (= true_term tmp9_cor_1571_48)) (?v_42 (= true_term (is RES_1574_35_1574_35 T_java_lang_Object))) (?v_43 (= true_term (isAllocated RES_1574_35_1574_35 alloc))) (?v_44 (= EC_1574_35_1574_35 ecReturn)) (?v_45 (= t_1574_2_1574_2_67_16_71 (cast RES_1536_24_1536_24 T_javafe_ast_PrimitiveType))) (?v_46 (not (= t_1574_2_1574_2_67_16_71 null)))) (let ((?v_97 (or (and ?v_41 ?v_4 ?v_42 ?v_43 ?v_44 ?v_40 ?v_45 ?v_46 (= true_term (is RES_1574_2_1574_2 T_boolean)) (= EC_1574_2_1574_2 ecReturn) (= RES_5_ RES_1574_2_1574_2) (= tmp8_cand_1573_2 RES_1574_2_1574_2) (= EC_5_ EC_1574_2_1574_2)) (and (not ?v_41) ?v_11 (= RES_5_ RES_4_) (= tmp8_cand_1573_2 false_term) (= EC_5_ EC_4_)))) (?v_98 (= true_term tmp8_cand_1573_2))) (let ((?v_99 (not ?v_98)) (?v_100 (= true_term (is RES_1577_16_1577_16 T_boolean))) (?v_48 (= EC_1577_16_1577_16 ecReturn)) (?v_50 (= true_term RES_1577_16_1577_16))) (let ((?v_101 (=> (and ?v_48 ?v_50) ?v_49)) (?v_52 (not ?v_50)) (?v_53 (= EC_1578_10_1578_10 ecReturn))) (let ((?v_102 (or (and ?v_50 ?v_11 (= RES_6_ RES_1577_16_1577_16) (= EC_6_ EC_1577_16_1577_16) (= tmp17_cor_1577_54 true_term)) (and ?v_52 (= true_term (is RES_1578_10_1578_10 T_boolean)) ?v_53 (=> (and ?v_53 (= true_term RES_1578_10_1578_10)) ?v_54) (= RES_6_ RES_1578_10_1578_10) (= EC_6_ EC_1578_10_1578_10) (= tmp17_cor_1577_54 RES_1578_10_1578_10)))) (?v_55 (= true_term tmp17_cor_1577_54))) (let ((?v_56 (not ?v_55)) (?v_57 (= EC_1579_10_1579_10 ecReturn))) (let ((?v_103 (or (and ?v_55 ?v_11 (= RES_7_ RES_6_) (= tmp16_cor_1578_49 true_term) (= EC_7_ EC_6_)) (and ?v_56 (= true_term (is RES_1579_10_1579_10 T_boolean)) ?v_57 (=> (and ?v_57 (= true_term RES_1579_10_1579_10)) (= ?v_19 ?v_58)) (= RES_7_ RES_1579_10_1579_10) (= tmp16_cor_1578_49 RES_1579_10_1579_10) (= EC_7_ EC_1579_10_1579_10)))) (?v_104 (= true_term tmp16_cor_1578_49)) (?v_105 (= true_term (is RES_1581_35_1581_35 T_java_lang_Object))) (?v_106 (= true_term (isAllocated RES_1581_35_1581_35 alloc))) (?v_107 (= EC_1581_35_1581_35 ecReturn)) (?v_108 (= t_1581_2_1581_2_67_16_71 (cast RES_1537_18_1537_18 T_javafe_ast_PrimitiveType))) (?v_109 (not (= t_1581_2_1581_2_67_16_71 null))) (?v_112 (not ?v_61)) (?v_113 (= true_term (is RES_1599_11_1599_11 T_boolean))) (?v_63 (= EC_1599_11_1599_11 ecReturn)) (?v_65 (= true_term RES_1599_11_1599_11)) (?v_67 (and ?v_64 ?v_62))) (let ((?v_114 (=> (and ?v_63 ?v_65) (= ?v_14 ?v_67))) (?v_115 (or (and ?v_65 (= true_term (is RES_1600_11_1600_11 T_boolean)) (= EC_1600_11_1600_11 ecReturn) (= RES_8_ RES_1600_11_1600_11) (= EC_8_ EC_1600_11_1600_11) (= tmp23_cand_1599_48 RES_1600_11_1600_11)) (and (not ?v_65) ?v_11 (= RES_8_ RES_1599_11_1599_11) (= EC_8_ EC_1599_11_1599_11) (= tmp23_cand_1599_48 false_term)))) (?v_116 (= true_term tmp23_cand_1599_48))) (let ((?v_117 (not ?v_116)) (?v_118 (= true_term (is RES_1602_11_1602_11 T_boolean))) (?v_66 (= EC_1602_11_1602_11 ecReturn)) (?v_68 (= true_term RES_1602_11_1602_11))) (let ((?v_119 (=> (and ?v_66 ?v_68) (= ?v_19 ?v_67))) (?v_120 (or (and ?v_68 (= true_term (is RES_1603_11_1603_11 T_boolean)) (= EC_1603_11_1603_11 ecReturn) (= RES_9_ RES_1603_11_1603_11) (= EC_9_ EC_1603_11_1603_11) (= tmp25_cand_1602_49 RES_1603_11_1603_11)) (and (not ?v_68) ?v_11 (= RES_9_ RES_1602_11_1602_11) (= EC_9_ EC_1602_11_1602_11) (= tmp25_cand_1602_49 false_term)))) (?v_121 (= true_term tmp25_cand_1602_49))) (let ((?v_122 (not ?v_121)) (?v_123 (= true_term (is RES_1615_11_1615_11 T_boolean))) (?v_124 (= EC_1615_11_1615_11 ecReturn)) (?v_69 (= true_term RES_1615_11_1615_11))) (let ((?v_125 (or (and ?v_69 (= true_term (is RES_1616_14_1616_14 T_boolean)) (= EC_1616_14_1616_14 ecReturn) (= RES_10_ RES_1616_14_1616_14) (= EC_10_ EC_1616_14_1616_14) (= tmp27_cand_1616_5 RES_1616_14_1616_14)) (and (not ?v_69) ?v_11 (= RES_10_ RES_1615_11_1615_11) (= EC_10_ EC_1615_11_1615_11) (= tmp27_cand_1616_5 false_term)))) (?v_126 (= true_term tmp27_cand_1616_5)) (?v_127 (= true_term (is RES_1617_9_1617_9 T_boolean))) (?v_128 (= EC_1617_9_1617_9 ecReturn)) (?v_129 (= true_term RES_1617_9_1617_9))) (let ((?v_130 (not ?v_129)) (?v_91 (= RES_11_ shortType_38_139_4)) (?v_110 (= true_term tmp15_cand_1580_2)) (?v_111 (= EC_1591_18_1591_18 ecReturn)) (?v_131 (= true_term (is RES_1619_9_1619_9 T_boolean))) (?v_132 (= EC_1619_9_1619_9 ecReturn)) (?v_133 (= true_term RES_1619_9_1619_9))) (not (=> true (=> (and (= EQ_pre_29_25_26 EQ_29_25_26) (= true_term (is EQ_29_25_26 T_int)) (= tmodifiers_pre_7_30_33 tmodifiers_7_30_33) (= tmodifiers_7_30_33 (asField tmodifiers_7_30_33 T_javafe_ast_TypeModifierPragmaVec)) (< (fClosedTime tmodifiers_7_30_33) alloc) (= ACC_FINAL_pre_31_23_26 ACC_FINAL_31_23_26) (= true_term (is ACC_FINAL_31_23_26 T_int)) (= RETURNSTMT_pre_30_33_7 RETURNSTMT_30_33_7) (= true_term (is RETURNSTMT_30_33_7 T_int)) (= expr_pre_78_15_28 expr_78_15_28) (= expr_78_15_28 (asField expr_78_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_78_15_28) alloc) (forall ((?s Int)) (=> (not (= ?s null)) (not (= (S_select expr_78_15_28 ?s) null)))) (= expr_pre_81_15_28 expr_81_15_28) (= expr_81_15_28 (asField expr_81_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_81_15_28) alloc) (forall ((?s_1_ Int)) (=> (not (= ?s_1_ null)) (not (= (S_select expr_81_15_28 ?s_1_) null)))) (= NOT_pre_29_56_26 NOT_29_56_26) (= true_term (is NOT_29_56_26 T_int)) (= loc_pre_164_16_13 loc_164_16_13) (= loc_164_16_13 (asField loc_164_16_13 T_int)) (= ids_pre_167_19_37 ids_167_19_37) (= ids_167_19_37 (asField ids_167_19_37 T_javafe_ast_IdentifierVec)) (< (fClosedTime ids_167_19_37) alloc) (forall ((?s_2_ Int)) (=> (not (= ?s_2_ null)) (not (= (S_select ids_167_19_37 ?s_2_) null)))) (= locOpenBracket_pre_89_21_13 locOpenBracket_89_21_13) (= locOpenBracket_89_21_13 (asField locOpenBracket_89_21_13 T_int)) (= locOpenParen_pre_42_48_13 locOpenParen_42_48_13) (= locOpenParen_42_48_13 (asField locOpenParen_42_48_13 T_int)) (= name_pre_107_20_28 name_107_20_28) (= name_107_20_28 (asField name_107_20_28 T_javafe_ast_Name)) (< (fClosedTime name_107_20_28) alloc) (forall ((?s_3_ Int)) (=> (not (= ?s_3_ null)) (not (= (S_select name_107_20_28 ?s_3_) null)))) (= CLASSLITERAL_pre_30_60_7 CLASSLITERAL_30_60_7) (= true_term (is CLASSLITERAL_30_60_7 T_int)) (= ACC_STATIC_pre_31_22_26 ACC_STATIC_31_22_26) (= true_term (is ACC_STATIC_31_22_26 T_int)) (= elements_pre_45_61_37 elements_45_61_37) (= elements_45_61_37 (asField elements_45_61_37 (array T_javafe_ast_TypeName))) (< (fClosedTime elements_45_61_37) alloc) (forall ((?s_4_ Int)) (=> (not (= ?s_4_ null)) (not (= (S_select elements_45_61_37 ?s_4_) null)))) (= state_pre_5_787_15 state_5_787_15) (= state_5_787_15 (asField state_5_787_15 T_int)) (= id_pre_33_15_34 id_33_15_34) (= id_33_15_34 (asField id_33_15_34 T_javafe_ast_Identifier)) (< (fClosedTime id_33_15_34) alloc) (forall ((?s_5_ Int)) (=> (not (= ?s_5_ null)) (not (= (S_select id_33_15_34 ?s_5_) null)))) (= stmt_pre_73_17_28 stmt_73_17_28) (= stmt_73_17_28 (asField stmt_73_17_28 T_javafe_ast_Stmt)) (< (fClosedTime stmt_73_17_28) alloc) (forall ((?s_6_ Int)) (=> (not (= ?s_6_ null)) (not (= (S_select stmt_73_17_28 ?s_6_) null)))) (= locCloseBrace_pre_18_54_13 locCloseBrace_18_54_13) (= locCloseBrace_18_54_13 (asField locCloseBrace_18_54_13 T_int)) (= NE_pre_29_24_26 NE_29_24_26) (= true_term (is NE_29_24_26 T_int)) (= loc_pre_74_33_13 loc_74_33_13) (= loc_74_33_13 (asField loc_74_33_13 T_int)) (= EVALSTMT_pre_30_32_7 EVALSTMT_30_32_7) (= true_term (is EVALSTMT_30_32_7 T_int)) (= syntax_pre_7_28_29 syntax_7_28_29) (= syntax_7_28_29 (asField syntax_7_28_29 T_boolean)) (= sig_pre_48_39 sig_48_39) (= sig_48_39 (asField sig_48_39 T_javafe_tc_TypeSig)) (< (fClosedTime sig_48_39) alloc) (= UNARYSUB_pre_29_55_26 UNARYSUB_29_55_26) (= true_term (is UNARYSUB_29_55_26 T_int)) (= METHODINVOCATION_pre_30_59_7 METHODINVOCATION_30_59_7) (= true_term (is METHODINVOCATION_30_59_7 T_int)) (= loc_pre_165_20_13 loc_165_20_13) (= loc_165_20_13 (asField loc_165_20_13 T_int)) (= type_pre_23_35_28 type_23_35_28) (= type_23_35_28 (asField type_23_35_28 T_javafe_ast_Type)) (< (fClosedTime type_23_35_28) alloc) (forall ((?s_7_ Int)) (=> (not (= ?s_7_ null)) (not (= (S_select type_23_35_28 ?s_7_) null)))) (= nullType_pre_38_131_4 nullType_38_131_4) ?v_64 (= true_term (isAllocated nullType_38_131_4 alloc)) (= BITAND_pre_29_23_26 BITAND_29_23_26) (= true_term (is BITAND_29_23_26 T_int)) (= SYNCHRONIZESTMT_pre_30_31_7 SYNCHRONIZESTMT_30_31_7) (= true_term (is SYNCHRONIZESTMT_30_31_7 T_int)) (= parent_pre_52_18_18 parent_52_18_18) (= parent_52_18_18 (asField parent_52_18_18 T_javafe_ast_TypeDecl)) (< (fClosedTime parent_52_18_18) alloc) (= UNARYADD_pre_29_54_26 UNARYADD_29_54_26) (= true_term (is UNARYADD_29_54_26 T_int)) (= AMBIGUOUSMETHODINVOCATION_pre_30_58_7 AMBIGUOUSMETHODINVOCATION_30_58_7) (= true_term (is AMBIGUOUSMETHODINVOCATION_30_58_7 T_int)) (= label_pre_73_15_34 label_73_15_34) (= label_73_15_34 (asField label_73_15_34 T_javafe_ast_Identifier)) (< (fClosedTime label_73_15_34) alloc) (forall ((?s_8_ Int)) (=> (not (= ?s_8_ null)) (not (= (S_select label_73_15_34 ?s_8_) null)))) (= otherCodes_pre_27_202_27 otherCodes_27_202_27) (= true_term (is otherCodes_27_202_27 ?v_0)) (= true_term (isAllocated otherCodes_27_202_27 alloc)) (= BITXOR_pre_29_22_26 BITXOR_29_22_26) (= true_term (is BITXOR_29_22_26 T_int)) (= loc_pre_80_20_13 loc_80_20_13) (= loc_80_20_13 (asField loc_80_20_13 T_int)) (= DOSTMT_pre_30_30_7 DOSTMT_30_30_7) (= true_term (is DOSTMT_30_30_7 T_int)) (= loc_pre_112_22_13 loc_112_22_13) (= loc_112_22_13 (asField loc_112_22_13 T_int)) (= type_pre_99_24_28 type_99_24_28) (= type_99_24_28 (asField type_99_24_28 T_javafe_ast_Type)) (< (fClosedTime type_99_24_28) alloc) (forall ((?s_9_ Int)) (=> (not (= ?s_9_ null)) (not (= (S_select type_99_24_28 ?s_9_) null)))) (= ASGBITXOR_pre_29_51_26 ASGBITXOR_29_51_26) (= true_term (is ASGBITXOR_29_51_26 T_int)) (= FIELDACCESS_pre_30_57_7 FIELDACCESS_30_57_7) (= true_term (is FIELDACCESS_30_57_7 T_int)) (= locKeyword_pre_42_45_13 locKeyword_42_45_13) (= locKeyword_42_45_13 (asField locKeyword_42_45_13 T_int)) (= punctuationStrings_pre_27_134_22 punctuationStrings_27_134_22) (= true_term (is punctuationStrings_27_134_22 ?v_1)) (= true_term (isAllocated punctuationStrings_27_134_22 alloc)) (= length_pre_98_50_25 length_98_50_25) (= length_98_50_25 (asField length_98_50_25 T_int)) (= loc_pre_39_35_13 loc_39_35_13) (= loc_39_35_13 (asField loc_39_35_13 T_int)) (= CHECKED_pre_5_776_28 CHECKED_5_776_28) (= true_term (is CHECKED_5_776_28 T_int)) (= locCloseBracket_pre_94_23_13 locCloseBracket_94_23_13) (= locCloseBracket_94_23_13 (asField locCloseBracket_94_23_13 T_int)) (= BITOR_pre_29_21_26 BITOR_29_21_26) (= true_term (is BITOR_29_21_26 T_int)) (= loc_pre_85_22_13 loc_85_22_13) (= loc_85_22_13 (asField loc_85_22_13 T_int)) (= count_pre_166_67_33 count_166_67_33) (= count_166_67_33 (asField count_166_67_33 T_int)) (= body_pre_74_30_28 body_74_30_28) (= body_74_30_28 (asField body_74_30_28 T_javafe_ast_Stmt)) (< (fClosedTime body_74_30_28) alloc) (forall ((?s_10_ Int)) (=> (not (= ?s_10_ null)) (not (= (S_select body_74_30_28 ?s_10_) null)))) (= WHILESTMT_pre_30_29_7 WHILESTMT_30_29_7) (= true_term (is WHILESTMT_30_29_7 T_int)) (= count_pre_90_67_33 count_90_67_33) (= count_90_67_33 (asField count_90_67_33 T_int)) (= permitsNullValue_pre_64_31_27 permitsNullValue_64_31_27) (= permitsNullValue_64_31_27 (asField permitsNullValue_64_31_27 T_boolean)) (= locOpenBrace_pre_18_51_13 locOpenBrace_18_51_13) (= locOpenBrace_18_51_13 (asField locOpenBrace_18_51_13 T_int)) (= ASGBITOR_pre_29_50_26 ASGBITOR_29_50_26) (= true_term (is ASGBITOR_29_50_26 T_int)) (= fieldSeq_pre_48_162_38 fieldSeq_48_162_38) (= fieldSeq_48_162_38 (asField fieldSeq_48_162_38 T_javafe_util_StackVector)) (< (fClosedTime fieldSeq_48_162_38) alloc) (forall ((?s_11_ Int)) (=> (not (= ?s_11_ null)) (not (= (S_select fieldSeq_48_162_38 ?s_11_) null)))) (= PREPPED_pre_5_775_28 PREPPED_5_775_28) (= true_term (is PREPPED_5_775_28 T_int)) (= VARIABLEACCESS_pre_30_56_7 VARIABLEACCESS_30_56_7) (= true_term (is VARIABLEACCESS_30_56_7 T_int)) (= elemType_pre_89_18_28 elemType_89_18_28) (= elemType_89_18_28 (asField elemType_89_18_28 T_javafe_ast_Type)) (< (fClosedTime elemType_89_18_28) alloc) (forall ((?s_12_ Int)) (=> (not (= ?s_12_ null)) (not (= (S_select elemType_89_18_28 ?s_12_) null)))) (= locDots_pre_167_31_29 locDots_167_31_29) (= locDots_167_31_29 (asField locDots_167_31_29 ?v_0)) (< (fClosedTime locDots_167_31_29) alloc) (forall ((?s_13_ Int)) (=> (not (= ?s_13_ null)) (not (= (S_select locDots_167_31_29 ?s_13_) null)))) (= count_pre_122_67_33 count_122_67_33) (= count_122_67_33 (asField count_122_67_33 T_int)) (= CLASSDECLSTMT_pre_30_28_7 CLASSDECLSTMT_30_28_7) (= true_term (is CLASSDECLSTMT_30_28_7 T_int)) (= locOpenBrackets_pre_99_65_29 locOpenBrackets_99_65_29) (= locOpenBrackets_99_65_29 (asField locOpenBrackets_99_65_29 ?v_0)) (< (fClosedTime locOpenBrackets_99_65_29) alloc) (forall ((?s_14_ Int)) (=> (not (= ?s_14_ null)) (not (= (S_select locOpenBrackets_99_65_29 ?s_14_) null)))) (= decl_pre_95_55_25 decl_95_55_25) (= decl_95_55_25 (asField decl_95_55_25 T_javafe_ast_ConstructorDecl)) (< (fClosedTime decl_95_55_25) alloc) (= charType_pre_38_127_4 charType_38_127_4) ?v_38 (= true_term (isAllocated charType_38_127_4 alloc)) (= ASGBITAND_pre_29_49_26 ASGBITAND_29_49_26) (= true_term (is ASGBITAND_29_49_26 T_int)) (= elements_pre_24_61_43 elements_24_61_43) (= elements_24_61_43 (asField elements_24_61_43 (array T_javafe_ast_ModifierPragma))) (< (fClosedTime elements_24_61_43) alloc) (forall ((?s_15_ Int)) (=> (not (= ?s_15_ null)) (not (= (S_select elements_24_61_43 ?s_15_) null)))) (= locOpenBrace_pre_32_36_13 locOpenBrace_32_36_13) (= locOpenBrace_32_36_13 (asField locOpenBrace_32_36_13 T_int)) (= AMBIGUOUSVARIABLEACCESS_pre_30_55_7 AMBIGUOUSVARIABLEACCESS_30_55_7) (= true_term (is AMBIGUOUSVARIABLEACCESS_30_55_7 T_int)) (= decl_pre_59_35_37 decl_59_35_37) (= decl_59_35_37 (asField decl_59_35_37 T_javafe_ast_TypeDecl)) (< (fClosedTime decl_59_35_37) alloc) (forall ((?s_16_ Int)) (=> (not (= ?s_16_ null)) (not (= (S_select decl_59_35_37 ?s_16_) null)))) (= id_pre_23_32_34 id_23_32_34) (= id_23_32_34 (asField id_23_32_34 T_javafe_ast_Identifier)) (< (fClosedTime id_23_32_34) alloc) (forall ((?s_17_ Int)) (=> (not (= ?s_17_ null)) (not (= (S_select id_23_32_34 ?s_17_) null)))) (= locDot_pre_108_21_13 locDot_108_21_13) (= locDot_108_21_13 (asField locDot_108_21_13 T_int)) (= locCloseParen_pre_102_24_13 locCloseParen_102_24_13) (= locCloseParen_102_24_13 (asField locCloseParen_102_24_13 T_int)) (= locOpenParen_pre_95_52_13 locOpenParen_95_52_13) (= locOpenParen_95_52_13 (asField locOpenParen_95_52_13 T_int)) (= body_pre_32_34_19 body_32_34_19) (= body_32_34_19 (asField body_32_34_19 T_javafe_ast_BlockStmt)) (< (fClosedTime body_32_34_19) alloc) (= stmt_pre_80_17_33 stmt_80_17_33) (= stmt_80_17_33 (asField stmt_80_17_33 T_javafe_ast_BlockStmt)) (< (fClosedTime stmt_80_17_33) alloc) (forall ((?s_18_ Int)) (=> (not (= ?s_18_ null)) (not (= (S_select stmt_80_17_33 ?s_18_) null)))) (= forUpdate_pre_74_28_31 forUpdate_74_28_31) (= forUpdate_74_28_31 (asField forUpdate_74_28_31 T_javafe_ast_ExprVec)) (< (fClosedTime forUpdate_74_28_31) alloc) (forall ((?s_19_ Int)) (=> (not (= ?s_19_ null)) (not (= (S_select forUpdate_74_28_31 ?s_19_) null)))) (= loc_pre_76_20_13 loc_76_20_13) (= loc_76_20_13 (asField loc_76_20_13 T_int)) (= AND_pre_29_20_26 AND_29_20_26) (= true_term (is AND_29_20_26 T_int)) (= VARDECLSTMT_pre_30_27_7 VARDECLSTMT_30_27_7) (= true_term (is VARDECLSTMT_30_27_7 T_int)) (= id_pre_112_19_34 id_112_19_34) (= id_112_19_34 (asField id_112_19_34 T_javafe_ast_Identifier)) (< (fClosedTime id_112_19_34) alloc) (forall ((?s_20_ Int)) (=> (not (= ?s_20_ null)) (not (= (S_select id_112_19_34 ?s_20_) null)))) (= ASGURSHIFT_pre_29_48_26 ASGURSHIFT_29_48_26) (= true_term (is ASGURSHIFT_29_48_26 T_int)) (= elements_pre_123_61_39 elements_123_61_39) (= elements_123_61_39 (asField elements_123_61_39 (array T_javafe_ast_MethodDecl))) (< (fClosedTime elements_123_61_39) alloc) (forall ((?s_21_ Int)) (=> (not (= ?s_21_ null)) (not (= (S_select elements_123_61_39 ?s_21_) null)))) (= PARENEXPR_pre_30_54_7 PARENEXPR_30_54_7) (= true_term (is PARENEXPR_30_54_7 T_int)) (= locDot_pre_42_41_13 locDot_42_41_13) (= locDot_42_41_13 (asField locDot_42_41_13 T_int)) (= raises_pre_32_32_35 raises_32_32_35) (= raises_32_32_35 (asField raises_32_32_35 T_javafe_ast_TypeNameVec)) (< (fClosedTime raises_32_32_35) alloc) (forall ((?s_22_ Int)) (=> (not (= ?s_22_ null)) (not (= (S_select raises_32_32_35 ?s_22_) null)))) (= typeDecoration_pre_1853_31 typeDecoration_1853_31) (= true_term (is typeDecoration_1853_31 T_javafe_ast_ASTDecoration)) (= true_term (isAllocated typeDecoration_1853_31 alloc)) (= elementType_pre_64_26_25 elementType_64_26_25) (= elementType_64_26_25 (asField elementType_64_26_25 T__TYPE)) (= tag_pre_39_30_13 tag_39_30_13) (= tag_39_30_13 (asField tag_39_30_13 T_int)) (= NULLLIT_pre_28_45_26 NULLLIT_28_45_26) (= true_term (is NULLLIT_28_45_26 T_int)) (= body_pre_85_19_33 body_85_19_33) (= body_85_19_33 (asField body_85_19_33 T_javafe_ast_BlockStmt)) (< (fClosedTime body_85_19_33) alloc) (forall ((?s_23_ Int)) (=> (not (= ?s_23_ null)) (not (= (S_select body_85_19_33 ?s_23_) null)))) (= PARSED_pre_5_772_28 PARSED_5_772_28) (= true_term (is PARSED_5_772_28 T_int)) (= OR_pre_29_19_26 OR_29_19_26) (= true_term (is OR_29_19_26 T_int)) (= SWITCHSTMT_pre_30_26_7 SWITCHSTMT_30_26_7) (= true_term (is SWITCHSTMT_30_26_7 T_int)) (= locOpenBracket_pre_94_20_13 locOpenBracket_94_20_13) (= locOpenBracket_94_20_13 (asField locOpenBracket_94_20_13 T_int)) (= ASGRSHIFT_pre_29_47_26 ASGRSHIFT_29_47_26) (= true_term (is ASGRSHIFT_29_47_26 T_int)) (= decl_pre_91_28_19 decl_91_28_19) (= decl_91_28_19 (asField decl_91_28_19 T_javafe_ast_FieldDecl)) (< (fClosedTime decl_91_28_19) alloc) (= locId_pre_18_48_13 locId_18_48_13) (= locId_18_48_13 (asField locId_18_48_13 T_int)) (= CASTEXPR_pre_30_53_7 CASTEXPR_30_53_7) (= true_term (is CASTEXPR_30_53_7 T_int)) (= LAST_KEYWORD_pre_27_103_26 LAST_KEYWORD_27_103_26) (= true_term (is LAST_KEYWORD_27_103_26 T_int)) (= elements_pre_43_61_33 elements_43_61_33) (= elements_43_61_33 (asField elements_43_61_33 (array T_javafe_ast_Expr))) (< (fClosedTime elements_43_61_33) alloc) (forall ((?s_24_ Int)) (=> (not (= ?s_24_ null)) (not (= (S_select elements_43_61_33 ?s_24_) null)))) (= pmodifiers_pre_23_30_27 pmodifiers_23_30_27) (= pmodifiers_23_30_27 (asField pmodifiers_23_30_27 T_javafe_ast_ModifierPragmaVec)) (< (fClosedTime pmodifiers_23_30_27) alloc) (= expr_pre_80_15_28 expr_80_15_28) (= expr_80_15_28 (asField expr_80_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_80_15_28) alloc) (forall ((?s_25_ Int)) (=> (not (= ?s_25_ null)) (not (= (S_select expr_80_15_28 ?s_25_) null)))) (= test_pre_74_26_28 test_74_26_28) (= test_74_26_28 (asField test_74_26_28 T_javafe_ast_Expr)) (< (fClosedTime test_74_26_28) alloc) (forall ((?s_26_ Int)) (=> (not (= ?s_26_ null)) (not (= (S_select test_74_26_28 ?s_26_) null)))) (= STRINGLIT_pre_28_44_26 STRINGLIT_28_44_26) (= true_term (is STRINGLIT_28_44_26 T_int)) (= locColon_pre_100_25_13 locColon_100_25_13) (= locColon_100_25_13 (asField locColon_100_25_13 T_int)) (= BLOCKSTMT_pre_30_25_7 BLOCKSTMT_30_25_7) (= true_term (is BLOCKSTMT_30_25_7 T_int)) (= inst_pre_48_25_52 inst_48_25_52) (= true_term (is inst_48_25_52 T_javafe_tc_PrepTypeDeclaration)) (= true_term (isAllocated inst_48_25_52 alloc)) (not (= inst_48_25_52 null)) (= NULL_pre_27_82_26 NULL_27_82_26) (= true_term (is NULL_27_82_26 T_int)) (= ASGLSHIFT_pre_29_46_26 ASGLSHIFT_29_46_26) (= true_term (is ASGLSHIFT_29_46_26 T_int)) (= modifiers_pre_23_28_13 modifiers_23_28_13) (= modifiers_23_28_13 (asField modifiers_23_28_13 T_int)) (= INSTANCEOFEXPR_pre_30_52_7 INSTANCEOFEXPR_30_52_7) (= true_term (is INSTANCEOFEXPR_30_52_7 T_int)) (= args_pre_32_30_41 args_32_30_41) (= args_32_30_41 (asField args_32_30_41 T_javafe_ast_FormalParaDeclVec)) (< (fClosedTime args_32_30_41) alloc) (forall ((?s_27_ Int)) (=> (not (= ?s_27_ null)) (not (= (S_select args_32_30_41 ?s_27_) null)))) (= tokenType_pre_58_90_8 tokenType_58_90_8) (= tokenType_58_90_8 (asField tokenType_58_90_8 T_int)) (= longType_pre_38_123_4 longType_38_123_4) (= true_term (is longType_38_123_4 T_javafe_ast_PrimitiveType)) (= true_term (isAllocated longType_38_123_4 alloc)) (= elements_pre_16_61_33 elements_16_61_33) (= elements_16_61_33 (asField elements_16_61_33 (array T_javafe_ast_Stmt))) (< (fClosedTime elements_16_61_33) alloc) (forall ((?s_28_ Int)) (=> (not (= ?s_28_ null)) (not (= (S_select elements_16_61_33 ?s_28_) null)))) (= superClass_pre_57_15_18 superClass_57_15_18) (= superClass_57_15_18 (asField superClass_57_15_18 T_javafe_ast_TypeName)) (< (fClosedTime superClass_57_15_18) alloc) (= arg_pre_85_17_38 arg_85_17_38) (= arg_85_17_38 (asField arg_85_17_38 T_javafe_ast_FormalParaDecl)) (< (fClosedTime arg_85_17_38) alloc) (forall ((?s_29_ Int)) (=> (not (= ?s_29_ null)) (not (= (S_select arg_85_17_38 ?s_29_) null)))) (= DOUBLELIT_pre_28_43_26 DOUBLELIT_28_43_26) (= true_term (is DOUBLELIT_28_43_26 T_int)) (= stmt_pre_76_17_28 stmt_76_17_28) (= stmt_76_17_28 (asField stmt_76_17_28 T_javafe_ast_Stmt)) (< (fClosedTime stmt_76_17_28) alloc) (forall ((?s_30_ Int)) (=> (not (= ?s_30_ null)) (not (= (S_select stmt_76_17_28 ?s_30_) null)))) (= loc_pre_95_49_13 loc_95_49_13) (= loc_95_49_13 (asField loc_95_49_13 T_int)) (= FORMALPARADECL_pre_30_24_7 FORMALPARADECL_30_24_7) (= true_term (is FORMALPARADECL_30_24_7 T_int)) (= map_pre_5_301_35 map_5_301_35) (= true_term (is map_5_301_35 T_java_util_Hashtable)) (= true_term (isAllocated map_5_301_35 alloc)) (= locOpenParen_pre_102_21_13 locOpenParen_102_21_13) (= locOpenParen_102_21_13 (asField locOpenParen_102_21_13 T_int)) (= locDot_pre_103_23_13 locDot_103_23_13) (= locDot_103_23_13 (asField locDot_103_23_13 T_int)) (= ASGSUB_pre_29_45_26 ASGSUB_29_45_26) (= true_term (is ASGSUB_29_45_26 T_int)) (= permitsNullKey_pre_64_21_27 permitsNullKey_64_21_27) (= permitsNullKey_64_21_27 (asField permitsNullKey_64_21_27 T_boolean)) (= elements_pre_21_61_41 elements_21_61_41) (= elements_21_61_41 (asField elements_21_61_41 (array T_javafe_ast_TypeDeclElem))) (< (fClosedTime elements_21_61_41) alloc) (forall ((?s_31_ Int)) (=> (not (= ?s_31_ null)) (not (= (S_select elements_21_61_41 ?s_31_) null)))) (= CONDEXPR_pre_30_51_7 CONDEXPR_30_51_7) (= true_term (is CONDEXPR_30_51_7 T_int)) (= decl_pre_111_34_20 decl_111_34_20) (= decl_111_34_20 (asField decl_111_34_20 T_javafe_ast_MethodDecl)) (< (fClosedTime decl_111_34_20) alloc) (= otherStrings_pre_27_193_30 otherStrings_27_193_30) (= true_term (is otherStrings_27_193_30 ?v_1)) (= true_term (isAllocated otherStrings_27_193_30 alloc)) (= elements_pre_153_72_21 elements_153_72_21) (= elements_153_72_21 (asField elements_153_72_21 (array T_java_lang_Object))) (< (fClosedTime elements_153_72_21) alloc) (= loc_pre_66_29_13 loc_66_29_13) (= loc_66_29_13 (asField loc_66_29_13 T_int)) (= forInit_pre_74_24_31 forInit_74_24_31) (= forInit_74_24_31 (asField forInit_74_24_31 T_javafe_ast_StmtVec)) (< (fClosedTime forInit_74_24_31) alloc) (forall ((?s_32_ Int)) (=> (not (= ?s_32_ null)) (not (= (S_select forInit_74_24_31 ?s_32_) null)))) (= FLOATLIT_pre_28_42_26 FLOATLIT_28_42_26) (= true_term (is FLOATLIT_28_42_26 T_int)) (= locGuardOpenParen_pre_75_23_13 locGuardOpenParen_75_23_13) (= locGuardOpenParen_75_23_13 (asField locGuardOpenParen_75_23_13 T_int)) (= loc_pre_101_21_13 loc_101_21_13) (= loc_101_21_13 (asField loc_101_21_13 T_int)) (= FIELDDECL_pre_30_23_7 FIELDDECL_30_23_7) (= true_term (is FIELDDECL_30_23_7 T_int)) (= count_pre_118_67_33 count_118_67_33) (= count_118_67_33 (asField count_118_67_33 T_int)) (= decorationType_pre_115_48_27 decorationType_115_48_27) (= decorationType_115_48_27 (asField decorationType_115_48_27 T__TYPE)) (= ASGADD_pre_29_44_26 ASGADD_29_44_26) (= true_term (is ASGADD_29_44_26 T_int)) (= index_pre_94_17_28 index_94_17_28) (= index_94_17_28 (asField index_94_17_28 T_javafe_ast_Expr)) (< (fClosedTime index_94_17_28) alloc) (forall ((?s_33_ Int)) (=> (not (= ?s_33_ null)) (not (= (S_select index_94_17_28 ?s_33_) null)))) (= loc_pre_18_45_13 loc_18_45_13) (= loc_18_45_13 (asField loc_18_45_13 T_int)) (= enclosingEnv_pre_5_52_36 enclosingEnv_5_52_36) (= enclosingEnv_5_52_36 (asField enclosingEnv_5_52_36 T_javafe_tc_Env)) (< (fClosedTime enclosingEnv_5_52_36) alloc) (= NEWARRAYEXPR_pre_30_50_7 NEWARRAYEXPR_30_50_7) (= true_term (is NEWARRAYEXPR_30_50_7 T_int)) (= enclosingInstance_pre_42_37_14 enclosingInstance_42_37_14) (= enclosingInstance_42_37_14 (asField enclosingInstance_42_37_14 T_javafe_ast_Expr)) (< (fClosedTime enclosingInstance_42_37_14) alloc) (= elements_pre_84_61_40 elements_84_61_40) (= elements_84_61_40 (asField elements_84_61_40 (array T_javafe_ast_CatchClause))) (< (fClosedTime elements_84_61_40) alloc) (forall ((?s_34_ Int)) (=> (not (= ?s_34_ null)) (not (= (S_select elements_84_61_40 ?s_34_) null)))) (= dontAddImplicitConstructorInvocations_pre_23_26 dontAddImplicitConstructorInvocations_23_26) (= true_term (is dontAddImplicitConstructorInvocations_23_26 T_boolean)) (= locId_pre_91_24_13 locId_91_24_13) (= locId_91_24_13 (asField locId_91_24_13 T_int)) (= CHARLIT_pre_28_41_26 CHARLIT_28_41_26) (= true_term (is CHARLIT_28_41_26 T_int)) (= expr_pre_76_15_28 expr_76_15_28) (= expr_76_15_28 (asField expr_76_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_76_15_28) alloc) (forall ((?s_35_ Int)) (=> (not (= ?s_35_ null)) (not (= (S_select expr_76_15_28 ?s_35_) null)))) (= LOCALVARDECL_pre_30_22_7 LOCALVARDECL_30_22_7) (= true_term (is LOCALVARDECL_30_22_7 T_int)) (= enclosingLabels_pre_77_22 enclosingLabels_77_22) (= enclosingLabels_77_22 (asField enclosingLabels_77_22 T_javafe_ast_StmtVec)) (< (fClosedTime enclosingLabels_77_22) alloc) (= whereDecoration_pre_20_597_41 whereDecoration_20_597_41) (= true_term (is whereDecoration_20_597_41 T_javafe_ast_ASTDecoration)) (= true_term (isAllocated whereDecoration_20_597_41 alloc)) (= ASGREM_pre_29_43_26 ASGREM_29_43_26) (= true_term (is ASGREM_29_43_26 T_int)) (= locQuestion_pre_100_22_13 locQuestion_100_22_13) (= locQuestion_100_22_13 (asField locQuestion_100_22_13 T_int)) (= pmodifiers_pre_32_26_27 pmodifiers_32_26_27) (= pmodifiers_32_26_27 (asField pmodifiers_32_26_27 T_javafe_ast_ModifierPragmaVec)) (< (fClosedTime pmodifiers_32_26_27) alloc) (= NEWINSTANCEEXPR_pre_30_49_7 NEWINSTANCEEXPR_30_49_7) (= true_term (is NEWINSTANCEEXPR_30_49_7 T_int)) (= loc_pre_92_29_13 loc_92_29_13) (= loc_92_29_13 (asField loc_92_29_13 T_int)) (= LONGLIT_pre_28_40_26 LONGLIT_28_40_26) (= true_term (is LONGLIT_28_40_26 T_int)) (= overridesDecoration_pre_48_154_45 overridesDecoration_48_154_45) (= true_term (is overridesDecoration_48_154_45 T_javafe_ast_ASTDecoration)) (= true_term (isAllocated overridesDecoration_48_154_45 alloc)) (not (= overridesDecoration_48_154_45 null)) (= modifiers_pre_32_24_13 modifiers_32_24_13) (= modifiers_32_24_13 (asField modifiers_32_24_13 T_int)) (= anonDecl_pre_95_45_19 anonDecl_95_45_19) (= anonDecl_95_45_19 (asField anonDecl_95_45_19 T_javafe_ast_ClassDecl)) (< (fClosedTime anonDecl_95_45_19) alloc) (= keyType_pre_64_16_25 keyType_64_16_25) (= keyType_64_16_25 (asField keyType_64_16_25 T__TYPE)) (= INITBLOCK_pre_30_21_7 INITBLOCK_30_21_7) (= true_term (is INITBLOCK_30_21_7 T_int)) (= loc_pre_83_23_13 loc_83_23_13) (= loc_83_23_13 (asField loc_83_23_13 T_int)) (= floatType_pre_38_119_4 floatType_38_119_4) (= true_term (is floatType_38_119_4 T_javafe_ast_PrimitiveType)) (= true_term (isAllocated floatType_38_119_4 alloc)) (= type_pre_102_18_28 type_102_18_28) (= type_102_18_28 (asField type_102_18_28 T_javafe_ast_Type)) (< (fClosedTime type_102_18_28) alloc) (forall ((?s_36_ Int)) (=> (not (= ?s_36_ null)) (not (= (S_select type_102_18_28 ?s_36_) null)))) (= array_pre_94_15_28 array_94_15_28) (= array_94_15_28 (asField array_94_15_28 T_javafe_ast_Expr)) (< (fClosedTime array_94_15_28) alloc) (forall ((?s_37_ Int)) (=> (not (= ?s_37_ null)) (not (= (S_select array_94_15_28 ?s_37_) null)))) (= ASGDIV_pre_29_42_26 ASGDIV_29_42_26) (= true_term (is ASGDIV_29_42_26 T_int)) (= ARRAYREFEXPR_pre_30_48_7 ARRAYREFEXPR_30_48_7) (= true_term (is ARRAYREFEXPR_30_48_7 T_int)) (= expr_pre_66_26_14 expr_66_26_14) (= expr_66_26_14 (asField expr_66_26_14 T_javafe_ast_Expr)) (< (fClosedTime expr_66_26_14) alloc) (= type_pre_109_27_28 type_109_27_28) (= type_109_27_28 (asField type_109_27_28 T_javafe_ast_Type)) (< (fClosedTime type_109_27_28) alloc) (forall ((?s_38_ Int)) (=> (not (= ?s_38_ null)) (not (= (S_select type_109_27_28 ?s_38_) null)))) (= locCloseBrace_pre_40_25_13 locCloseBrace_40_25_13) (= locCloseBrace_40_25_13 (asField locCloseBrace_40_25_13 T_int)) (= INTLIT_pre_28_39_26 INTLIT_28_39_26) (= true_term (is INTLIT_28_39_26 T_int)) (= type_pre_101_18_28 type_101_18_28) (= type_101_18_28 (asField type_101_18_28 T_javafe_ast_Type)) (< (fClosedTime type_101_18_28) alloc) (forall ((?s_39_ Int)) (=> (not (= ?s_39_ null)) (not (= (S_select type_101_18_28 ?s_39_) null)))) (= METHODDECL_pre_30_20_7 METHODDECL_30_20_7) (= true_term (is METHODDECL_30_20_7 T_int)) (= args_pre_111_30_31 args_111_30_31) (= args_111_30_31 (asField args_111_30_31 T_javafe_ast_ExprVec)) (< (fClosedTime args_111_30_31) alloc) (forall ((?s_40_ Int)) (=> (not (= ?s_40_ null)) (not (= (S_select args_111_30_31 ?s_40_) null)))) (= ht_pre_155_33_36 ht_155_33_36) (= ht_155_33_36 (asField ht_155_33_36 T_java_util_Hashtable)) (< (fClosedTime ht_155_33_36) alloc) (forall ((?s_41_ Int)) (=> (not (= ?s_41_ null)) (not (= (S_select ht_155_33_36 ?s_41_) null)))) (= ASGMUL_pre_29_41_26 ASGMUL_29_41_26) (= true_term (is ASGMUL_29_41_26 T_int)) (= typeEnv_pre_20_323_32 typeEnv_20_323_32) (= true_term (is typeEnv_20_323_32 T_javafe_ast_ASTDecoration)) (= true_term (isAllocated typeEnv_20_323_32 alloc)) (= elems_pre_18_41_39 elems_18_41_39) (= elems_18_41_39 (asField elems_18_41_39 T_javafe_ast_TypeDeclElemVec)) (< (fClosedTime elems_18_41_39) alloc) (forall ((?s_42_ Int)) (=> (not (= ?s_42_ null)) (not (= (S_select elems_18_41_39 ?s_42_) null)))) (= lengthFieldDecl_pre_38_917_40 lengthFieldDecl_38_917_40) (= true_term (is lengthFieldDecl_38_917_40 T_javafe_ast_FieldDecl)) (= true_term (isAllocated lengthFieldDecl_38_917_40 alloc)) (not (= lengthFieldDecl_38_917_40 null)) (= THISEXPR_pre_30_47_7 THISEXPR_30_47_7) (= true_term (is THISEXPR_30_47_7 T_int)) (= parent_pre_32_21_18 parent_32_21_18) (= parent_32_21_18 (asField parent_32_21_18 T_javafe_ast_TypeDecl)) (< (fClosedTime parent_32_21_18) alloc) (= count_pre_47_67_33 count_47_67_33) (= count_47_67_33 (asField count_47_67_33 T_int)) (= locFinally_pre_82_25_13 locFinally_82_25_13) (= locFinally_82_25_13 (asField locFinally_82_25_13 T_int)) (= count_pre_15_67_33 count_15_67_33) (= count_15_67_33 (asField count_15_67_33 T_int)) (= loc_pre_60_18_13 loc_60_18_13) (= loc_60_18_13 (asField loc_60_18_13 T_int)) (= type_pre_103_20_28 type_103_20_28) (= type_103_20_28 (asField type_103_20_28 T_javafe_ast_Type)) (< (fClosedTime type_103_20_28) alloc) (forall ((?s_43_ Int)) (=> (not (= ?s_43_ null)) (not (= (S_select type_103_20_28 ?s_43_) null)))) (= id_pre_91_21_34 id_91_21_34) (= id_91_21_34 (asField id_91_21_34 T_javafe_ast_Identifier)) (< (fClosedTime id_91_21_34) alloc) (forall ((?s_44_ Int)) (=> (not (= ?s_44_ null)) (not (= (S_select id_91_21_34 ?s_44_) null)))) (= BOOLEANLIT_pre_28_38_26 BOOLEANLIT_28_38_26) (= true_term (is BOOLEANLIT_28_38_26 T_int)) (= loc_pre_72_18_13 loc_72_18_13) (= loc_72_18_13 (asField loc_72_18_13 T_int)) (= CONSTRUCTORDECL_pre_30_19_7 CONSTRUCTORDECL_30_19_7) (= true_term (is CONSTRUCTORDECL_30_19_7 T_int)) (= ASSIGN_pre_29_40_26 ASSIGN_29_40_26) (= true_term (is ASSIGN_29_40_26 T_int)) (= TYPEMODIFIERPRAGMA_pre_27_28_26 TYPEMODIFIERPRAGMA_27_28_26) (= true_term (is TYPEMODIFIERPRAGMA_27_28_26 T_int)) (= ARRAYINIT_pre_30_46_7 ARRAYINIT_30_46_7) (= true_term (is ARRAYINIT_30_46_7 T_int)) (= els_pre_100_19_28 els_100_19_28) (= els_100_19_28 (asField els_100_19_28 T_javafe_ast_Expr)) (< (fClosedTime els_100_19_28) alloc) (forall ((?s_45_ Int)) (=> (not (= ?s_45_ null)) (not (= (S_select els_100_19_28 ?s_45_) null)))) (= member_pre_5_44_39 member_5_44_39) (= member_5_44_39 (asField member_5_44_39 T_boolean)) (= args_pre_95_34_31 args_95_34_31) (= args_95_34_31 (asField args_95_34_31 T_javafe_ast_ExprVec)) (< (fClosedTime args_95_34_31) alloc) (forall ((?s_46_ Int)) (=> (not (= ?s_46_ null)) (not (= (S_select args_95_34_31 ?s_46_) null)))) (= classPrefix_pre_92_25_14 classPrefix_92_25_14) (= classPrefix_92_25_14 (asField classPrefix_92_25_14 T_javafe_ast_Type)) (< (fClosedTime classPrefix_92_25_14) alloc) (= loc_pre_75_20_13 loc_75_20_13) (= loc_75_20_13 (asField loc_75_20_13 T_int)) (= SHORTTYPE_pre_28_36_26 SHORTTYPE_28_36_26) (= true_term (is SHORTTYPE_28_36_26 T_int)) (= locOpenParen_pre_111_28_13 locOpenParen_111_28_13) (= locOpenParen_111_28_13 (asField locOpenParen_111_28_13 T_int)) (= INTERFACEDECL_pre_30_18_7 INTERFACEDECL_30_18_7) (= true_term (is INTERFACEDECL_30_18_7 T_int)) (= inst_pre_93_29_44 inst_93_29_44) (= true_term (is inst_93_29_44 T_javafe_ast_PrettyPrint)) (= true_term (isAllocated inst_93_29_44 alloc)) (not (= inst_93_29_44 null)) (= init_pre_22_20_17 init_22_20_17) (= init_22_20_17 (asField init_22_20_17 T_javafe_ast_VarInit)) (< (fClosedTime init_22_20_17) alloc) (= TYPESIG_pre_26_6_28 TYPESIG_26_6_28) (= true_term (is TYPESIG_26_6_28 T_int)) (= STAR_pre_29_37_26 STAR_29_37_26) (= true_term (is STAR_29_37_26 T_int)) (= locCloseParen_pre_106_21_13 locCloseParen_106_21_13) (= locCloseParen_106_21_13 (asField locCloseParen_106_21_13 T_int)) (= allowedExceptions_pre_74_25 allowedExceptions_74_25) (= allowedExceptions_74_25 (asField allowedExceptions_74_25 T_javafe_tc_TypeSigVec)) (< (fClosedTime allowedExceptions_74_25) alloc) (= CATCHCLAUSE_pre_30_45_7 CATCHCLAUSE_30_45_7) (= true_term (is CATCHCLAUSE_30_45_7 T_int)) (= elements_pre_166_61_39 elements_166_61_39) (= elements_166_61_39 (asField elements_166_61_39 (array T_javafe_ast_Identifier))) (< (fClosedTime elements_166_61_39) alloc) (forall ((?s_47_ Int)) (=> (not (= ?s_47_ null)) (not (= (S_select elements_166_61_39 ?s_47_) null)))) (= elements_pre_90_61_36 elements_90_61_36) (= elements_90_61_36 (asField elements_90_61_36 (array T_javafe_ast_VarInit))) (< (fClosedTime elements_90_61_36) alloc) (forall ((?s_48_ Int)) (=> (not (= ?s_48_ null)) (not (= (S_select elements_90_61_36 ?s_48_) null)))) (= methods_pre_5_883_26 methods_5_883_26) (= methods_5_883_26 (asField methods_5_883_26 T_javafe_tc_MethodDeclVec)) (< (fClosedTime methods_5_883_26) alloc) (= NOTACCESSIBLE_pre_86_13_26 NOTACCESSIBLE_86_13_26) (= true_term (is NOTACCESSIBLE_86_13_26 T_int)) (= TYPEDECLELEMPRAGMA_pre_27_27_26 TYPEDECLELEMPRAGMA_27_27_26) (= true_term (is TYPEDECLELEMPRAGMA_27_27_26 T_int)) (= od_pre_91_19_40 od_91_19_40) (= od_91_19_40 (asField od_91_19_40 T_javafe_ast_ObjectDesignator)) (< (fClosedTime od_91_19_40) alloc) (forall ((?s_49_ Int)) (=> (not (= ?s_49_ null)) (not (= (S_select od_91_19_40 ?s_49_) null)))) (= doubleType_pre_38_115_4 doubleType_38_115_4) (= true_term (is doubleType_38_115_4 T_javafe_ast_PrimitiveType)) (= true_term (isAllocated doubleType_38_115_4 alloc)) (= parent_pre_22_18_18 parent_22_18_18) (= parent_22_18_18 (asField parent_22_18_18 T_javafe_ast_TypeDecl)) (< (fClosedTime parent_22_18_18) alloc) (= locOpenBrace_pre_40_22_13 locOpenBrace_40_22_13) (= locOpenBrace_40_22_13 (asField locOpenBrace_40_22_13 T_int)) (= BYTETYPE_pre_28_35_26 BYTETYPE_28_35_26) (= true_term (is BYTETYPE_28_35_26 T_int)) (= CLASSDECL_pre_30_17_7 CLASSDECL_30_17_7) (= true_term (is CLASSDECL_30_17_7 T_int)) (= expr_pre_102_15_28 expr_102_15_28) (= expr_102_15_28 (asField expr_102_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_102_15_28) alloc) (forall ((?s_50_ Int)) (=> (not (= ?s_50_ null)) (not (= (S_select expr_102_15_28 ?s_50_) null)))) (= MOD_pre_29_36_26 MOD_29_36_26) (= true_term (is MOD_29_36_26 T_int)) (= constructorSeq_pre_48_171_38 constructorSeq_48_171_38) (= constructorSeq_48_171_38 (asField constructorSeq_48_171_38 T_javafe_util_StackVector)) (< (fClosedTime constructorSeq_48_171_38) alloc) (forall ((?s_51_ Int)) (=> (not (= ?s_51_ null)) (not (= (S_select constructorSeq_48_171_38 ?s_51_) null)))) (= BADTYPECOMBO_pre_86_12_26 BADTYPECOMBO_86_12_26) (= true_term (is BADTYPECOMBO_86_12_26 T_int)) (= thn_pre_100_17_28 thn_100_17_28) (= thn_100_17_28 (asField thn_100_17_28 T_javafe_ast_Expr)) (< (fClosedTime thn_100_17_28) alloc) (forall ((?s_52_ Int)) (=> (not (= ?s_52_ null)) (not (= (S_select thn_100_17_28 ?s_52_) null)))) (= CONSTRUCTORINVOCATION_pre_30_44_7 CONSTRUCTORINVOCATION_30_44_7) (= true_term (is CONSTRUCTORINVOCATION_30_44_7 T_int)) (= superInterfaces_pre_18_34_35 superInterfaces_18_34_35) (= superInterfaces_18_34_35 (asField superInterfaces_18_34_35 T_javafe_ast_TypeNameVec)) (< (fClosedTime superInterfaces_18_34_35) alloc) (forall ((?s_53_ Int)) (=> (not (= ?s_53_ null)) (not (= (S_select superInterfaces_18_34_35 ?s_53_) null)))) (= elements_pre_122_61_38 elements_122_61_38) (= elements_122_61_38 (asField elements_122_61_38 (array T_javafe_ast_FieldDecl))) (< (fClosedTime elements_122_61_38) alloc) (forall ((?s_54_ Int)) (=> (not (= ?s_54_ null)) (not (= (S_select elements_122_61_38 ?s_54_) null)))) (= catchClauses_pre_83_20_38 catchClauses_83_20_38) (= catchClauses_83_20_38 (asField catchClauses_83_20_38 T_javafe_ast_CatchClauseVec)) (< (fClosedTime catchClauses_83_20_38) alloc) (forall ((?s_55_ Int)) (=> (not (= ?s_55_ null)) (not (= (S_select catchClauses_83_20_38 ?s_55_) null)))) (= locIds_pre_167_25_29 locIds_167_25_29) (= locIds_167_25_29 (asField locIds_167_25_29 ?v_0)) (< (fClosedTime locIds_167_25_29) alloc) (forall ((?s_56_ Int)) (=> (not (= ?s_56_ null)) (not (= (S_select locIds_167_25_29 ?s_56_) null)))) (= count_pre_45_67_33 count_45_67_33) (= count_45_67_33 (asField count_45_67_33 T_int)) (= type_pre_95_32_32 type_95_32_32) (= type_95_32_32 (asField type_95_32_32 T_javafe_ast_TypeName)) (< (fClosedTime type_95_32_32) alloc) (forall ((?s_57_ Int)) (=> (not (= ?s_57_ null)) (not (= (S_select type_95_32_32 ?s_57_) null)))) (= locOp_pre_104_43_13 locOp_104_43_13) (= locOp_104_43_13 (asField locOp_104_43_13 T_int)) (= expr_pre_60_15_28 expr_60_15_28) (= expr_60_15_28 (asField expr_60_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_60_15_28) alloc) (forall ((?s_58_ Int)) (=> (not (= ?s_58_ null)) (not (= (S_select expr_60_15_28 ?s_58_) null)))) (= loc_pre_82_22_13 loc_82_22_13) (= loc_82_22_13 (asField loc_82_22_13 T_int)) (= loc_pre_99_49_13 loc_99_49_13) (= loc_99_49_13 (asField loc_99_49_13 T_int)) (= expr_pre_113_22_28 expr_113_22_28) (= expr_113_22_28 (asField expr_113_22_28 T_javafe_ast_Expr)) (< (fClosedTime expr_113_22_28) alloc) (forall ((?s_59_ Int)) (=> (not (= ?s_59_ null)) (not (= (S_select expr_113_22_28 ?s_59_) null)))) (= NULLTYPE_pre_28_34_26 NULLTYPE_28_34_26) (= true_term (is NULLTYPE_28_34_26 T_int)) (= expr_pre_101_15_28 expr_101_15_28) (= expr_101_15_28 (asField expr_101_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_101_15_28) alloc) (forall ((?s_60_ Int)) (=> (not (= ?s_60_ null)) (not (= (S_select expr_101_15_28 ?s_60_) null)))) (= label_pre_72_15_20 label_72_15_20) (= label_72_15_20 (asField label_72_15_20 T_javafe_ast_Identifier)) (< (fClosedTime label_72_15_20) alloc) (= STMTPRAGMA_pre_27_26_26 STMTPRAGMA_27_26_26) (= true_term (is STMTPRAGMA_27_26_26 T_int)) (= ONDEMANDIMPORTDECL_pre_30_16_7 ONDEMANDIMPORTDECL_30_16_7) (= true_term (is ONDEMANDIMPORTDECL_30_16_7 T_int)) (= locOp_pre_105_32_13 locOp_105_32_13) (= locOp_105_32_13 (asField locOp_105_32_13 T_int)) (= DIV_pre_29_35_26 DIV_29_35_26) (= true_term (is DIV_29_35_26 T_int)) (= TRYCATCHSTMT_pre_30_43_7 TRYCATCHSTMT_30_43_7) (= true_term (is TRYCATCHSTMT_30_43_7 T_int)) (= currentStackBottom_pre_153_87_33 currentStackBottom_153_87_33) (= currentStackBottom_153_87_33 (asField currentStackBottom_153_87_33 T_int)) (= superCall_pre_42_24_17 superCall_42_24_17) (= superCall_42_24_17 (asField superCall_42_24_17 T_boolean)) (= stmt_pre_75_17_28 stmt_75_17_28) (= stmt_75_17_28 (asField stmt_75_17_28 T_javafe_ast_Stmt)) (< (fClosedTime stmt_75_17_28) alloc) (forall ((?s_61_ Int)) (=> (not (= ?s_61_ null)) (not (= (S_select stmt_75_17_28 ?s_61_) null)))) (= simpleName_pre_5_37_38 simpleName_5_37_38) (= simpleName_5_37_38 (asField simpleName_5_37_38 T_java_lang_String)) (< (fClosedTime simpleName_5_37_38) alloc) (= VOIDTYPE_pre_28_33_26 VOIDTYPE_28_33_26) (= true_term (is VOIDTYPE_28_33_26 T_int)) (= SINGLETYPEIMPORTDECL_pre_30_15_7 SINGLETYPEIMPORTDECL_30_15_7) (= true_term (is SINGLETYPEIMPORTDECL_30_15_7 T_int)) (= locId_pre_111_25_13 locId_111_25_13) (= locId_111_25_13 (asField locId_111_25_13 T_int)) (= locSuper_pre_114_20_13 locSuper_114_20_13) (= locSuper_114_20_13 (asField locSuper_114_20_13 T_int)) (= SUB_pre_29_34_26 SUB_29_34_26) (= true_term (is SUB_29_34_26 T_int)) (= AMBIGUOUS_pre_86_11_26 AMBIGUOUS_86_11_26) (= true_term (is AMBIGUOUS_86_11_26 T_int)) (= MODIFIERPRAGMA_pre_27_25_26 MODIFIERPRAGMA_27_25_26) (= true_term (is MODIFIERPRAGMA_27_25_26 T_int)) (= test_pre_100_15_28 test_100_15_28) (= test_100_15_28 (asField test_100_15_28 T_javafe_ast_Expr)) (< (fClosedTime test_100_15_28) alloc) (forall ((?s_62_ Int)) (=> (not (= ?s_62_ null)) (not (= (S_select test_100_15_28 ?s_62_) null)))) (= locCloseBrace_pre_88_24_13 locCloseBrace_88_24_13) (= locCloseBrace_88_24_13 (asField locCloseBrace_88_24_13 T_int)) (= TRYFINALLYSTMT_pre_30_42_7 TRYFINALLYSTMT_30_42_7) (= true_term (is TRYFINALLYSTMT_30_42_7 T_int)) (= locDot_pre_95_29_13 locDot_95_29_13) (= locDot_95_29_13 (asField locDot_95_29_13 T_int)) (= decl_pre_50_38_43 decl_50_38_43) (= decl_50_38_43 (asField decl_50_38_43 T_javafe_ast_GenericVarDecl)) (< (fClosedTime decl_50_38_43) alloc) (forall ((?s_63_ Int)) (=> (not (= ?s_63_ null)) (not (= (S_select decl_50_38_43 ?s_63_) null)))) (= id_pre_18_32_34 id_18_32_34) (= id_18_32_34 (asField id_18_32_34 T_javafe_ast_Identifier)) (< (fClosedTime id_18_32_34) alloc) (forall ((?s_64_ Int)) (=> (not (= ?s_64_ null)) (not (= (S_select id_18_32_34 ?s_64_) null)))) (= tryClause_pre_83_18_28 tryClause_83_18_28) (= tryClause_83_18_28 (asField tryClause_83_18_28 T_javafe_ast_Stmt)) (< (fClosedTime tryClause_83_18_28) alloc) (forall ((?s_65_ Int)) (=> (not (= ?s_65_ null)) (not (= (S_select tryClause_83_18_28 ?s_65_) null)))) (= stmts_pre_40_19_31 stmts_40_19_31) (= stmts_40_19_31 (asField stmts_40_19_31 T_javafe_ast_StmtVec)) (< (fClosedTime stmts_40_19_31) alloc) (forall ((?s_66_ Int)) (=> (not (= ?s_66_ null)) (not (= (S_select stmts_40_19_31 ?s_66_) null)))) (= loc_pre_79_22_13 loc_79_22_13) (= loc_79_22_13 (asField loc_79_22_13 T_int)) (= DOUBLETYPE_pre_28_32_26 DOUBLETYPE_28_32_26) (= true_term (is DOUBLETYPE_28_32_26 T_int)) (= NOTFOUND_pre_86_10_26 NOTFOUND_86_10_26) (= true_term (is NOTFOUND_86_10_26 T_int)) (= COMPILATIONUNIT_pre_30_14_7 COMPILATIONUNIT_30_14_7) (= true_term (is COMPILATIONUNIT_30_14_7 T_int)) (= loc_pre_77_18_13 loc_77_18_13) (= loc_77_18_13 (asField loc_77_18_13 T_int)) (= ADD_pre_29_33_26 ADD_29_33_26) (= true_term (is ADD_29_33_26 T_int)) (= intType_pre_38_111_4 intType_38_111_4) (= true_term (is intType_38_111_4 T_javafe_ast_PrimitiveType)) (= true_term (isAllocated intType_38_111_4 alloc)) (= FIRST_KEYWORD_pre_27_51_26 FIRST_KEYWORD_27_51_26) (= true_term (is FIRST_KEYWORD_27_51_26 T_int)) (= locType_pre_33_21_13 locType_33_21_13) (= locType_33_21_13 (asField locType_33_21_13 T_int)) (= SWITCHLABEL_pre_30_41_7 SWITCHLABEL_30_41_7) (= true_term (is SWITCHLABEL_30_41_7 T_int)) (= LEXICALPRAGMA_pre_27_24_26 LEXICALPRAGMA_27_24_26) (= true_term (is LEXICALPRAGMA_27_24_26 T_int)) (= enclosingType_pre_5_32_39 enclosingType_5_32_39) (= enclosingType_5_32_39 (asField enclosingType_5_32_39 T_javafe_tc_TypeSig)) (< (fClosedTime enclosingType_5_32_39) alloc) (= reason_pre_86_8_13 reason_86_8_13) (= reason_86_8_13 (asField reason_86_8_13 T_int)) (= right_pre_104_40_28 right_104_40_28) (= right_104_40_28 (asField right_104_40_28 T_javafe_ast_Expr)) (< (fClosedTime right_104_40_28) alloc) (forall ((?s_67_ Int)) (=> (not (= ?s_67_ null)) (not (= (S_select right_104_40_28 ?s_67_) null)))) (= expr_pre_75_15_28 expr_75_15_28) (= expr_75_15_28 (asField expr_75_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_75_15_28) alloc) (forall ((?s_68_ Int)) (=> (not (= ?s_68_ null)) (not (= (S_select expr_75_15_28 ?s_68_) null)))) (= locOpenParen_pre_106_18_13 locOpenParen_106_18_13) (= locOpenParen_106_18_13 (asField locOpenParen_106_18_13 T_int)) (= finallyClause_pre_82_19_28 finallyClause_82_19_28) (= finallyClause_82_19_28 (asField finallyClause_82_19_28 T_javafe_ast_Stmt)) (< (fClosedTime finallyClause_82_19_28) alloc) (forall ((?s_69_ Int)) (=> (not (= ?s_69_ null)) (not (= (S_select finallyClause_82_19_28 ?s_69_) null)))) (= dims_pre_99_45_31 dims_99_45_31) (= dims_99_45_31 (asField dims_99_45_31 T_javafe_ast_ExprVec)) (< (fClosedTime dims_99_45_31) alloc) (forall ((?s_70_ Int)) (=> (not (= ?s_70_ null)) (not (= (S_select dims_99_45_31 ?s_70_) null)))) (= FLOATTYPE_pre_28_31_26 FLOATTYPE_28_31_26) (= true_term (is FLOATTYPE_28_31_26 T_int)) (= expr_pre_105_29_28 expr_105_29_28) (= expr_105_29_28 (asField expr_105_29_28 T_javafe_ast_Expr)) (< (fClosedTime expr_105_29_28) alloc) (forall ((?s_71_ Int)) (=> (not (= ?s_71_ null)) (not (= (S_select expr_105_29_28 ?s_71_) null)))) (= returnType_pre_68_19 returnType_68_19) (= returnType_68_19 (asField returnType_68_19 T_javafe_ast_Type)) (< (fClosedTime returnType_68_19) alloc) (= URSHIFT_pre_29_32_26 URSHIFT_29_32_26) (= true_term (is URSHIFT_29_32_26 T_int)) (= locOpenParen_pre_110_30_13 locOpenParen_110_30_13) (= locOpenParen_110_30_13 (asField locOpenParen_110_30_13 T_int)) (= SKIPSTMT_pre_30_40_7 SKIPSTMT_30_40_7) (= true_term (is SKIPSTMT_30_40_7 T_int)) (= decl_pre_56_15_33 decl_56_15_33) (= decl_56_15_33 (asField decl_56_15_33 T_javafe_ast_ClassDecl)) (< (fClosedTime decl_56_15_33) alloc) (forall ((?s_72_ Int)) (=> (not (= ?s_72_ null)) (not (= (S_select decl_56_15_33 ?s_72_) null)))) (= pmodifiers_pre_18_30_27 pmodifiers_18_30_27) (= pmodifiers_18_30_27 (asField pmodifiers_18_30_27 T_javafe_ast_ModifierPragmaVec)) (< (fClosedTime pmodifiers_18_30_27) alloc) (= COMPOUNDNAME_pre_30_67_7 COMPOUNDNAME_30_67_7) (= true_term (is COMPOUNDNAME_30_67_7 T_int)) (= fields_pre_5_875_27 fields_5_875_27) (= fields_5_875_27 (asField fields_5_875_27 T_javafe_tc_FieldDeclVec)) (< (fClosedTime fields_5_875_27) alloc) (= CHARTYPE_pre_28_30_26 CHARTYPE_28_30_26) (= true_term (is CHARTYPE_28_30_26 T_int)) (= count_pre_24_67_33 count_24_67_33) (= count_24_67_33 (asField count_24_67_33 T_int)) (= init_pre_55_19_17 init_55_19_17) (= init_55_19_17 (asField init_55_19_17 T_javafe_ast_VarInit)) (< (fClosedTime init_55_19_17) alloc) (= RSHIFT_pre_29_31_26 RSHIFT_29_31_26) (= true_term (is RSHIFT_29_31_26 T_int)) (= modifiers_pre_18_28_13 modifiers_18_28_13) (= modifiers_18_28_13 (asField modifiers_18_28_13 T_int)) (= CU_pre_5_71_30 CU_5_71_30) (= CU_5_71_30 (asField CU_5_71_30 T_javafe_ast_CompilationUnit)) (< (fClosedTime CU_5_71_30) alloc) (= FORSTMT_pre_30_39_7 FORSTMT_30_39_7) (= true_term (is FORSTMT_30_39_7 T_int)) (= locOpenBrace_pre_88_21_13 locOpenBrace_88_21_13) (= locOpenBrace_88_21_13 (asField locOpenBrace_88_21_13 T_int)) (= tag_pre_124_32_13 tag_124_32_13) (= tag_124_32_13 (asField tag_124_32_13 T_int)) (= left_pre_104_38_28 left_104_38_28) (= left_104_38_28 (asField left_104_38_28 T_javafe_ast_Expr)) (< (fClosedTime left_104_38_28) alloc) (forall ((?s_73_ Int)) (=> (not (= ?s_73_ null)) (not (= (S_select left_104_38_28 ?s_73_) null)))) (= elements_pre_118_61_47 elements_118_61_47) (= elements_118_61_47 (asField elements_118_61_47 (array T_javafe_ast_TypeModifierPragma))) (< (fClosedTime elements_118_61_47) alloc) (forall ((?s_74_ Int)) (=> (not (= ?s_74_ null)) (not (= (S_select elements_118_61_47 ?s_74_) null)))) (= leftToRight_pre_65_22 leftToRight_65_22) (= leftToRight_65_22 (asField leftToRight_65_22 T_boolean)) (= specOnly_pre_18_26_17 specOnly_18_26_17) (= specOnly_18_26_17 (asField specOnly_18_26_17 T_boolean)) (= id_pre_111_20_34 id_111_20_34) (= id_111_20_34 (asField id_111_20_34 T_javafe_ast_Identifier)) (< (fClosedTime id_111_20_34) alloc) (forall ((?s_75_ Int)) (=> (not (= ?s_75_ null)) (not (= (S_select id_111_20_34 ?s_75_) null)))) (= SIMPLENAME_pre_30_66_7 SIMPLENAME_30_66_7) (= true_term (is SIMPLENAME_30_66_7 T_int)) (= lenId_pre_38_914_30 lenId_38_914_30) (= true_term (is lenId_38_914_30 T_javafe_ast_Identifier)) (= true_term (isAllocated lenId_38_914_30 alloc)) (= tryClause_pre_82_17_28 tryClause_82_17_28) (= tryClause_82_17_28 (asField tryClause_82_17_28 T_javafe_ast_Stmt)) (< (fClosedTime tryClause_82_17_28) alloc) (forall ((?s_76_ Int)) (=> (not (= ?s_76_ null)) (not (= (S_select tryClause_82_17_28 ?s_76_) null)))) (= LONGTYPE_pre_28_29_26 LONGTYPE_28_29_26) (= true_term (is LONGTYPE_28_29_26 T_int)) (= els_pre_79_19_28 els_79_19_28) (= els_79_19_28 (asField els_79_19_28 T_javafe_ast_Stmt)) (< (fClosedTime els_79_19_28) alloc) (forall ((?s_77_ Int)) (=> (not (= ?s_77_ null)) (not (= (S_select els_79_19_28 ?s_77_) null)))) (= hasParent_pre_19_149_30 hasParent_19_149_30) (= hasParent_19_149_30 (asField hasParent_19_149_30 T_boolean)) (= op_pre_105_26_13 op_105_26_13) (= op_105_26_13 (asField op_105_26_13 T_int)) (= count_pre_123_67_33 count_123_67_33) (= count_123_67_33 (asField count_123_67_33 T_int)) (= expr_pre_77_15_14 expr_77_15_14) (= expr_77_15_14 (asField expr_77_15_14 T_javafe_ast_Expr)) (< (fClosedTime expr_77_15_14) alloc) (= shortType_pre_38_139_4 shortType_38_139_4) ?v_20 (= true_term (isAllocated shortType_38_139_4 alloc)) (= LSHIFT_pre_29_30_26 LSHIFT_29_30_26) (= true_term (is LSHIFT_29_30_26 T_int)) (= enclosingInstance_pre_95_25_14 enclosingInstance_95_25_14) (= enclosingInstance_95_25_14 (asField enclosingInstance_95_25_14 T_javafe_ast_Expr)) (< (fClosedTime enclosingInstance_95_25_14) alloc) (= IFSTMT_pre_30_38_7 IFSTMT_30_38_7) (= true_term (is IFSTMT_30_38_7 T_int)) (= POSTFIXDEC_pre_29_63_26 POSTFIXDEC_29_63_26) (= true_term (is POSTFIXDEC_29_63_26 T_int)) (= loc_pre_160_18_13 loc_160_18_13) (= loc_160_18_13 (asField loc_160_18_13 T_int)) (= booleanType_pre_38_107_4 booleanType_38_107_4) (= true_term (is booleanType_38_107_4 T_javafe_ast_PrimitiveType)) (= true_term (isAllocated booleanType_38_107_4 alloc)) (= ARRAYTYPE_pre_30_65_7 ARRAYTYPE_30_65_7) (= true_term (is ARRAYTYPE_30_65_7 T_int)) (= expr_pre_106_15_28 expr_106_15_28) (= expr_106_15_28 (asField expr_106_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_106_15_28) alloc) (forall ((?s_78_ Int)) (=> (not (= ?s_78_ null)) (not (= (S_select expr_106_15_28 ?s_78_) null)))) (= loc_pre_124_50_13 loc_124_50_13) (= loc_124_50_13 (asField loc_124_50_13 T_int)) (= INTTYPE_pre_28_28_26 INTTYPE_28_28_26) (= true_term (is INTTYPE_28_28_26 T_int)) (= LT_pre_29_29_26 LT_29_29_26) (= true_term (is LT_29_29_26 T_int)) (= block_pre_51_28_33 block_51_28_33) (= block_51_28_33 (asField block_51_28_33 T_javafe_ast_BlockStmt)) (< (fClosedTime block_51_28_33) alloc) (forall ((?s_79_ Int)) (=> (not (= ?s_79_ null)) (not (= (S_select block_51_28_33 ?s_79_) null)))) (= LABELSTMT_pre_30_37_7 LABELSTMT_30_37_7) (= true_term (is LABELSTMT_30_37_7 T_int)) (= count_pre_43_67_33 count_43_67_33) (= count_43_67_33 (asField count_43_67_33 T_int)) (= POSTFIXINC_pre_29_62_26 POSTFIXINC_29_62_26) (= true_term (is POSTFIXINC_29_62_26 T_int)) (= op_pre_104_35_13 op_104_35_13) (= op_104_35_13 (asField op_104_35_13 T_int)) (= locId_pre_32_43_13 locId_32_43_13) (= locId_32_43_13 (asField locId_32_43_13 T_int)) (= noTokens_pre_27_212_27 noTokens_27_212_27) (= true_term (is noTokens_27_212_27 T_int)) (= od_pre_111_18_40 od_111_18_40) (= od_111_18_40 (asField od_111_18_40 T_javafe_ast_ObjectDesignator)) (< (fClosedTime od_111_18_40) alloc) (forall ((?s_80_ Int)) (=> (not (= ?s_80_ null)) (not (= (S_select od_111_18_40 ?s_80_) null)))) (= TYPENAME_pre_30_64_7 TYPENAME_30_64_7) (= true_term (is TYPENAME_30_64_7 T_int)) (= thn_pre_79_17_28 thn_79_17_28) (= thn_79_17_28 (asField thn_79_17_28 T_javafe_ast_Stmt)) (< (fClosedTime thn_79_17_28) alloc) (forall ((?s_81_ Int)) (=> (not (= ?s_81_ null)) (not (= (S_select thn_79_17_28 ?s_81_) null)))) (= BOOLEANTYPE_pre_28_27_26 BOOLEANTYPE_28_27_26) (= true_term (is BOOLEANTYPE_28_27_26 T_int)) (= owner_pre_4_35_28 owner_4_35_28) (= owner_4_35_28 (asField owner_4_35_28 T_java_lang_Object)) (< (fClosedTime owner_4_35_28) alloc) (= methodSeq_pre_48_167_38 methodSeq_48_167_38) (= methodSeq_48_167_38 (asField methodSeq_48_167_38 T_javafe_util_StackVector)) (< (fClosedTime methodSeq_48_167_38) alloc) (forall ((?s_82_ Int)) (=> (not (= ?s_82_ null)) (not (= (S_select methodSeq_48_167_38 ?s_82_) null)))) (= returnType_pre_33_18_28 returnType_33_18_28) (= returnType_33_18_28 (asField returnType_33_18_28 T_javafe_ast_Type)) (< (fClosedTime returnType_33_18_28) alloc) (forall ((?s_83_ Int)) (=> (not (= ?s_83_ null)) (not (= (S_select returnType_33_18_28 ?s_83_) null)))) (= loc_pre_121_30_13 loc_121_30_13) (= loc_121_30_13 (asField loc_121_30_13 T_int)) (= LE_pre_29_28_26 LE_29_28_26) (= true_term (is LE_29_28_26 T_int)) (= CONTINUESTMT_pre_30_36_7 CONTINUESTMT_30_36_7) (= true_term (is CONTINUESTMT_30_36_7 T_int)) (= loc_pre_78_18_13 loc_78_18_13) (= loc_78_18_13 (asField loc_78_18_13 T_int)) (= punctuationCodes_pre_27_164_19 punctuationCodes_27_164_19) (= true_term (is punctuationCodes_27_164_19 ?v_0)) (= true_term (isAllocated punctuationCodes_27_164_19 alloc)) (= elems_pre_88_18_34 elems_88_18_34) (= elems_88_18_34 (asField elems_88_18_34 T_javafe_ast_VarInitVec)) (< (fClosedTime elems_88_18_34) alloc) (forall ((?s_84_ Int)) (=> (not (= ?s_84_ null)) (not (= (S_select elems_88_18_34 ?s_84_) null)))) (= DEC_pre_29_59_26 DEC_29_59_26) (= true_term (is DEC_29_59_26 T_int)) (= rootSEnv_pre_54_45 rootSEnv_54_45) (= rootSEnv_54_45 (asField rootSEnv_54_45 T_javafe_tc_EnvForTypeSig)) (< (fClosedTime rootSEnv_54_45) alloc) (= count_pre_16_67_33 count_16_67_33) (= count_16_67_33 (asField count_16_67_33 T_int)) (= locFirstSemi_pre_74_36_13 locFirstSemi_74_36_13) (= locFirstSemi_74_36_13 (asField locFirstSemi_74_36_13 T_int)) (= SUPEROBJECTDESIGNATOR_pre_30_63_7 SUPEROBJECTDESIGNATOR_30_63_7) (= true_term (is SUPEROBJECTDESIGNATOR_30_63_7 T_int)) (= IDENT_pre_28_25_26 IDENT_28_25_26) (= true_term (is IDENT_28_25_26 T_int)) (= parent_pre_18_59_18 parent_18_59_18) (= parent_18_59_18 (asField parent_18_59_18 T_javafe_ast_TypeDecl)) (< (fClosedTime parent_18_59_18) alloc) (= elements_pre_47_61_43 elements_47_61_43) (= elements_47_61_43 (asField elements_47_61_43 (array T_javafe_ast_FormalParaDecl))) (< (fClosedTime elements_47_61_43) alloc) (forall ((?s_85_ Int)) (=> (not (= ?s_85_ null)) (not (= (S_select elements_47_61_43 ?s_85_) null)))) (= branchDecoration_pre_1898_31 branchDecoration_1898_31) (= true_term (is branchDecoration_1898_31 T_javafe_ast_ASTDecoration)) (= true_term (isAllocated branchDecoration_1898_31 alloc)) (= decl_pre_42_54_25 decl_42_54_25) (= decl_42_54_25 (asField decl_42_54_25 T_javafe_ast_ConstructorDecl)) (< (fClosedTime decl_42_54_25) alloc) (= locId_pre_73_20_13 locId_73_20_13) (= locId_73_20_13 (asField locId_73_20_13 T_int)) (= name_pre_46_18_28 name_46_18_28) (= name_46_18_28 (asField name_46_18_28 T_javafe_ast_Name)) (< (fClosedTime name_46_18_28) alloc) (forall ((?s_86_ Int)) (=> (not (= ?s_86_ null)) (not (= (S_select name_46_18_28 ?s_86_) null)))) (= count_pre_21_67_33 count_21_67_33) (= count_21_67_33 (asField count_21_67_33 T_int)) (= GT_pre_29_27_26 GT_29_27_26) (= true_term (is GT_29_27_26 T_int)) (= decl_pre_54_15_36 decl_54_15_36) (= decl_54_15_36 (asField decl_54_15_36 T_javafe_ast_LocalVarDecl)) (< (fClosedTime decl_54_15_36) alloc) (forall ((?s_87_ Int)) (=> (not (= ?s_87_ null)) (not (= (S_select decl_54_15_36 ?s_87_) null)))) (= elementType_pre_155_22_27 elementType_155_22_27) (= elementType_155_22_27 (asField elementType_155_22_27 T__TYPE)) (= elements_pre_15_61_36 elements_15_61_36) (= elements_15_61_36 (asField elements_15_61_36 (array T_javafe_tc_TypeSig))) (< (fClosedTime elements_15_61_36) alloc) (forall ((?s_88_ Int)) (=> (not (= ?s_88_ null)) (not (= (S_select elements_15_61_36 ?s_88_) null)))) (= BREAKSTMT_pre_30_35_7 BREAKSTMT_30_35_7) (= true_term (is BREAKSTMT_30_35_7 T_int)) (= INC_pre_29_58_26 INC_29_58_26) (= true_term (is INC_29_58_26 T_int)) (= init_pre_99_35_19 init_99_35_19) (= init_99_35_19 (asField init_99_35_19 T_javafe_ast_ArrayInit)) (< (fClosedTime init_99_35_19) alloc) (= byteType_pre_38_135_4 byteType_38_135_4) ?v_15 (= true_term (isAllocated byteType_38_135_4 alloc)) (= args_pre_42_51_31 args_42_51_31) (= args_42_51_31 (asField args_42_51_31 T_javafe_ast_ExprVec)) (< (fClosedTime args_42_51_31) alloc) (forall ((?s_89_ Int)) (=> (not (= ?s_89_ null)) (not (= (S_select args_42_51_31 ?s_89_) null)))) (= TYPEOBJECTDESIGNATOR_pre_30_62_7 TYPEOBJECTDESIGNATOR_30_62_7) (= true_term (is TYPEOBJECTDESIGNATOR_30_62_7 T_int)) (= sigDecoration_pre_5_104_38 sigDecoration_5_104_38) (= true_term (is sigDecoration_5_104_38 T_javafe_ast_ASTDecoration)) (= true_term (isAllocated sigDecoration_5_104_38 alloc)) (= expr_pre_79_15_28 expr_79_15_28) (= expr_79_15_28 (asField expr_79_15_28 T_javafe_ast_Expr)) (< (fClosedTime expr_79_15_28) alloc) (forall ((?s_90_ Int)) (=> (not (= ?s_90_ null)) (not (= (S_select expr_79_15_28 ?s_90_) null)))) (= value_pre_124_45_16 value_124_45_16) (= value_124_45_16 (asField value_124_45_16 T_java_lang_Object)) (< (fClosedTime value_124_45_16) alloc) (= elementCount_pre_153_79_33 elementCount_153_79_33) (= elementCount_153_79_33 (asField elementCount_153_79_33 T_int)) (= locOpenParen_pre_80_23_13 locOpenParen_80_23_13) (= locOpenParen_80_23_13 (asField locOpenParen_80_23_13 T_int)) (= modifiers_pre_51_24_13 modifiers_51_24_13) (= modifiers_51_24_13 (asField modifiers_51_24_13 T_int)) (= elementType_pre_153_43_27 elementType_153_43_27) (= elementType_153_43_27 (asField elementType_153_43_27 T__TYPE)) (= locId_pre_23_38_13 locId_23_38_13) (= locId_23_38_13 (asField locId_23_38_13 T_int)) (= decl_pre_112_26_38 decl_112_26_38) (= decl_112_26_38 (asField decl_112_26_38 T_javafe_ast_GenericVarDecl)) (< (fClosedTime decl_112_26_38) alloc) (forall ((?s_91_ Int)) (=> (not (= ?s_91_ null)) (not (= (S_select decl_112_26_38 ?s_91_) null)))) (= GE_pre_29_26_26 GE_29_26_26) (= true_term (is GE_29_26_26 T_int)) (= voidType_pre_38_103_4 voidType_38_103_4) (= true_term (is voidType_38_103_4 T_javafe_ast_PrimitiveType)) (= true_term (isAllocated voidType_38_103_4 alloc)) (= keywordStrings_pre_27_181_30 keywordStrings_27_181_30) (= true_term (is keywordStrings_27_181_30 ?v_1)) (= true_term (isAllocated keywordStrings_27_181_30 alloc)) (= myTypeDecl_pre_5_63_40 myTypeDecl_5_63_40) (= myTypeDecl_5_63_40 (asField myTypeDecl_5_63_40 T_javafe_ast_TypeDecl)) (< (fClosedTime myTypeDecl_5_63_40) alloc) (= THROWSTMT_pre_30_34_7 THROWSTMT_30_34_7) (= true_term (is THROWSTMT_30_34_7 T_int)) (= NULL_pre_44_60_26 NULL_44_60_26) (= true_term (is NULL_44_60_26 T_int)) (= parent_pre_51_22_18 parent_51_22_18) (= parent_51_22_18 (asField parent_51_22_18 T_javafe_ast_TypeDecl)) (< (fClosedTime parent_51_22_18) alloc) (= count_pre_84_67_33 count_84_67_33) (= count_84_67_33 (asField count_84_67_33 T_int)) (= rootIEnv_pre_51_45 rootIEnv_51_45) (= rootIEnv_51_45 (asField rootIEnv_51_45 T_javafe_tc_EnvForTypeSig)) (< (fClosedTime rootIEnv_51_45) alloc) (= BITNOT_pre_29_57_26 BITNOT_29_57_26) (= true_term (is BITNOT_29_57_26 T_int)) (= loc_pre_32_40_13 loc_32_40_13) (= loc_32_40_13 (asField loc_32_40_13 T_int)) (= EXPROBJECTDESIGNATOR_pre_30_61_7 EXPROBJECTDESIGNATOR_30_61_7) (= true_term (is EXPROBJECTDESIGNATOR_30_61_7 T_int)) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= true_term (is this T_javafe_tc_FlowInsensitiveChecks)) (= true_term (isAllocated this alloc)) (not (= this null)) (= true_term (is leftExpr_1535_39 T_javafe_ast_Expr)) (= true_term (isAllocated leftExpr_1535_39 alloc)) (= true_term (is rightExpr_1535_54 T_javafe_ast_Expr)) (= true_term (isAllocated rightExpr_1535_54 alloc)) ?v_2 ?v_4 ?v_12 ?v_17 ?v_34 ?v_62 (or ?v_59 (and ?v_2 ?v_70 ?v_71 ?v_3 ?v_72 (or ?v_39 (and ?v_4 ?v_73 ?v_74 ?v_5 ?v_75 (or (not (and ?v_6 ?v_7)) (and ?v_76 ?v_8 ?v_77 ?v_78 ?v_11 ?v_79 ?v_80 ?v_81 (or (and ?v_61 ?v_11 (or ?v_26 (and ?v_82 ?v_13 ?v_83 (or (and ?v_16 ?v_51) (and ?v_84 ?v_86 ?v_11 (or ?v_47 (and ?v_87 ?v_21 ?v_88 (or (and ?v_23 ?v_30) (and ?v_89 ?v_92 ?v_11 (or ?v_26 (and ?v_93 ?v_27 ?v_94 (or (and ?v_31 ?v_30) (and ?v_95 (or (and ?v_36 (not (and ?v_6 ?v_34))) (and ?v_96 (or (and ?v_41 (or ?v_39 (and ?v_4 ?v_42 ?v_43 ?v_44 (or (not ?v_40) (and ?v_40 ?v_45 (not ?v_46)))))) (and ?v_97 ?v_99 ?v_11 (or ?v_47 (and ?v_100 ?v_48 ?v_101 (or (and ?v_52 ?v_51) (and ?v_102 (or (and ?v_56 (not (and ?v_7 ?v_34))) (and ?v_103 ?v_104 (or ?v_59 (and ?v_2 ?v_105 ?v_106 ?v_107 (or (not ?v_60) (and ?v_60 ?v_108 (not ?v_109)))))))))))))))))))))))))))) (and ?v_112 ?v_11 (or (not (and ?v_6 ?v_62)) (and ?v_113 ?v_63 ?v_114 ?v_115 ?v_117 ?v_11 (or (not (and ?v_7 ?v_62)) (and ?v_118 ?v_66 ?v_119 ?v_120 ?v_122 ?v_11 ?v_123 ?v_124 ?v_125 ?v_126 ?v_11 (or (not (and ?v_2 ?v_7)) (and ?v_127 ?v_128 ?v_130 ?v_11 (not (and ?v_4 ?v_6))))))))))))))) (and ?v_2 ?v_70 ?v_71 ?v_3 ?v_72 ?v_4 ?v_73 ?v_74 ?v_5 ?v_75 ?v_76 ?v_8 ?v_77 (or (and ?v_9 ?v_11 ?v_11) (and ?v_78 ?v_11 ?v_79 ?v_80 ?v_81 (or (and ?v_61 ?v_11 ?v_82 ?v_13 ?v_83 ?v_84 (or (and ?v_85 ?v_11 ?v_11 ?v_91) (and ?v_86 ?v_11 ?v_87 ?v_21 ?v_88 ?v_89 (or (and ?v_90 ?v_11 ?v_11 ?v_91) (and ?v_92 ?v_11 ?v_93 ?v_27 ?v_94 ?v_95 ?v_96 ?v_97 (or (and ?v_98 ?v_11 ?v_11 (= RES_11_ RES_1536_24_1536_24)) (and ?v_99 ?v_11 ?v_100 ?v_48 ?v_101 ?v_102 ?v_103 (or (and ?v_104 ?v_2 ?v_105 ?v_106 ?v_107 ?v_60 ?v_108 ?v_109 (= true_term (is RES_1581_2_1581_2 T_boolean)) (= EC_1581_2_1581_2 ecReturn) (= RES_12_ RES_1581_2_1581_2) (= EC_11_ EC_1581_2_1581_2) (= tmp15_cand_1580_2 RES_1581_2_1581_2)) (and (not ?v_104) ?v_11 (= RES_12_ RES_7_) (= EC_11_ EC_7_) (= tmp15_cand_1580_2 false_term))) (or (and ?v_110 ?v_11 ?v_11 (= RES_11_ RES_1537_18_1537_18)) (and (not ?v_110) ?v_11 (= true_term (is RES_1591_18_1591_18 T_javafe_ast_Type)) (= true_term (isAllocated RES_1591_18_1591_18 alloc)) ?v_111 (=> ?v_111 (not (= RES_1591_18_1591_18 null))) ?v_11 (= RES_11_ RES_1591_18_1591_18)))))))))) (and ?v_112 ?v_11 ?v_113 ?v_63 ?v_114 ?v_115 (or (and ?v_116 ?v_11 ?v_11) (and ?v_117 ?v_11 ?v_118 ?v_66 ?v_119 ?v_120 (or (and ?v_121 ?v_11 ?v_11) (and ?v_122 ?v_11 ?v_123 ?v_124 ?v_125 (or (and ?v_126 ?v_11 ?v_127 ?v_128 (or (and ?v_129 ?v_11 ?v_11) (and ?v_130 ?v_11 ?v_131 ?v_132 ?v_133 ?v_11 ?v_11))) (and (or (and ?v_126 ?v_11 ?v_127 ?v_128 ?v_130 ?v_11 ?v_131 ?v_132 (not ?v_133) ?v_11 (= EC_12_ EC_1619_9_1619_9)) (and (not ?v_126) ?v_11 (= EC_12_ EC_10_))) ?v_11)))))))))) (not (= ecReturn ecReturn))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)