(set-logic AUFLIA)
(set-info :source | 
  Simplify front end test suite.
  This benchmark was translated by Michal Moskal.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun L_102.5 () Int)
(declare-fun integralOr (Int Int) Int)
(declare-fun type_86.35.28 () Int)
(declare-fun RES_88.1_0_126.5_0_127.18_127.18 () Int)
(declare-fun j_88.1_0_102.5_0_102.43 () Int)
(declare-fun arrayShapeMore (Int Int) Int)
(declare-fun typeEnv_pre_35.323.32 () Int)
(declare-fun integralAnd (Int Int) Int)
(declare-fun RES_6_ () Int)
(declare-fun T_.TYPE () Int)
(declare-fun T_javafe.ast.MethodDecl () Int)
(declare-fun EC_127.12_1_ () Int)
(declare-fun i_97.24_88.1_0_97.24_22.62.48 () Int)
(declare-fun elems_pre_6.27.35 () Int)
(declare-fun intFirst () Int)
(declare-fun syntax_21.28.29 () Int)
(declare-fun RES_88.1_0_126.5_0_144.29_144.29 () Int)
(declare-fun tmp13_88.1_0_102.5_0_115.3 () Int)
(declare-fun T_javafe.ast.FieldDecl () Int)
(declare-fun RES_7_ () Int)
(declare-fun eClosedTime (Int) Int)
(declare-fun int_m9223372036854775808 () Int)
(declare-fun EC_90.24 () Int)
(declare-fun EC_88.1_0_126.5_0_136.7_136.7 () Int)
(declare-fun elements_82.61.38 () Int)
(declare-fun S_143.10 () Int)
(declare-fun int_m2147483648 () Int)
(declare-fun T_java.lang.Comparable () Int)
(declare-fun T_javafe.ast.TypeName () Int)
(declare-fun TYPEDECLELEMPRAGMA_pre_56.27.26 () Int)
(declare-fun arrayPosition (Int) Int)
(declare-fun loc_pre_88.40.13 () Int)
(declare-fun TYPEDECLELEMPRAGMA_56.27.26 () Int)
(declare-fun RES_8_ () Int)
(declare-fun keywordStrings_56.181.30 () Int)
(declare-fun select1 (Int Int) Int)
(declare-fun select2 (Int Int Int) Int)
(declare-fun RES_88.1_0_126.5_0_126.27_126.27 () Int)
(declare-fun T_java.util.EscjavaKeyValue () Int)
(declare-fun T_javafe.ast.TypeDecl () Int)
(declare-fun EC_54.14_54.14 () Int)
(declare-fun T_long () Int)
(declare-fun RES_88.1_0_126.5_0_136.27_136.27 () Int)
(declare-fun elements_17.61.39 () Int)
(declare-fun RES_9_ () Int)
(declare-fun T_javafe.filespace.Extension () Int)
(declare-fun INTLIT_57.39.26 () Int)
(declare-fun C_126.5 () Int)
(declare-fun lockLE (Int Int) Bool)
(declare-fun classLiteral (Int) Int)
(declare-fun RES_88.1_0_102.5_1_102.35_102.35 () Int)
(declare-fun S_142.5 () Int)
(declare-fun lockLT (Int Int) Bool)
(declare-fun RES_127.12 () Int)
(declare-fun body_88.34.19 () Int)
(declare-fun T_float () Int)
(declare-fun alloc () Int)
(declare-fun elems_77.1 () Int)
(declare-fun id_26.32.34 () Int)
(declare-fun EC_88.1_0_88.29_88.29 () Int)
(declare-fun locOpenBrace_pre_88.36.13 () Int)
(declare-fun T_javafe.ast.Modifiers () Int)
(declare-fun asChild (Int Int) Int)
(declare-fun CONCVARSYM (Int) Int)
(declare-fun len_136.7_88.1_0_126.5_0_136.7_22.171.36 () Int)
(declare-fun T_int () Int)
(declare-fun EC_57.14_57.14 () Int)
(declare-fun otherCodes_pre_56.202.27 () Int)
(declare-fun EC_88.1_0_126.5_0_132.13_132.13 () Int)
(declare-fun locId_86.38.13 () Int)
(declare-fun RES_127.12_1_ () Int)
(declare-fun otherStrings_pre_56.193.30 () Int)
(declare-fun int_2147483647 () Int)
(declare-fun T_javafe.ast.GenericBlockStmt () Int)
(declare-fun elements_pre_17.61.39 () Int)
(declare-fun int_9223372036854775807 () Int)
(declare-fun RES_88.1_0_126.5_1_126.27_126.27 () Int)
(declare-fun T_byte () Int)
(declare-fun loc_6.30.13 () Int)
(declare-fun punctuationStrings_56.134.22 () Int)
(declare-fun j_loopold_88.1_0_102.14 () Int)
(declare-fun typeName_19.15.32 () Int)
(declare-fun store1 (Int Int Int) Int)
(declare-fun store2 (Int Int Int Int) Int)
(declare-fun body_pre_88.34.19 () Int)
(declare-fun FIRST_KEYWORD_56.51.26 () Int)
(declare-fun loc_57.14_57.14_15.98.40 () Int)
(declare-fun S_115.3 () Int)
(declare-fun owner_pre_4.35.28 () Int)
(declare-fun checkedField_pre_30.33 () Int)
(declare-fun max (Int) Int)
(declare-fun T_javafe.ast.ImportDecl () Int)
(declare-fun checkedField_30.33 () Int)
(declare-fun T_java.util.Map () Int)
(declare-fun LEXICALPRAGMA_pre_56.24.26 () Int)
(declare-fun LONGLIT_57.40.26 () Int)
(declare-fun noTokens_56.212.27 () Int)
(declare-fun FLOATLIT_pre_57.42.26 () Int)
(declare-fun count_17.67.33 () Int)
(declare-fun RES_90.24 () Int)
(declare-fun NULL_56.82.26 () Int)
(declare-fun STMTPRAGMA_pre_56.26.26 () Int)
(declare-fun L_88.1 () Int)
(declare-fun EC_88.1_0_102.5_0_114.15_114.15 () Int)
(declare-fun locOpenBrace_pre_26.51.13 () Int)
(declare-fun noTokens_pre_56.212.27 () Int)
(declare-fun otherStrings_56.193.30 () Int)
(declare-fun integralDiv (Int Int) Int)
(declare-fun NULL_15.60.26 () Int)
(declare-fun T_javafe.ast.Identifier () Int)
(declare-fun locCloseBrace_97.25.13 () Int)
(declare-fun TYPEMODIFIERPRAGMA_56.28.26 () Int)
(declare-fun locId_pre_86.38.13 () Int)
(declare-fun EC_loopold_88.1_0 () Int)
(declare-fun elems_6.27.35 () Int)
(declare-fun T_javafe.ast.TagConstants () Int)
(declare-fun T_java.lang.Class () Int)
(declare-fun L_126.5 () Int)
(declare-fun RES_52.18_52.18 () Int)
(declare-fun T_java.lang.Object () Int)
(declare-fun RES_88.1_0_126.5_0_141.6_141.6 () Int)
(declare-fun returnType_pre_87.18.28 () Int)
(declare-fun EC_88.1_0_102.5_0_113.21_113.21 () Int)
(declare-fun T_javafe.parser.TagConstants () Int)
(declare-fun pkgName_pre_6.21.14 () Int)
(declare-fun STRINGLIT_57.44.26 () Int)
(declare-fun imports_76.1 () Int)
(declare-fun longLast () Int)
(declare-fun T_javafe.ast.PrettyPrint () Int)
(declare-fun termConditional (Int Int Int) Int)
(declare-fun EC_88.1_0_102.5_0_111.21_111.21 () Int)
(declare-fun BOOLEANLIT_57.38.26 () Int)
(declare-fun i_loopold_88.10 () Int)
(declare-fun locCloseBrace_pre_26.54.13 () Int)
(declare-fun modifiers_pre_26.28.13 () Int)
(declare-fun EC_52.5_1_ () Int)
(declare-fun imports_pre_6.25.37 () Int)
(declare-fun loc_pre_6.30.13 () Int)
(declare-fun RES_90.24_1_ () Int)
(declare-fun T_java.util.Dictionary () Int)
(declare-fun bool_false () Int)
(declare-fun Smt.true () Int)
(declare-fun punctuationStrings_pre_56.134.22 () Int)
(declare-fun EC_88.1_0_126.5_0_140.18_140.18 () Int)
(declare-fun EC_88.1_0_102.5_0_116.22_116.22 () Int)
(declare-fun name_pre_20.18.28 () Int)
(declare-fun asLockSet (Int) Int)
(declare-fun integralMod (Int Int) Int)
(declare-fun T_javafe.ast.BlockStmt () Int)
(declare-fun EC_88.1_0_90.32_90.32 () Int)
(declare-fun count_pre_83.67.33 () Int)
(declare-fun EC_104.21 () Int)
(declare-fun EC_88.1_0_126.5_0_135.13_135.13 () Int)
(declare-fun Smt.false () Int)
(declare-fun typeof (Int) Int)
(declare-fun int_18446744073709551615 () Int)
(declare-fun RES_54.22_54.22 () Int)
(declare-fun EC_88.1_0_97.24_97.24 () Int)
(declare-fun owner_4.35.28 () Int)
(declare-fun RES_88.1_0_97.40_97.40 () Int)
(declare-fun length_22.50.25 () Int)
(declare-fun DOUBLELIT_pre_57.43.26 () Int)
(declare-fun stringCat (Int Int) Int)
(declare-fun otherCodes_56.202.27 () Int)
(declare-fun LAST_KEYWORD_pre_56.103.26 () Int)
(declare-fun T_boolean () Int)
(declare-fun EC_loopold_88.1_0_1_ () Int)
(declare-fun EC_52.18_52.18 () Int)
(declare-fun longFirst () Int)
(declare-fun decorationType_5.48.27 () Int)
(declare-fun returnType_87.18.28 () Int)
(declare-fun T_java.util.Hashtable () Int)
(declare-fun RES_10_ () Int)
(declare-fun NULL_pre_15.60.26 () Int)
(declare-fun EC_88.1_0_126.5_0_136.17_136.17 () Int)
(declare-fun RES_11_ () Int)
(declare-fun EC_10_ () Int)
(declare-fun arrayFresh (Int Int Int Int Int Int Int) Bool)
(declare-fun decorationType_pre_5.48.27 () Int)
(declare-fun locId_26.48.13 () Int)
(declare-fun locOpenBrace_88.36.13 () Int)
(declare-fun EC_88.1_0_126.5_0_144.14_144.14 () Int)
(declare-fun T_javafe.tc.Env () Int)
(declare-fun locOpenBrace_pre_97.22.13 () Int)
(declare-fun punctuationCodes_56.164.19 () Int)
(declare-fun RES () Int)
(declare-fun type_pre_86.35.28 () Int)
(declare-fun msg_140.18_88.1_0_126.5_0_140.18_24.220.45 () Int)
(declare-fun EC_11_ () Int)
(declare-fun i_88.1_0_88.37 () Int)
(declare-fun locType_pre_87.21.13 () Int)
(declare-fun RES_88.1_0_126.5_0_136.7_136.7 () Int)
(declare-fun LAST_KEYWORD_56.103.26 () Int)
(declare-fun count_pre_25.67.33 () Int)
(declare-fun S_118.9 () Int)
(declare-fun RES_88.1_0_102.5_0_113.21_113.21 () Int)
(declare-fun EC_12_ () Int)
(declare-fun EC_88.1_0_126.5_0_127.18_127.18 () Int)
(declare-fun intLast () Int)
(declare-fun EC_88.1_0_102.5_0_102.35_102.35 () Int)
(declare-fun arrayType () Int)
(declare-fun typeEnv_35.323.32 () Int)
(declare-fun FLOATLIT_57.42.26 () Int)
(declare-fun RES_88.1_0_102.5_0_111.21_111.21 () Int)
(declare-fun EC_88.1_0_102.5_0_114.24_114.24 () Int)
(declare-fun boolEq (Int Int) Bool)
(declare-fun EC_13_ () Int)
(declare-fun count_pre_82.67.33 () Int)
(declare-fun STMTPRAGMA_56.26.26 () Int)
(declare-fun T_javafe.ast.Name () Int)
(declare-fun arrayLength (Int) Int)
(declare-fun RES_88.1_1_88.29_88.29 () Int)
(declare-fun S_56.10 () Int)
(declare-fun locOpenBrace_26.51.13 () Int)
(declare-fun cast (Int Int) Int)
(declare-fun asElems (Int) Int)
(declare-fun locCloseBrace_pre_97.25.13 () Int)
(declare-fun locId_pre_26.48.13 () Int)
(declare-fun T_char () Int)
(declare-fun i_111.21_88.1_0_102.5_0_111.21_22.62.48 () Int)
(declare-fun whereDecoration_pre_35.597.41 () Int)
(declare-fun other_136.27_88.1_0_126.5_0_136.27_22.42.42 () Int)
(declare-fun EC_88.1_0_126.5_0_126.27_126.27 () Int)
(declare-fun tmp17_cand_135.22 () Int)
(declare-fun loc_18.18.13 () Int)
(declare-fun T_javafe.tc.CheckCompilationUnit () Int)
(declare-fun punctuationCodes_pre_56.164.19 () Int)
(declare-fun T_javafe.ast.ASTNode () Int)
(declare-fun RES_88.1_0_126.5_0_135.13_135.13 () Int)
(declare-fun T_javafe.tc.EnvForCU () Int)
(declare-fun locType_87.21.13 () Int)
(declare-fun divides (Int Int) Int)
(declare-fun name_20.18.28 () Int)
(declare-fun length_pre_22.50.25 () Int)
(declare-fun T_javafe.genericfile.GenericFile () Int)
(declare-fun elements_83.61.39 () Int)
(declare-fun RES_88.1_0_126.5_0_132.13_132.13 () Int)
(declare-fun T_javafe.ast.GenericVarDecl () Int)
(declare-fun T_javafe.ast.TypeDeclElem () Int)
(declare-fun InRange (Int Int) Bool)
(declare-fun loc_pre_18.18.13 () Int)
(declare-fun inst_pre_36.29.44 () Int)
(declare-fun MODIFIERPRAGMA_pre_56.25.26 () Int)
(declare-fun EC_88.1_0_126.5_0_140.27_140.27 () Int)
(declare-fun j_loopold_88.1_0_126.14 () Int)
(declare-fun msg_114.15_88.1_0_102.5_0_114.15_24.220.45 () Int)
(declare-fun EC_88.1_0_102.5_0_115.34_115.34 () Int)
(declare-fun modifiers_26.28.13 () Int)
(declare-fun CHARLIT_pre_57.41.26 () Int)
(declare-fun INTLIT_pre_57.39.26 () Int)
(declare-fun msg_56.6_56.6_16.69.34 () Int)
(declare-fun tmp9_cand_88.1_0_102.5_0_113.6 () Bool)
(declare-fun FIRST_KEYWORD_pre_56.51.26 () Int)
(declare-fun S_57.35 () Int)
(declare-fun refEQ (Int Int) Int)
(declare-fun NULL_pre_56.82.26 () Int)
(declare-fun T_javafe.ast.OperatorTags () Int)
(declare-fun EC_loopold () Int)
(declare-fun CHARLIT_57.41.26 () Int)
(declare-fun T_javafe.tc.TypeSig () Int)
(declare-fun EC_88.1_0_102.5_0_104.29_104.29 () Int)
(declare-fun elements_pre_83.61.39 () Int)
(declare-fun RES_88.1_0_102.5_0_114.15_114.15 () Int)
(declare-fun BOOLEANLIT_pre_57.38.26 () Int)
(declare-fun T_javafe.ast.ASTDecoration () Int)
(declare-fun RES_88.1_0_126.5_0_144.14_144.14 () Int)
(declare-fun IDENT_57.25.26 () Int)
(declare-fun T_javafe.ast.GeneratedTags () Int)
(declare-fun is (Int Int) Int)
(declare-fun EC_88.1_0_102.5_0_111.37_111.37 () Int)
(declare-fun locId_88.43.13 () Int)
(declare-fun T_javafe.ast.TypeDeclVec () Int)
(declare-fun integralEQ (Int Int) Int)
(declare-fun RES_104.21 () Int)
(declare-fun syntax_pre_21.28.29 () Int)
(declare-fun boolNE (Int Int) Bool)
(declare-fun EC_90.24_1_ () Int)
(declare-fun isNewArray (Int) Int)
(declare-fun S_117.9 () Int)
(declare-fun loc_144.14_88.1_0_126.5_0_144.14_15.152.36 () Int)
(declare-fun elems_pre () Int)
(declare-fun T_javafe.ast.Stmt () Int)
(declare-fun intShiftL (Int Int) Int)
(declare-fun nonnullelements (Int Int) Bool)
(declare-fun IDENT_pre_57.25.26 () Int)
(declare-fun multiply (Int Int) Int)
(declare-fun T_javafe.util.ErrorSet () Int)
(declare-fun RES_88.1_0_102.5_0_102.35_102.35 () Int)
(declare-fun integralGE (Int Int) Int)
(declare-fun EC_127.12 () Int)
(declare-fun count_83.67.33 () Int)
(declare-fun T_short () Int)
(declare-fun elements_25.61.37 () Int)
(declare-fun RES_88.1_0_102.5_0_114.24_114.24 () Int)
(declare-fun alloc_pre () Int)
(declare-fun loc_88.40.13 () Int)
(declare-fun integralGT (Int Int) Int)
(declare-fun EC () Int)
(declare-fun boolAnd (Int Int) Bool)
(declare-fun T_javafe.ast.Type () Int)
(declare-fun loc_26.45.13 () Int)
(declare-fun EC_1_ () Int)
(declare-fun T_javafe.tc.MethodDeclVec () Int)
(declare-fun arrayShapeOne (Int) Int)
(declare-fun T_double () Int)
(declare-fun EC_54.22_54.22 () Int)
(declare-fun after_54.22_54.22 () Int)
(declare-fun longShiftL (Int Int) Int)
(declare-fun T_java.io.Serializable () Int)
(declare-fun boolOr (Int Int) Bool)
(declare-fun N2_88.1_0_102.5_0_110.2 () Int)
(declare-fun int_4294967295 () Int)
(declare-fun modulo (Int Int) Int)
(declare-fun EC_88.1_0_126.5_0_144.29_144.29 () Int)
(declare-fun EC_2_ () Int)
(declare-fun EC_88.1_0_97.40_97.40 () Int)
(declare-fun EC_67.1_67.1 () Int)
(declare-fun locId_pre_88.43.13 () Int)
(declare-fun sigDecoration_pre_33.104.38 () Int)
(declare-fun C_88.1 () Int)
(declare-fun C_102.5 () Int)
(declare-fun loc_pre_26.45.13 () Int)
(declare-fun keywordStrings_pre_56.181.30 () Int)
(declare-fun locOpenBrace_97.22.13 () Int)
(declare-fun LONGLIT_pre_57.40.26 () Int)
(declare-fun RES_88.1_0_126.5_0_140.18_140.18 () Int)
(declare-fun count_pre_17.67.33 () Int)
(declare-fun RES_88.1_0_102.5_0_116.22_116.22 () Int)
(declare-fun EC_88.1_0_126.5_0_141.6_141.6 () Int)
(declare-fun EC_3_ () Int)
(declare-fun imports_6.25.37 () Int)
(declare-fun null () Int)
(declare-fun EC_56.6_56.6 () Int)
(declare-fun inst_36.29.44 () Int)
(declare-fun elements_pre_25.61.37 () Int)
(declare-fun j_88.1_0_126.5_0_126.35 () Int)
(declare-fun T_java.lang.Boolean () Int)
(declare-fun EC_52.5 () Int)
(declare-fun EC_88.1_0_126.5_0_136.27_136.27 () Int)
(declare-fun T_javafe.tc.FieldDeclVec () Int)
(declare-fun T_java.lang.String () Int)
(declare-fun EC_4_ () Int)
(declare-fun asField (Int Int) Int)
(declare-fun pkgName_6.21.14 () Int)
(declare-fun EC_88.1_0_102.5_1_102.35_102.35 () Int)
(declare-fun tmp9_cand_113.13 () Bool)
(declare-fun TYPEMODIFIERPRAGMA_pre_56.28.26 () Int)
(declare-fun elements_pre_82.61.38 () Int)
(declare-fun boolImplies (Int Int) Bool)
(declare-fun sigDecoration_33.104.38 () Int)
(declare-fun EC_5_ () Int)
(declare-fun integralLE (Int Int) Int)
(declare-fun RES_1_ () Int)
(declare-fun T_javafe.ast.ImportDeclVec () Int)
(declare-fun EC_61.1_61.1 () Int)
(declare-fun id_pre_26.32.34 () Int)
(declare-fun T_javafe.ast.CompilationUnit () Int)
(declare-fun RES_88.1_0_126.5_0_140.27_140.27 () Int)
(declare-fun tokenType_pre_23.90.8 () Int)
(declare-fun tmp22_88.1_0_126.5_0_141.3 () Int)
(declare-fun integralLT (Int Int) Int)
(declare-fun typeName_pre_19.15.32 () Int)
(declare-fun T_javafe.ast.SingleTypeImportDecl () Int)
(declare-fun count_25.67.33 () Int)
(declare-fun vAllocTime (Int) Int)
(declare-fun j_88.1_0_102.10 () Int)
(declare-fun EC_6_ () Int)
(declare-fun RES_88.1_0_102.5_0_115.34_115.34 () Int)
(declare-fun T_java.lang.Cloneable () Int)
(declare-fun RES_2_ () Int)
(declare-fun boolNot (Int) Bool)
(declare-fun refNE (Int Int) Int)
(declare-fun integralXor (Int Int) Int)
(declare-fun classDown (Int Int) Int)
(declare-fun N1_88.1_0_96.5 () Int)
(declare-fun T_javafe.util.Info () Int)
(declare-fun EC_7_ () Int)
(declare-fun integralNE (Int Int) Int)
(declare-fun RES_88.1_0_102.5_0_104.29_104.29 () Int)
(declare-fun RES_88.1_0_126.5_0_136.17_136.17 () Int)
(declare-fun RES_3_ () Int)
(declare-fun EC_88.1_0_126.5_1_126.27_126.27 () Int)
(declare-fun count_82.67.33 () Int)
(declare-fun STRINGLIT_pre_57.44.26 () Int)
(declare-fun RES_88.1_0_102.5_0_111.37_111.37 () Int)
(declare-fun tokenType_23.90.8 () Int)
(declare-fun arrayParent (Int) Int)
(declare-fun elemtype (Int) Int)
(declare-fun DOUBLELIT_57.43.26 () Int)
(declare-fun fClosedTime (Int) Int)
(declare-fun MODIFIERPRAGMA_56.25.26 () Int)
(declare-fun cu_48.60 () Int)
(declare-fun array (Int) Int)
(declare-fun EC_8_ () Int)
(declare-fun T_javafe.ast.RoutineDecl () Int)
(declare-fun T_javafe.util.Location () Int)
(declare-fun LS () Int)
(declare-fun RES_4_ () Int)
(declare-fun whereDecoration_35.597.41 () Int)
(declare-fun RES_88.1_0_90.32_90.32 () Int)
(declare-fun ecReturn () Int)
(declare-fun S_116.9 () Int)
(declare-fun EC_88.1_1_88.29_88.29 () Int)
(declare-fun isAllocated (Int Int) Bool)
(declare-fun elems () Int)
(declare-fun locCloseBrace_26.54.13 () Int)
(declare-fun subtypes (Int Int) Bool)
(declare-fun RES_88.1_0_88.29_88.29 () Int)
(declare-fun EC_9_ () Int)
(declare-fun RES_88.1_0_97.24_97.24 () Int)
(declare-fun LEXICALPRAGMA_56.24.26 () Int)
(declare-fun RES_5_ () Int)
(declare-fun RES_57.14_57.14 () Int)
(assert (subtypes T_javafe.ast.ImportDecl T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.ImportDecl (asChild T_javafe.ast.ImportDecl T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.ast.Type T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.Type (asChild T_javafe.ast.Type T_javafe.ast.ASTNode)))
(assert (subtypes T_java.util.EscjavaKeyValue T_java.lang.Object))
(assert (subtypes T_javafe.ast.GenericVarDecl T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.GenericVarDecl (asChild T_javafe.ast.GenericVarDecl T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.tc.MethodDeclVec T_java.lang.Object))
(assert (= T_javafe.tc.MethodDeclVec (asChild T_javafe.tc.MethodDeclVec T_java.lang.Object)))
(assert (subtypes T_javafe.genericfile.GenericFile T_java.lang.Object))
(assert (subtypes T_java.io.Serializable T_java.lang.Object))
(assert (subtypes T_javafe.ast.BlockStmt T_javafe.ast.GenericBlockStmt))
(assert (= T_javafe.ast.BlockStmt (asChild T_javafe.ast.BlockStmt T_javafe.ast.GenericBlockStmt)))
(assert (subtypes T_javafe.ast.Name T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.Name (asChild T_javafe.ast.Name T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.ast.GenericBlockStmt T_javafe.ast.Stmt))
(assert (= T_javafe.ast.GenericBlockStmt (asChild T_javafe.ast.GenericBlockStmt T_javafe.ast.Stmt)))
(assert (subtypes T_javafe.ast.TypeName T_javafe.ast.Type))
(assert (= T_javafe.ast.TypeName (asChild T_javafe.ast.TypeName T_javafe.ast.Type)))
(assert (subtypes T_javafe.ast.GeneratedTags T_java.lang.Object))
(assert (subtypes T_javafe.ast.CompilationUnit T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.CompilationUnit (asChild T_javafe.ast.CompilationUnit T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.ast.RoutineDecl T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.RoutineDecl (asChild T_javafe.ast.RoutineDecl T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.ast.RoutineDecl T_javafe.ast.TypeDeclElem))
(assert (subtypes T_javafe.ast.ImportDeclVec T_java.lang.Object))
(assert (= T_javafe.ast.ImportDeclVec (asChild T_javafe.ast.ImportDeclVec T_java.lang.Object)))
(assert (subtypes T_java.lang.Boolean T_java.lang.Object))
(assert (= T_java.lang.Boolean (asChild T_java.lang.Boolean T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.Boolean) (= ?t T_java.lang.Boolean)) :pattern ((subtypes ?t T_java.lang.Boolean)) )))
(assert (subtypes T_java.lang.Boolean T_java.io.Serializable))
(assert (subtypes T_javafe.ast.PrettyPrint T_java.lang.Object))
(assert (= T_javafe.ast.PrettyPrint (asChild T_javafe.ast.PrettyPrint T_java.lang.Object)))
(assert (subtypes T_javafe.tc.CheckCompilationUnit T_java.lang.Object))
(assert (= T_javafe.tc.CheckCompilationUnit (asChild T_javafe.tc.CheckCompilationUnit T_java.lang.Object)))
(assert (subtypes T_javafe.ast.Stmt T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.Stmt (asChild T_javafe.ast.Stmt T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.parser.TagConstants T_javafe.ast.TagConstants))
(assert (= T_javafe.parser.TagConstants (asChild T_javafe.parser.TagConstants T_javafe.ast.TagConstants)))
(assert (subtypes T_java.util.Hashtable T_java.util.Dictionary))
(assert (= T_java.util.Hashtable (asChild T_java.util.Hashtable T_java.util.Dictionary)))
(assert (subtypes T_java.util.Hashtable T_java.util.Map))
(assert (subtypes T_java.util.Hashtable T_java.lang.Cloneable))
(assert (subtypes T_java.util.Hashtable T_java.io.Serializable))
(assert (subtypes T_javafe.util.ErrorSet T_java.lang.Object))
(assert (= T_javafe.util.ErrorSet (asChild T_javafe.util.ErrorSet T_java.lang.Object)))
(assert (subtypes T_javafe.util.Info T_java.lang.Object))
(assert (= T_javafe.util.Info (asChild T_javafe.util.Info T_java.lang.Object)))
(assert (subtypes T_java.lang.Comparable T_java.lang.Object))
(assert (subtypes T_javafe.ast.TypeDeclElem T_java.lang.Object))
(assert (subtypes T_javafe.ast.Modifiers T_java.lang.Object))
(assert (= T_javafe.ast.Modifiers (asChild T_javafe.ast.Modifiers T_java.lang.Object)))
(assert (subtypes T_java.lang.Cloneable T_java.lang.Object))
(assert (subtypes T_javafe.filespace.Extension T_java.lang.Object))
(assert (= T_javafe.filespace.Extension (asChild T_javafe.filespace.Extension T_java.lang.Object)))
(assert (subtypes T_javafe.ast.TypeDeclVec T_java.lang.Object))
(assert (= T_javafe.ast.TypeDeclVec (asChild T_javafe.ast.TypeDeclVec T_java.lang.Object)))
(assert (subtypes T_javafe.ast.OperatorTags T_java.lang.Object))
(assert (= T_javafe.ast.OperatorTags (asChild T_javafe.ast.OperatorTags T_java.lang.Object)))
(assert (subtypes T_javafe.ast.OperatorTags T_javafe.ast.GeneratedTags))
(assert (subtypes T_javafe.ast.ASTDecoration T_java.lang.Object))
(assert (= T_javafe.ast.ASTDecoration (asChild T_javafe.ast.ASTDecoration T_java.lang.Object)))
(assert (subtypes T_javafe.ast.TagConstants T_javafe.ast.OperatorTags))
(assert (= T_javafe.ast.TagConstants (asChild T_javafe.ast.TagConstants T_javafe.ast.OperatorTags)))
(assert (subtypes T_java.lang.String T_java.lang.Object))
(assert (= T_java.lang.String (asChild T_java.lang.String T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.String) (= ?t T_java.lang.String)) :pattern ((subtypes ?t T_java.lang.String)) )))
(assert (subtypes T_java.lang.String T_java.io.Serializable))
(assert (subtypes T_java.lang.String T_java.lang.Comparable))
(assert (subtypes T_javafe.tc.Env T_java.lang.Object))
(assert (= T_javafe.tc.Env (asChild T_javafe.tc.Env T_java.lang.Object)))
(assert (subtypes T_javafe.ast.FieldDecl T_javafe.ast.GenericVarDecl))
(assert (= T_javafe.ast.FieldDecl (asChild T_javafe.ast.FieldDecl T_javafe.ast.GenericVarDecl)))
(assert (subtypes T_javafe.ast.FieldDecl T_javafe.ast.TypeDeclElem))
(assert (subtypes T_javafe.ast.ASTNode T_java.lang.Object))
(assert (= T_javafe.ast.ASTNode (asChild T_javafe.ast.ASTNode T_java.lang.Object)))
(assert (subtypes T_javafe.ast.ASTNode T_java.lang.Cloneable))
(assert (subtypes T_javafe.ast.Identifier T_java.lang.Object))
(assert (= T_javafe.ast.Identifier (asChild T_javafe.ast.Identifier T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_javafe.ast.Identifier) (= ?t T_javafe.ast.Identifier)) :pattern ((subtypes ?t T_javafe.ast.Identifier)) )))
(assert (subtypes T_javafe.ast.MethodDecl T_javafe.ast.RoutineDecl))
(assert (= T_javafe.ast.MethodDecl (asChild T_javafe.ast.MethodDecl T_javafe.ast.RoutineDecl)))
(assert (subtypes T_javafe.ast.TypeDecl T_javafe.ast.ASTNode))
(assert (= T_javafe.ast.TypeDecl (asChild T_javafe.ast.TypeDecl T_javafe.ast.ASTNode)))
(assert (subtypes T_javafe.ast.TypeDecl T_javafe.ast.TypeDeclElem))
(assert (subtypes T_java.util.Map T_java.lang.Object))
(assert (subtypes T_java.util.Map T_java.util.EscjavaKeyValue))
(assert (subtypes T_javafe.tc.TypeSig T_javafe.ast.Type))
(assert (= T_javafe.tc.TypeSig (asChild T_javafe.tc.TypeSig T_javafe.ast.Type)))
(assert (subtypes T_javafe.tc.FieldDeclVec T_java.lang.Object))
(assert (= T_javafe.tc.FieldDeclVec (asChild T_javafe.tc.FieldDeclVec T_java.lang.Object)))
(assert (subtypes T_javafe.tc.EnvForCU T_javafe.tc.Env))
(assert (= T_javafe.tc.EnvForCU (asChild T_javafe.tc.EnvForCU T_javafe.tc.Env)))
(assert (subtypes T_javafe.util.Location T_java.lang.Object))
(assert (= T_javafe.util.Location (asChild T_javafe.util.Location T_java.lang.Object)))
(assert (subtypes T_javafe.ast.SingleTypeImportDecl T_javafe.ast.ImportDecl))
(assert (= T_javafe.ast.SingleTypeImportDecl (asChild T_javafe.ast.SingleTypeImportDecl T_javafe.ast.ImportDecl)))
(assert (subtypes T_java.util.Dictionary T_java.lang.Object))
(assert (= T_java.util.Dictionary (asChild T_java.util.Dictionary T_java.lang.Object)))
(assert (subtypes T_java.util.Dictionary T_java.util.EscjavaKeyValue))
(assert (distinct arrayType T_boolean T_char T_byte T_short T_int T_long T_float T_double T_.TYPE T_javafe.ast.ImportDecl T_javafe.ast.Type T_java.util.EscjavaKeyValue T_javafe.ast.GenericVarDecl T_javafe.tc.MethodDeclVec T_javafe.genericfile.GenericFile T_java.io.Serializable T_javafe.ast.BlockStmt T_javafe.ast.Name T_javafe.ast.GenericBlockStmt T_javafe.ast.TypeName T_javafe.ast.GeneratedTags T_javafe.ast.CompilationUnit T_javafe.ast.RoutineDecl T_javafe.ast.ImportDeclVec T_java.lang.Boolean T_javafe.ast.PrettyPrint T_javafe.tc.CheckCompilationUnit T_javafe.ast.Stmt T_javafe.parser.TagConstants T_java.util.Hashtable T_javafe.util.ErrorSet T_javafe.util.Info T_java.lang.Comparable T_javafe.ast.TypeDeclElem T_javafe.ast.Modifiers T_java.lang.Cloneable T_javafe.filespace.Extension T_javafe.ast.TypeDeclVec T_javafe.ast.OperatorTags T_javafe.ast.ASTDecoration T_javafe.ast.TagConstants T_java.lang.String T_javafe.tc.Env T_javafe.ast.FieldDecl T_javafe.ast.ASTNode T_javafe.ast.Identifier T_javafe.ast.MethodDecl T_javafe.ast.TypeDecl T_java.util.Map T_javafe.tc.TypeSig T_javafe.tc.FieldDeclVec T_javafe.tc.EnvForCU T_javafe.util.Location T_java.lang.Object T_javafe.ast.SingleTypeImportDecl T_java.util.Dictionary))
(assert (= Smt.true (is NULL_56.82.26 T_int)))
(assert (= NULL_56.82.26 163))
(assert (= Smt.true (is TYPEMODIFIERPRAGMA_56.28.26 T_int)))
(assert (= TYPEMODIFIERPRAGMA_56.28.26 118))
(assert (= Smt.true (is STRINGLIT_57.44.26 T_int)))
(assert (= STRINGLIT_57.44.26 110))
(assert (= Smt.true (is IDENT_57.25.26 T_int)))
(assert (= IDENT_57.25.26 93))
(assert (= Smt.true (is otherCodes_56.202.27 (array T_int))))
(assert (not (= otherCodes_56.202.27 null)))
(assert (= (typeof otherCodes_56.202.27) (array T_int)))
(assert (= (arrayLength otherCodes_56.202.27) 15))
(assert (= Smt.true (is LAST_KEYWORD_56.103.26 T_int)))
(assert (= LAST_KEYWORD_56.103.26 183))
(assert (= Smt.true (is punctuationStrings_56.134.22 (array T_java.lang.String))))
(assert (not (= punctuationStrings_56.134.22 null)))
(assert (= (typeof punctuationStrings_56.134.22) (array T_java.lang.String)))
(assert (= (arrayLength punctuationStrings_56.134.22) 48))
(assert (= Smt.true (is punctuationCodes_56.164.19 (array T_int))))
(assert (not (= punctuationCodes_56.164.19 null)))
(assert (= (typeof punctuationCodes_56.164.19) (array T_int)))
(assert (= (arrayLength punctuationCodes_56.164.19) 48))
(assert (= Smt.true (is whereDecoration_35.597.41 T_javafe.ast.ASTDecoration)))
(assert (not (= whereDecoration_35.597.41 null)))
(assert (= (typeof whereDecoration_35.597.41) T_javafe.ast.ASTDecoration))
(assert (= Smt.true (is noTokens_56.212.27 T_int)))
(assert (= Smt.true (is LEXICALPRAGMA_56.24.26 T_int)))
(assert (= LEXICALPRAGMA_56.24.26 114))
(assert (= Smt.true (is LONGLIT_57.40.26 T_int)))
(assert (= LONGLIT_57.40.26 106))
(assert (= Smt.true (is sigDecoration_33.104.38 T_javafe.ast.ASTDecoration)))
(assert (not (= sigDecoration_33.104.38 null)))
(assert (= (typeof sigDecoration_33.104.38) T_javafe.ast.ASTDecoration))
(assert (= Smt.true (is TYPEDECLELEMPRAGMA_56.27.26 T_int)))
(assert (= TYPEDECLELEMPRAGMA_56.27.26 117))
(assert (= Smt.true (is NULL_15.60.26 T_int)))
(assert (= NULL_15.60.26 0))
(assert (= Smt.true (is DOUBLELIT_57.43.26 T_int)))
(assert (= DOUBLELIT_57.43.26 109))
(assert (= Smt.true (is FIRST_KEYWORD_56.51.26 T_int)))
(assert (= FIRST_KEYWORD_56.51.26 133))
(assert (= Smt.true (is INTLIT_57.39.26 T_int)))
(assert (= INTLIT_57.39.26 105))
(assert (= Smt.true (is STMTPRAGMA_56.26.26 T_int)))
(assert (= STMTPRAGMA_56.26.26 116))
(assert (= Smt.true (is keywordStrings_56.181.30 (array T_java.lang.String))))
(assert (not (= keywordStrings_56.181.30 null)))
(assert (= (typeof keywordStrings_56.181.30) (array T_java.lang.String)))
(assert (= (arrayLength keywordStrings_56.181.30) 51))
(assert (= Smt.true (is FLOATLIT_57.42.26 T_int)))
(assert (= FLOATLIT_57.42.26 108))
(assert (= Smt.true (is BOOLEANLIT_57.38.26 T_int)))
(assert (= BOOLEANLIT_57.38.26 104))
(assert (= Smt.true (is otherStrings_56.193.30 (array T_java.lang.String))))
(assert (not (= otherStrings_56.193.30 null)))
(assert (= (typeof otherStrings_56.193.30) (array T_java.lang.String)))
(assert (= (arrayLength otherStrings_56.193.30) 15))
(assert (= Smt.true (is MODIFIERPRAGMA_56.25.26 T_int)))
(assert (= MODIFIERPRAGMA_56.25.26 115))
(assert (= Smt.true (is CHARLIT_57.41.26 T_int)))
(assert (= CHARLIT_57.41.26 107))
(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 63)) (<= 1 (longShiftL 1 ?n))) :pattern ((longShiftL 1 ?n)) )))
(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 31)) (<= 1 (intShiftL 1 ?n))) :pattern ((intShiftL 1 ?n)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (and (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralXor ?x ?y))) :pattern ((integralXor ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralDiv ?x ?y))) (=> (and (<= 0 ?x) (< 0 ?y)) (and (<= 0 ?v_0) (<= ?v_0 ?x)))) :pattern ((integralDiv ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralOr ?x ?y))) (=> (and (<= 0 ?x) (<= 0 ?y)) (and (<= ?x ?v_0) (<= ?y ?v_0)))) :pattern ((integralOr ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?y) (<= (integralAnd ?x ?y) ?y)) :pattern ((integralAnd ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?x) (<= (integralAnd ?x ?y) ?x)) :pattern ((integralAnd ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (=> (or (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralAnd ?x ?y))) :pattern ((integralAnd ?x ?y)) )))
(assert (forall ((?t Int)) (! (let ((?v_0 (classLiteral ?t))) (and (not (= ?v_0 null)) (= Smt.true (is ?v_0 T_java.lang.Class)) (isAllocated ?v_0 alloc))) :pattern ((classLiteral ?t)) )))
(assert (forall ((?x Int) (?e Int)) (= (nonnullelements ?x ?e) (and (not (= ?x null)) (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i (arrayLength ?x))) (not (= (select1 (select1 ?e ?x) ?i) null))))))))
(assert (forall ((?b Int) (?x Int) (?y Int)) (! (=> (not (= ?b Smt.true)) (= (termConditional ?b ?x ?y) ?y)) :pattern ((termConditional ?b ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (termConditional Smt.true ?x ?y) ?x) :pattern ((termConditional Smt.true ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (refNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((refNE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (refEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((refEQ ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((integralNE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLT ?x ?y) Smt.true) (< ?x ?y)) :pattern ((integralLT ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLE ?x ?y) Smt.true) (<= ?x ?y)) :pattern ((integralLE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGT ?x ?y) Smt.true) (> ?x ?y)) :pattern ((integralGT ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGE ?x ?y) Smt.true) (>= ?x ?y)) :pattern ((integralGE ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (stringCat ?x ?y))) (and (not (= ?v_0 null)) (subtypes (typeof ?v_0) T_java.lang.String))) :pattern ((stringCat ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (integralEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((integralEQ ?x ?y)) )))
(assert (forall ((?a Int) (?b Int)) (= (boolOr ?a ?b) (or (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?a Int)) (= (boolNot ?a) (not (= ?a Smt.true)))))
(assert (forall ((?a Int) (?b Int)) (= (boolNE ?a ?b) (not (= (= ?a Smt.true) (= ?b Smt.true))))))
(assert (forall ((?a Int) (?b Int)) (= (boolImplies ?a ?b) (=> (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?a Int) (?b Int)) (= (boolEq ?a ?b) (= (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?a Int) (?b Int)) (= (boolAnd ?a ?b) (and (= ?a Smt.true) (= ?b Smt.true)))))
(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (multiply ?x ?y))) (= (multiply (integralDiv ?v_0 ?y) ?y) ?v_0))))
(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?j ?i) ?j) (integralMod ?i ?j))))
(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?i ?j) ?j) (integralMod ?i ?j))))
(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< ?j 0) (and (< ?j ?v_0) (<= ?v_0 0)))) :pattern ((integralMod ?i ?j)) )))
(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< 0 ?j) (and (<= 0 ?v_0) (< ?v_0 ?j)))) :pattern ((integralMod ?i ?j)) )))
(assert (forall ((?i Int) (?j Int)) (! (= (+ (multiply (integralDiv ?i ?j) ?j) (integralMod ?i ?j)) ?i) :pattern ((integralMod ?i ?j))  :pattern ((integralDiv ?i ?j)) )))
(assert (forall ((?s Int)) (! (=> (= Smt.true (isNewArray ?s)) (subtypes (typeof ?s) arrayType)) :pattern ((isNewArray ?s)) )))
(assert (forall ((?t Int)) (! (subtypes (array ?t) arrayType) :pattern ((array ?t)) )))
(assert (= arrayType (asChild arrayType T_java.lang.Object)))
(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (= (select1 (select1 ?e ?a) ?i) ?v) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v)) )))
(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?s Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (let ((?v_0 (select1 (select1 ?e ?a) ?i))) (and (arrayFresh ?v_0 ?a0 ?b0 ?e ?s (elemtype ?T) ?v) (= (arrayParent ?v_0) ?a) (= (arrayPosition ?v_0) ?i))) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v)) )))
(assert (forall ((?a Int)) (! (let ((?v_0 (arrayLength ?a))) (and (<= 0 ?v_0) (= Smt.true (is ?v_0 T_int)))) :pattern ((arrayLength ?a)) )))
(assert (forall ((?x Int)) (! (=> (subtypes (typeof ?x) T_java.lang.Object) (lockLE null ?x)) :pattern ((lockLE null ?x))  :pattern ((lockLT null ?x))  :pattern ((lockLE ?x null))  :pattern ((lockLT ?x null)) )))
(assert (forall ((?S Int) (?mu Int)) (let ((?v_0 (asLockSet ?S))) (=> (= (select1 ?v_0 ?mu) Smt.true) (lockLE ?mu (max ?v_0))))))
(assert (forall ((?x Int) (?y Int)) (= (lockLT ?x ?y) (< ?x ?y))))
(assert (forall ((?x Int) (?y Int)) (= (lockLE ?x ?y) (<= ?x ?y))))
(assert (forall ((?S Int)) (! (= (select1 (asLockSet ?S) null) Smt.true) :pattern ((asLockSet ?S)) )))
(assert (forall ((?S Int)) (let ((?v_0 (asLockSet ?S))) (= (select1 ?v_0 (max ?v_0)) Smt.true))))
(assert (forall ((?a Int) (?e Int) (?i Int) (?a0 Int)) (! (=> (and (< (eClosedTime ?e) ?a0) (isAllocated ?a ?a0)) (isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) :pattern ((isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) )))
(assert (forall ((?x Int) (?f Int) (?a0 Int)) (! (=> (and (< (fClosedTime ?f) ?a0) (isAllocated ?x ?a0)) (isAllocated (select1 ?f ?x) ?a0)) :pattern ((isAllocated (select1 ?f ?x) ?a0)) )))
(assert (forall ((?x Int) (?a0 Int)) (= (isAllocated ?x ?a0) (< (vAllocTime ?x) ?a0))))
(assert (forall ((?e Int) (?a Int) (?i Int)) (! (= Smt.true (is (select1 (select1 (asElems ?e) ?a) ?i) (elemtype (typeof ?a)))) :pattern ((select1 (select1 (asElems ?e) ?a) ?i)) )))
(assert (forall ((?f Int) (?t Int) (?x Int)) (! (= Smt.true (is (select1 (asField ?f ?t) ?x) ?t)) :pattern ((select1 (asField ?f ?t) ?x)) )))
(assert (forall ((?x Int) (?t Int)) (! (=> (subtypes ?t T_java.lang.Object) (= (= Smt.true (is ?x ?t)) (or (= ?x null) (subtypes (typeof ?x) ?t)))) :pattern ((subtypes ?t T_java.lang.Object) (is ?x ?t)) )))
(assert (< intLast longLast))
(assert (< 1000000 intLast))
(assert (< intFirst (- 1000000)))
(assert (< longFirst intFirst))
(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_long)) (and (<= longFirst ?x) (<= ?x longLast))) :pattern ((is ?x T_long)) )))
(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_int)) (and (<= intFirst ?x) (<= ?x intLast))) :pattern ((is ?x T_int)) )))
(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_short)) (and (<= (- 32768) ?x) (<= ?x 32767)))))
(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_byte)) (and (<= (- 128) ?x) (<= ?x 127)))))
(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_char)) (and (<= 0 ?x) (<= ?x 65535))) :pattern ((is ?x T_char)) )))
(assert (distinct bool_false Smt.true))
(assert (forall ((?x Int) (?t Int)) (! (=> (= Smt.true (is ?x ?t)) (= (cast ?x ?t) ?x)) :pattern ((cast ?x ?t)) )))
(assert (forall ((?x Int) (?t Int)) (! (= Smt.true (is (cast ?x ?t) ?t)) :pattern ((cast ?x ?t)) )))
(assert (forall ((?t0 Int) (?t1 Int)) (! (let ((?v_0 (elemtype ?t0))) (= (subtypes ?t0 (array ?t1)) (and (= ?t0 (array ?v_0)) (subtypes ?v_0 ?t1)))) :pattern ((subtypes ?t0 (array ?t1))) )))
(assert (forall ((?t Int)) (! (= (elemtype (array ?t)) ?t) :pattern ((elemtype (array ?t))) )))
(assert (forall ((?t Int)) (! (subtypes (array ?t) T_java.lang.Cloneable) :pattern ((array ?t)) )))
(assert (subtypes T_java.lang.Cloneable T_java.lang.Object))
(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (let ((?v_0 (asChild ?t1 ?t2))) (=> (subtypes ?t0 ?v_0) (= (classDown ?t2 ?t0) ?v_0)))))
(assert (forall ((?t Int)) (! (=> (subtypes T_double ?t) (= ?t T_double)) :pattern ((subtypes T_double ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_float ?t) (= ?t T_float)) :pattern ((subtypes T_float ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_long ?t) (= ?t T_long)) :pattern ((subtypes T_long ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_int ?t) (= ?t T_int)) :pattern ((subtypes T_int ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_short ?t) (= ?t T_short)) :pattern ((subtypes T_short ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_byte ?t) (= ?t T_byte)) :pattern ((subtypes T_byte ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_char ?t) (= ?t T_char)) :pattern ((subtypes T_char ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes T_boolean ?t) (= ?t T_boolean)) :pattern ((subtypes T_boolean ?t)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_double) (= ?t T_double)) :pattern ((subtypes ?t T_double)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_float) (= ?t T_float)) :pattern ((subtypes ?t T_float)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_long) (= ?t T_long)) :pattern ((subtypes ?t T_long)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_int) (= ?t T_int)) :pattern ((subtypes ?t T_int)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_short) (= ?t T_short)) :pattern ((subtypes ?t T_short)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_byte) (= ?t T_byte)) :pattern ((subtypes ?t T_byte)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_char) (= ?t T_char)) :pattern ((subtypes ?t T_char)) )))
(assert (forall ((?t Int)) (! (=> (subtypes ?t T_boolean) (= ?t T_boolean)) :pattern ((subtypes ?t T_boolean)) )))
(assert (forall ((?t0 Int) (?t1 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) (= ?t0 ?t1)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) )))
(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) (subtypes ?t0 ?t2)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) )))
(assert (subtypes T_java.lang.Object T_java.lang.Object))
(assert (forall ((?t Int)) (! (subtypes ?t ?t) :pattern ((subtypes ?t ?t)) )))
(assert (forall ((?m Int) (?i Int) (?j Int) (?x Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?m ?i ?x) ?j) (select1 ?m ?j)))))
(assert (forall ((?m Int) (?i Int) (?x Int)) (= (select1 (store1 ?m ?i ?x) ?i) ?x)))
(assert (let ((?v_0 (array T_int)) (?v_1 (array T_java.lang.String)) (?v_4 (arrayLength punctuationStrings_56.134.22)) (?v_3 (arrayLength keywordStrings_56.181.30)) (?v_5 (arrayLength otherStrings_56.193.30)) (?v_7 (not (= cu_48.60 null))) (?v_2 (select1 owner_4.35.28 punctuationCodes_56.164.19)) (?v_9 (select1 decorationType_5.48.27 checkedField_30.33)) (?v_6 (not (= checkedField_30.33 null)))) (let ((?v_10 (not ?v_6)) (?v_11 (not ?v_7)) (?v_173 (= Smt.true (is RES_52.18_52.18 T_java.lang.Object))) (?v_174 (isAllocated RES_52.18_52.18 alloc)) (?v_8 (= EC_52.18_52.18 ecReturn))) (let ((?v_175 (=> ?v_8 (subtypes (typeof RES_52.18_52.18) ?v_9))) (?v_202 (not (= RES_52.18_52.18 null)))) (let ((?v_176 (not ?v_202)) (?v_17 (= Smt.true Smt.true)) (?v_177 (< alloc after_54.22_54.22)) (?v_178 (not (= RES_54.22_54.22 null))) (?v_179 (not (isAllocated RES_54.22_54.22 alloc))) (?v_180 (= Smt.true (is RES_54.22_54.22 T_java.lang.Boolean))) (?v_181 (isAllocated RES_54.22_54.22 after_54.22_54.22)) (?v_182 (= EC_54.22_54.22 ecReturn)) (?v_183 (= (select1 owner_4.35.28 RES_54.22_54.22) null)) (?v_12 (typeof RES_54.22_54.22))) (let ((?v_184 (= ?v_12 T_java.lang.Boolean)) (?v_13 (subtypes ?v_12 ?v_9)) (?v_185 (= EC_54.14_54.14 ecReturn)) (?v_14 (= loc_57.14_57.14_15.98.40 (select1 loc_6.30.13 cu_48.60))) (?v_15 (not (= loc_57.14_57.14_15.98.40 NULL_15.60.26))) (?v_186 (= Smt.true (is RES_57.14_57.14 T_java.lang.String))) (?v_187 (isAllocated RES_57.14_57.14 after_54.22_54.22)) (?v_16 (= EC_57.14_57.14 ecReturn))) (let ((?v_188 (=> ?v_16 (not (= RES_57.14_57.14 null)))) (?v_189 (= msg_56.6_56.6_16.69.34 (stringCat (stringCat S_56.10 RES_57.14_57.14) S_57.35))) (?v_190 (= EC_56.6_56.6 ecReturn)) (?v_191 (= EC_61.1_61.1 ecReturn)) (?v_192 (= EC_67.1_67.1 ecReturn)) (?v_193 (= imports_76.1 (select1 imports_6.25.37 cu_48.60))) (?v_194 (= elems_77.1 (select1 elems_6.27.35 cu_48.60))) (?v_195 (= EC_67.1_67.1 EC_loopold)) (?v_196 (= 0 i_loopold_88.10)) (?v_18 (not (= imports_76.1 null)))) (let ((?v_20 (not ?v_18)) (?v_149 (= Smt.true (is RES_88.1_0_88.29_88.29 T_int))) (?v_19 (= EC_88.1_0_88.29_88.29 ecReturn)) (?v_21 (select1 count_17.67.33 imports_76.1))) (let ((?v_150 (=> ?v_19 (= RES_88.1_0_88.29_88.29 ?v_21))) (?v_151 (< 0 RES_88.1_0_88.29_88.29)) (?v_48 (<= 0 0)) (?v_152 (= Smt.true (is RES_88.1_0_90.32_90.32 T_javafe.ast.ImportDecl))) (?v_153 (isAllocated RES_88.1_0_90.32_90.32 after_54.22_54.22)) (?v_22 (= EC_88.1_0_90.32_90.32 ecReturn)) (?v_23 (not (= RES_88.1_0_90.32_90.32 null)))) (let ((?v_154 (=> ?v_22 ?v_23)) (?v_24 (= Smt.true (is RES_88.1_0_90.32_90.32 T_javafe.ast.SingleTypeImportDecl))) (?v_26 (cast RES_88.1_0_90.32_90.32 T_javafe.ast.SingleTypeImportDecl))) (let ((?v_25 (not (= ?v_26 null))) (?v_155 (= N1_88.1_0_96.5 (select1 name_20.18.28 (select1 typeName_19.15.32 ?v_26)))) (?v_27 (not (= N1_88.1_0_96.5 null)))) (let ((?v_29 (not ?v_27)) (?v_156 (= Smt.true (is RES_88.1_0_97.40_97.40 T_int))) (?v_28 (= EC_88.1_0_97.40_97.40 ecReturn)) (?v_30 (select1 length_22.50.25 N1_88.1_0_96.5))) (let ((?v_157 (=> ?v_28 (= RES_88.1_0_97.40_97.40 ?v_30))) (?v_31 (= i_97.24_88.1_0_97.24_22.62.48 (- RES_88.1_0_97.40_97.40 1))) (?v_158 (= Smt.true (is RES_88.1_0_97.24_97.24 T_javafe.ast.Identifier))) (?v_159 (isAllocated RES_88.1_0_97.24_97.24 after_54.22_54.22)) (?v_32 (= EC_88.1_0_97.24_97.24 ecReturn))) (let ((?v_160 (=> ?v_32 (not (= RES_88.1_0_97.24_97.24 null)))) (?v_148 (+ 0 1))) (let ((?v_77 (= j_88.1_0_102.10 ?v_148)) (?v_78 (= EC_88.1_0_97.24_97.24 EC_loopold_88.1_0)) (?v_79 (= j_88.1_0_102.10 j_loopold_88.1_0_102.14)) (?v_53 (= Smt.true (is RES_88.1_0_102.5_0_102.35_102.35 T_int))) (?v_33 (= EC_88.1_0_102.5_0_102.35_102.35 ecReturn))) (let ((?v_54 (=> ?v_33 (= RES_88.1_0_102.5_0_102.35_102.35 ?v_21))) (?v_55 (< j_88.1_0_102.10 RES_88.1_0_102.5_0_102.35_102.35)) (?v_56 (= Smt.true (is RES_88.1_0_102.5_0_104.29_104.29 T_javafe.ast.ImportDecl))) (?v_57 (isAllocated RES_88.1_0_102.5_0_104.29_104.29 after_54.22_54.22)) (?v_34 (= EC_88.1_0_102.5_0_104.29_104.29 ecReturn)) (?v_35 (not (= RES_88.1_0_102.5_0_104.29_104.29 null)))) (let ((?v_58 (=> ?v_34 ?v_35)) (?v_36 (= Smt.true (is RES_88.1_0_102.5_0_104.29_104.29 T_javafe.ast.SingleTypeImportDecl))) (?v_38 (cast RES_88.1_0_102.5_0_104.29_104.29 T_javafe.ast.SingleTypeImportDecl))) (let ((?v_37 (not (= ?v_38 null))) (?v_59 (= N2_88.1_0_102.5_0_110.2 (select1 name_20.18.28 (select1 typeName_19.15.32 ?v_38)))) (?v_47 (= N2_88.1_0_102.5_0_110.2 null))) (let ((?v_39 (not ?v_47))) (let ((?v_41 (not ?v_39)) (?v_60 (= Smt.true (is RES_88.1_0_102.5_0_111.37_111.37 T_int))) (?v_40 (= EC_88.1_0_102.5_0_111.37_111.37 ecReturn)) (?v_42 (select1 length_22.50.25 N2_88.1_0_102.5_0_110.2))) (let ((?v_61 (=> ?v_40 (= RES_88.1_0_102.5_0_111.37_111.37 ?v_42))) (?v_43 (= i_111.21_88.1_0_102.5_0_111.21_22.62.48 (- RES_88.1_0_102.5_0_111.37_111.37 1))) (?v_62 (= Smt.true (is RES_88.1_0_102.5_0_111.21_111.21 T_javafe.ast.Identifier))) (?v_63 (isAllocated RES_88.1_0_102.5_0_111.21_111.21 after_54.22_54.22)) (?v_44 (= EC_88.1_0_102.5_0_111.21_111.21 ecReturn))) (let ((?v_64 (=> ?v_44 (not (= RES_88.1_0_102.5_0_111.21_111.21 null)))) (?v_45 (= RES_88.1_0_97.24_97.24 RES_88.1_0_102.5_0_111.21_111.21)) (?v_46 (= EC_88.1_0_102.5_0_113.21_113.21 ecReturn))) (let ((?v_65 (or (and ?v_45 ?v_27 (= Smt.true (is RES_88.1_0_102.5_0_113.21_113.21 T_boolean)) ?v_46 (=> (and ?v_46 ?v_47) (not (= Smt.true RES_88.1_0_102.5_0_113.21_113.21))) (= tmp9_cand_88.1_0_102.5_0_113.6 (boolNot RES_88.1_0_102.5_0_113.21_113.21)) (= RES RES_88.1_0_102.5_0_113.21_113.21) (= EC EC_88.1_0_102.5_0_113.21_113.21) (= tmp9_cand_113.13 tmp9_cand_88.1_0_102.5_0_113.6)) (and (not ?v_45) ?v_17 (= RES RES_88.1_0_102.5_0_111.21_111.21) (= EC EC_88.1_0_102.5_0_111.21_111.21) (= tmp9_cand_113.13 (= Smt.true bool_false))))) (?v_110 (not (and ?v_48 (< 0 ?v_30)))) (?v_66 (= Smt.true (is RES_88.1_0_102.5_0_114.24_114.24 T_int))) (?v_49 (= EC_88.1_0_102.5_0_114.24_114.24 ecReturn)) (?v_52 (not (= RES_88.1_0_102.5_0_114.24_114.24 NULL_15.60.26)))) (let ((?v_67 (=> ?v_49 ?v_52)) (?v_68 (= Smt.true (is RES_88.1_0_102.5_0_115.34_115.34 T_java.lang.String))) (?v_69 (isAllocated RES_88.1_0_102.5_0_115.34_115.34 after_54.22_54.22)) (?v_50 (= EC_88.1_0_102.5_0_115.34_115.34 ecReturn))) (let ((?v_70 (=> ?v_50 (not (= RES_88.1_0_102.5_0_115.34_115.34 null)))) (?v_71 (= tmp13_88.1_0_102.5_0_115.3 (stringCat (stringCat S_115.3 RES_88.1_0_102.5_0_115.34_115.34) S_116.9))) (?v_72 (= Smt.true (is RES_88.1_0_102.5_0_116.22_116.22 T_java.lang.String))) (?v_73 (isAllocated RES_88.1_0_102.5_0_116.22_116.22 after_54.22_54.22)) (?v_51 (= EC_88.1_0_102.5_0_116.22_116.22 ecReturn))) (let ((?v_74 (=> ?v_51 (not (= RES_88.1_0_102.5_0_116.22_116.22 null)))) (?v_75 (= msg_114.15_88.1_0_102.5_0_114.15_24.220.45 (stringCat (stringCat (stringCat (stringCat tmp13_88.1_0_102.5_0_115.3 RES_88.1_0_102.5_0_116.22_116.22) S_117.9) RES_88.1_0_97.24_97.24) S_118.9))) (?v_76 (= EC_88.1_0_102.5_0_114.15_114.15 ecReturn)) (?v_80 (not (and ?v_36 ?v_35))) (?v_81 (= C_102.5 C_102.5))) (let ((?v_82 (or (and ?v_18 ?v_56 ?v_57 ?v_34 ?v_58 ?v_36 ?v_35 ?v_17 ?v_36 ?v_37 ?v_59 ?v_39 ?v_60 ?v_40 ?v_61 ?v_39 ?v_43 ?v_62 ?v_63 ?v_44 ?v_64 ?v_65 (or (and tmp9_cand_113.13 ?v_17 ?v_27 ?v_66 ?v_49 ?v_67 ?v_27 ?v_68 ?v_69 ?v_50 ?v_70 ?v_71 ?v_39 ?v_72 ?v_73 ?v_51 ?v_74 ?v_75 ?v_52 ?v_76 (not ?v_76) (= RES_1_ RES_88.1_0_102.5_0_114.15_114.15) (= EC_1_ EC_88.1_0_102.5_0_114.15_114.15)) (and (not tmp9_cand_113.13) ?v_17 (= RES_1_ RES) (= EC_1_ EC))) (= RES_104.21 RES_1_) (= EC_104.21 EC_1_)) (and ?v_18 ?v_56 ?v_57 ?v_34 ?v_58 ?v_80 ?v_17 ?v_17 ?v_81 (= RES_104.21 RES_88.1_0_102.5_0_104.29_104.29) (= EC_104.21 C_102.5)))) (?v_83 (= j_88.1_0_102.5_0_102.43 (+ j_88.1_0_102.10 1))) (?v_84 (= EC_88.1_0_102.5_1_102.35_102.35 ecReturn)) (?v_85 (= EC_3_ L_102.5))) (let ((?v_161 (or (and ?v_17 (or (and ?v_18 ?v_53 ?v_33 ?v_54 (not ?v_55) (= RES_2_ RES_88.1_0_102.5_0_102.35_102.35) (= EC_2_ L_102.5)) (and ?v_18 ?v_53 ?v_33 ?v_54 ?v_55 ?v_18 ?v_56 ?v_57 ?v_34 ?v_58 ?v_80 ?v_17 ?v_17 (not ?v_81) (= RES_2_ RES_88.1_0_102.5_0_104.29_104.29) (= EC_2_ C_102.5))) (= RES_3_ RES_2_) (= EC_3_ EC_2_)) (and ?v_17 ?v_18 ?v_53 ?v_33 ?v_54 ?v_55 ?v_82 ?v_83 ?v_17 ?v_18 (= Smt.true (is RES_88.1_0_102.5_1_102.35_102.35 T_int)) ?v_84 (=> ?v_84 (= RES_88.1_0_102.5_1_102.35_102.35 ?v_21)) (not (< j_88.1_0_102.5_0_102.43 RES_88.1_0_102.5_1_102.35_102.35)) (= RES_3_ RES_88.1_0_102.5_1_102.35_102.35) ?v_85))) (?v_162 (= RES_4_ RES_3_)) (?v_163 (= EC_4_ EC_3_)) (?v_164 (= 0 j_loopold_88.1_0_126.14)) (?v_165 (= EC_4_ EC_loopold_88.1_0_1_)) (?v_86 (not (= elems_77.1 null)))) (let ((?v_88 (not ?v_86)) (?v_117 (= Smt.true (is RES_88.1_0_126.5_0_126.27_126.27 T_int))) (?v_87 (= EC_88.1_0_126.5_0_126.27_126.27 ecReturn)) (?v_89 (select1 count_25.67.33 elems_77.1))) (let ((?v_118 (=> ?v_87 (= RES_88.1_0_126.5_0_126.27_126.27 ?v_89))) (?v_119 (< 0 RES_88.1_0_126.5_0_126.27_126.27)) (?v_113 (not (and ?v_48 (< 0 ?v_89)))) (?v_120 (= Smt.true (is RES_88.1_0_126.5_0_127.18_127.18 T_javafe.ast.TypeDecl))) (?v_121 (isAllocated RES_88.1_0_126.5_0_127.18_127.18 after_54.22_54.22)) (?v_90 (= EC_88.1_0_126.5_0_127.18_127.18 ecReturn)) (?v_91 (not (= RES_88.1_0_126.5_0_127.18_127.18 null)))) (let ((?v_122 (=> ?v_90 ?v_91)) (?v_140 (not (= RES_88.1_0_97.24_97.24 (select1 id_26.32.34 RES_88.1_0_126.5_0_127.18_127.18))))) (let ((?v_123 (not ?v_140)) (?v_108 (select1 pkgName_6.21.14 cu_48.60))) (let ((?v_92 (= ?v_108 null))) (let ((?v_99 (not ?v_92)) (?v_100 (= Smt.true (is RES_88.1_0_126.5_0_135.13_135.13 T_int))) (?v_93 (= EC_88.1_0_126.5_0_135.13_135.13 ecReturn))) (let ((?v_101 (=> ?v_93 (= RES_88.1_0_126.5_0_135.13_135.13 ?v_30))) (?v_102 (> RES_88.1_0_126.5_0_135.13_135.13 1)) (?v_103 (= Smt.true (is RES_88.1_0_126.5_0_136.17_136.17 T_int))) (?v_94 (= EC_88.1_0_126.5_0_136.17_136.17 ecReturn))) (let ((?v_104 (=> ?v_94 (= RES_88.1_0_126.5_0_136.17_136.17 ?v_30))) (?v_95 (= len_136.7_88.1_0_126.5_0_136.7_22.171.36 (- RES_88.1_0_126.5_0_136.17_136.17 1))) (?v_105 (= Smt.true (is RES_88.1_0_126.5_0_136.7_136.7 T_javafe.ast.Name))) (?v_106 (isAllocated RES_88.1_0_126.5_0_136.7_136.7 after_54.22_54.22)) (?v_96 (= EC_88.1_0_126.5_0_136.7_136.7 ecReturn)) (?v_97 (not (= RES_88.1_0_126.5_0_136.7_136.7 null)))) (let ((?v_107 (=> ?v_96 ?v_97)) (?v_141 (= Smt.true (is RES_88.1_0_126.5_0_132.13_132.13 T_int))) (?v_98 (= EC_88.1_0_126.5_0_132.13_132.13 ecReturn))) (let ((?v_142 (=> ?v_98 (= RES_88.1_0_126.5_0_132.13_132.13 ?v_30))) (?v_143 (= RES_88.1_0_126.5_0_132.13_132.13 1)) (?v_109 (= EC_88.1_0_126.5_0_136.27_136.27 ecReturn))) (let ((?v_144 (or (and ?v_102 ?v_27 ?v_103 ?v_94 ?v_104 ?v_27 ?v_95 ?v_105 ?v_106 ?v_96 ?v_107 ?v_7 ?v_97 (= other_136.27_88.1_0_126.5_0_136.27_22.42.42 ?v_108) (= Smt.true (is RES_88.1_0_126.5_0_136.27_136.27 T_boolean)) ?v_109 (=> (and ?v_109 (= other_136.27_88.1_0_126.5_0_136.27_22.42.42 null)) (not (= Smt.true RES_88.1_0_126.5_0_136.27_136.27))) (= RES_6_ RES_88.1_0_126.5_0_136.27_136.27) (= tmp17_cand_135.22 RES_88.1_0_126.5_0_136.27_136.27) (= EC_6_ EC_88.1_0_126.5_0_136.27_136.27)) (and (not ?v_102) ?v_17 (= RES_6_ RES_88.1_0_126.5_0_135.13_135.13) (= tmp17_cand_135.22 bool_false) (= EC_6_ EC_88.1_0_126.5_0_135.13_135.13)))) (?v_145 (= Smt.true tmp17_cand_135.22))) (let ((?v_124 (or (and ?v_92 ?v_17 ?v_27 ?v_141 ?v_98 ?v_142 (not ?v_143) ?v_17 (= RES_5_ RES_88.1_0_126.5_0_132.13_132.13) (= EC_5_ EC_88.1_0_126.5_0_132.13_132.13)) (and ?v_99 ?v_17 ?v_27 ?v_100 ?v_93 ?v_101 ?v_144 (not ?v_145) ?v_17 (= RES_5_ RES_6_) (= EC_5_ EC_6_)))) (?v_125 (= Smt.true (is RES_88.1_0_126.5_0_140.27_140.27 T_int))) (?v_111 (= EC_88.1_0_126.5_0_140.27_140.27 ecReturn)) (?v_116 (not (= RES_88.1_0_126.5_0_140.27_140.27 NULL_15.60.26)))) (let ((?v_126 (=> ?v_111 ?v_116)) (?v_127 (= Smt.true (is RES_88.1_0_126.5_0_141.6_141.6 T_java.lang.String))) (?v_128 (isAllocated RES_88.1_0_126.5_0_141.6_141.6 after_54.22_54.22)) (?v_112 (= EC_88.1_0_126.5_0_141.6_141.6 ecReturn))) (let ((?v_129 (=> ?v_112 (not (= RES_88.1_0_126.5_0_141.6_141.6 null)))) (?v_130 (= tmp22_88.1_0_126.5_0_141.3 (stringCat (stringCat (stringCat RES_88.1_0_126.5_0_141.6_141.6 S_142.5) RES_88.1_0_97.24_97.24) S_143.10))) (?v_131 (= Smt.true (is RES_88.1_0_126.5_0_144.29_144.29 T_javafe.ast.TypeDecl))) (?v_132 (isAllocated RES_88.1_0_126.5_0_144.29_144.29 after_54.22_54.22)) (?v_114 (= EC_88.1_0_126.5_0_144.29_144.29 ecReturn)) (?v_115 (not (= RES_88.1_0_126.5_0_144.29_144.29 null)))) (let ((?v_133 (=> ?v_114 ?v_115)) (?v_134 (= loc_144.14_88.1_0_126.5_0_144.14_15.152.36 (select1 loc_26.45.13 RES_88.1_0_126.5_0_144.29_144.29))) (?v_135 (= Smt.true (is RES_88.1_0_126.5_0_144.14_144.14 T_java.lang.String))) (?v_136 (isAllocated RES_88.1_0_126.5_0_144.14_144.14 after_54.22_54.22)) (?v_137 (= EC_88.1_0_126.5_0_144.14_144.14 ecReturn)) (?v_138 (= msg_140.18_88.1_0_126.5_0_140.18_24.220.45 (stringCat tmp22_88.1_0_126.5_0_141.3 RES_88.1_0_126.5_0_144.14_144.14))) (?v_139 (= EC_88.1_0_126.5_0_140.18_140.18 ecReturn)) (?v_147 (= EC_127.12_1_ C_126.5)) (?v_146 (= EC_7_ C_126.5))) (let ((?v_166 (or (and ?v_140 ?v_17 ?v_17 (= RES_127.12_1_ RES_88.1_0_126.5_0_127.18_127.18) ?v_147) (and ?v_123 ?v_17 ?v_7 (or (and ?v_92 ?v_17 ?v_27 ?v_141 ?v_98 ?v_142 ?v_143 ?v_17 ?v_17 (= RES_7_ RES_88.1_0_126.5_0_132.13_132.13) ?v_146) (and ?v_99 ?v_17 ?v_27 ?v_100 ?v_93 ?v_101 ?v_144 ?v_145 ?v_17 ?v_17 (= RES_7_ RES_6_) ?v_146)) (= RES_127.12_1_ RES_7_) (= EC_127.12_1_ EC_7_))))) (let ((?v_167 (or (and ?v_86 ?v_120 ?v_121 ?v_90 ?v_122 ?v_91 ?v_123 ?v_17 ?v_7 ?v_124 ?v_27 ?v_125 ?v_111 ?v_126 ?v_27 ?v_127 ?v_128 ?v_112 ?v_129 ?v_130 ?v_86 ?v_131 ?v_132 ?v_114 ?v_133 ?v_115 ?v_134 ?v_135 ?v_136 ?v_137 ?v_138 ?v_116 ?v_139 (not ?v_139) (= RES_127.12 RES_88.1_0_126.5_0_140.18_140.18) (= EC_127.12 EC_88.1_0_126.5_0_140.18_140.18)) (and ?v_86 ?v_120 ?v_121 ?v_90 ?v_122 ?v_91 ?v_166 ?v_147 (= RES_127.12 RES_127.12_1_) (= EC_127.12 EC_127.12_1_)))) (?v_168 (= j_88.1_0_126.5_0_126.35 ?v_148)) (?v_169 (= EC_88.1_0_126.5_1_126.27_126.27 ecReturn)) (?v_170 (= EC_9_ L_126.5))) (let ((?v_171 (or (and ?v_17 (or (and ?v_86 ?v_117 ?v_87 ?v_118 (not ?v_119) (= RES_8_ RES_88.1_0_126.5_0_126.27_126.27) (= EC_8_ L_126.5)) (and ?v_86 ?v_117 ?v_87 ?v_118 ?v_119 ?v_86 ?v_120 ?v_121 ?v_90 ?v_122 ?v_91 ?v_166 (not ?v_147) (= RES_8_ RES_127.12_1_) (= EC_8_ EC_127.12_1_))) (= RES_9_ RES_8_) (= EC_9_ EC_8_)) (and ?v_17 ?v_86 ?v_117 ?v_87 ?v_118 ?v_119 ?v_167 ?v_168 ?v_17 ?v_86 (= Smt.true (is RES_88.1_0_126.5_1_126.27_126.27 T_int)) ?v_169 (=> ?v_169 (= RES_88.1_0_126.5_1_126.27_126.27 ?v_89)) (not (< j_88.1_0_126.5_0_126.35 RES_88.1_0_126.5_1_126.27_126.27)) (= RES_9_ RES_88.1_0_126.5_1_126.27_126.27) ?v_170))) (?v_172 (= EC_90.24_1_ C_88.1))) (let ((?v_197 (or (and (not (and ?v_24 ?v_23)) ?v_17 ?v_17 (= RES_90.24_1_ RES_88.1_0_90.32_90.32) ?v_172) (and ?v_24 ?v_23 ?v_17 ?v_24 ?v_25 ?v_155 ?v_27 ?v_156 ?v_28 ?v_157 ?v_27 ?v_31 ?v_158 ?v_159 ?v_32 ?v_160 (or (and ?v_77 ?v_78 ?v_79 ?v_161 (not ?v_85) (= RES_90.24_1_ RES_3_) (= EC_90.24_1_ EC_3_)) (and ?v_77 ?v_78 ?v_79 ?v_161 ?v_85 ?v_162 ?v_163 ?v_164 ?v_165 ?v_171 (not ?v_170) (= RES_90.24_1_ RES_9_) (= EC_90.24_1_ EC_9_))))))) (let ((?v_198 (or (and ?v_18 ?v_152 ?v_153 ?v_22 ?v_154 ?v_24 ?v_23 ?v_17 ?v_24 ?v_25 ?v_155 ?v_27 ?v_156 ?v_28 ?v_157 ?v_27 ?v_31 ?v_158 ?v_159 ?v_32 ?v_160 ?v_77 ?v_78 ?v_79 ?v_161 ?v_85 ?v_162 ?v_163 ?v_164 ?v_165 ?v_171 ?v_170 (= RES_10_ RES_9_) (= EC_10_ EC_9_) (= RES_90.24 RES_10_) (= EC_90.24 EC_10_)) (and ?v_18 ?v_152 ?v_153 ?v_22 ?v_154 ?v_197 ?v_172 (= RES_90.24 RES_90.24_1_) (= EC_90.24 EC_90.24_1_)))) (?v_199 (= i_88.1_0_88.37 ?v_148)) (?v_200 (= EC_88.1_1_88.29_88.29 ecReturn)) (?v_201 (= EC_12_ L_88.1))) (let ((?v_203 (or (and ?v_17 (or (and ?v_18 ?v_149 ?v_19 ?v_150 (not ?v_151) (= RES_11_ RES_88.1_0_88.29_88.29) (= EC_11_ L_88.1)) (and ?v_18 ?v_149 ?v_19 ?v_150 ?v_151 ?v_18 ?v_152 ?v_153 ?v_22 ?v_154 ?v_197 (not ?v_172) (= RES_11_ RES_90.24_1_) (= EC_11_ EC_90.24_1_))) (= EC_12_ EC_11_)) (and ?v_17 ?v_18 ?v_149 ?v_19 ?v_150 ?v_151 ?v_198 ?v_199 ?v_17 ?v_18 (= Smt.true (is RES_88.1_1_88.29_88.29 T_int)) ?v_200 (=> ?v_200 (= RES_88.1_1_88.29_88.29 ?v_21)) (not (< i_88.1_0_88.37 RES_88.1_1_88.29_88.29)) ?v_201))) (?v_204 (= EC_52.5 ecReturn))) (not (=> (and (distinct C_126.5 C_102.5 ecReturn C_88.1 L_126.5 L_102.5 L_88.1) (not (= S_118.9 null)) (= (typeof S_118.9) T_java.lang.String) (not (= S_57.35 null)) (= (typeof S_57.35) T_java.lang.String) (not (= S_117.9 null)) (= (typeof S_117.9) T_java.lang.String) (not (= S_143.10 null)) (= (typeof S_143.10) T_java.lang.String) (not (= S_56.10 null)) (= (typeof S_56.10) T_java.lang.String) (not (= S_142.5 null)) (= (typeof S_142.5) T_java.lang.String) (not (= S_116.9 null)) (= (typeof S_116.9) T_java.lang.String) (not (= S_115.3 null)) (= (typeof S_115.3) T_java.lang.String)) (=> (and (= NULL_pre_56.82.26 NULL_56.82.26) (= Smt.true (is NULL_56.82.26 T_int)) (= name_pre_20.18.28 name_20.18.28) (= name_20.18.28 (asField name_20.18.28 T_javafe.ast.Name)) (< (fClosedTime name_20.18.28) alloc) (forall ((?s Int)) (=> (not (= ?s null)) (not (= (select1 name_20.18.28 ?s) null)))) (= loc_pre_18.18.13 loc_18.18.13) (= loc_18.18.13 (asField loc_18.18.13 T_int)) (= TYPEMODIFIERPRAGMA_pre_56.28.26 TYPEMODIFIERPRAGMA_56.28.26) (= Smt.true (is TYPEMODIFIERPRAGMA_56.28.26 T_int)) (= locId_pre_86.38.13 locId_86.38.13) (= locId_86.38.13 (asField locId_86.38.13 T_int)) (= locId_pre_88.43.13 locId_88.43.13) (= locId_88.43.13 (asField locId_88.43.13 T_int)) (= pkgName_pre_6.21.14 pkgName_6.21.14) (= pkgName_6.21.14 (asField pkgName_6.21.14 T_javafe.ast.Name)) (< (fClosedTime pkgName_6.21.14) alloc) (= STRINGLIT_pre_57.44.26 STRINGLIT_57.44.26) (= Smt.true (is STRINGLIT_57.44.26 T_int)) (= IDENT_pre_57.25.26 IDENT_57.25.26) (= Smt.true (is IDENT_57.25.26 T_int)) (= imports_pre_6.25.37 imports_6.25.37) (= imports_6.25.37 (asField imports_6.25.37 T_javafe.ast.ImportDeclVec)) (< (fClosedTime imports_6.25.37) alloc) (forall ((?s_1_ Int)) (=> (not (= ?s_1_ null)) (not (= (select1 imports_6.25.37 ?s_1_) null)))) (= elements_pre_83.61.39 elements_83.61.39) (= elements_83.61.39 (asField elements_83.61.39 (array T_javafe.ast.MethodDecl))) (< (fClosedTime elements_83.61.39) alloc) (forall ((?s_2_ Int)) (=> (not (= ?s_2_ null)) (not (= (select1 elements_83.61.39 ?s_2_) null)))) (= count_pre_17.67.33 count_17.67.33) (= count_17.67.33 (asField count_17.67.33 T_int)) (= otherCodes_pre_56.202.27 otherCodes_56.202.27) (= Smt.true (is otherCodes_56.202.27 ?v_0)) (isAllocated otherCodes_56.202.27 alloc) (= LAST_KEYWORD_pre_56.103.26 LAST_KEYWORD_56.103.26) (= Smt.true (is LAST_KEYWORD_56.103.26 T_int)) (= locType_pre_87.21.13 locType_87.21.13) (= locType_87.21.13 (asField locType_87.21.13 T_int)) (= punctuationStrings_pre_56.134.22 punctuationStrings_56.134.22) (= Smt.true (is punctuationStrings_56.134.22 ?v_1)) (isAllocated punctuationStrings_56.134.22 alloc) (= punctuationCodes_pre_56.164.19 punctuationCodes_56.164.19) (= Smt.true (is punctuationCodes_56.164.19 ?v_0)) (isAllocated punctuationCodes_56.164.19 alloc) (= loc_pre_26.45.13 loc_26.45.13) (= loc_26.45.13 (asField loc_26.45.13 T_int)) (= whereDecoration_pre_35.597.41 whereDecoration_35.597.41) (= Smt.true (is whereDecoration_35.597.41 T_javafe.ast.ASTDecoration)) (isAllocated whereDecoration_35.597.41 alloc) (= noTokens_pre_56.212.27 noTokens_56.212.27) (= Smt.true (is noTokens_56.212.27 T_int)) (= LEXICALPRAGMA_pre_56.24.26 LEXICALPRAGMA_56.24.26) (= Smt.true (is LEXICALPRAGMA_56.24.26 T_int)) (= syntax_pre_21.28.29 syntax_21.28.29) (= syntax_21.28.29 (asField syntax_21.28.29 T_boolean)) (= locOpenBrace_pre_97.22.13 locOpenBrace_97.22.13) (= locOpenBrace_97.22.13 (asField locOpenBrace_97.22.13 T_int)) (= LONGLIT_pre_57.40.26 LONGLIT_57.40.26) (= Smt.true (is LONGLIT_57.40.26 T_int)) (= tokenType_pre_23.90.8 tokenType_23.90.8) (= tokenType_23.90.8 (asField tokenType_23.90.8 T_int)) (= sigDecoration_pre_33.104.38 sigDecoration_33.104.38) (= Smt.true (is sigDecoration_33.104.38 T_javafe.ast.ASTDecoration)) (isAllocated sigDecoration_33.104.38 alloc) (= locId_pre_26.48.13 locId_26.48.13) (= locId_26.48.13 (asField locId_26.48.13 T_int)) (= locOpenBrace_pre_26.51.13 locOpenBrace_26.51.13) (= locOpenBrace_26.51.13 (asField locOpenBrace_26.51.13 T_int)) (= elements_pre_82.61.38 elements_82.61.38) (= elements_82.61.38 (asField elements_82.61.38 (array T_javafe.ast.FieldDecl))) (< (fClosedTime elements_82.61.38) alloc) (forall ((?s_3_ Int)) (=> (not (= ?s_3_ null)) (not (= (select1 elements_82.61.38 ?s_3_) null)))) (= locCloseBrace_pre_26.54.13 locCloseBrace_26.54.13) (= locCloseBrace_26.54.13 (asField locCloseBrace_26.54.13 T_int)) (= TYPEDECLELEMPRAGMA_pre_56.27.26 TYPEDECLELEMPRAGMA_56.27.26) (= Smt.true (is TYPEDECLELEMPRAGMA_56.27.26 T_int)) (= locCloseBrace_pre_97.25.13 locCloseBrace_97.25.13) (= locCloseBrace_97.25.13 (asField locCloseBrace_97.25.13 T_int)) (= NULL_pre_15.60.26 NULL_15.60.26) (= Smt.true (is NULL_15.60.26 T_int)) (= DOUBLELIT_pre_57.43.26 DOUBLELIT_57.43.26) (= Smt.true (is DOUBLELIT_57.43.26 T_int)) (= typeName_pre_19.15.32 typeName_19.15.32) (= typeName_19.15.32 (asField typeName_19.15.32 T_javafe.ast.TypeName)) (< (fClosedTime typeName_19.15.32) alloc) (forall ((?s_4_ Int)) (=> (not (= ?s_4_ null)) (not (= (select1 typeName_19.15.32 ?s_4_) null)))) (= FIRST_KEYWORD_pre_56.51.26 FIRST_KEYWORD_56.51.26) (= Smt.true (is FIRST_KEYWORD_56.51.26 T_int)) (= count_pre_25.67.33 count_25.67.33) (= count_25.67.33 (asField count_25.67.33 T_int)) (= length_pre_22.50.25 length_22.50.25) (= length_22.50.25 (asField length_22.50.25 T_int)) (= loc_pre_6.30.13 loc_6.30.13) (= loc_6.30.13 (asField loc_6.30.13 T_int)) (= elems_pre_6.27.35 elems_6.27.35) (= elems_6.27.35 (asField elems_6.27.35 T_javafe.ast.TypeDeclVec)) (< (fClosedTime elems_6.27.35) alloc) (forall ((?s_5_ Int)) (=> (not (= ?s_5_ null)) (not (= (select1 elems_6.27.35 ?s_5_) null)))) (= INTLIT_pre_57.39.26 INTLIT_57.39.26) (= Smt.true (is INTLIT_57.39.26 T_int)) (= STMTPRAGMA_pre_56.26.26 STMTPRAGMA_56.26.26) (= Smt.true (is STMTPRAGMA_56.26.26 T_int)) (= returnType_pre_87.18.28 returnType_87.18.28) (= returnType_87.18.28 (asField returnType_87.18.28 T_javafe.ast.Type)) (< (fClosedTime returnType_87.18.28) alloc) (forall ((?s_6_ Int)) (=> (not (= ?s_6_ null)) (not (= (select1 returnType_87.18.28 ?s_6_) null)))) (= keywordStrings_pre_56.181.30 keywordStrings_56.181.30) (= Smt.true (is keywordStrings_56.181.30 ?v_1)) (isAllocated keywordStrings_56.181.30 alloc) (= elements_pre_17.61.39 elements_17.61.39) (= elements_17.61.39 (asField elements_17.61.39 (array T_javafe.ast.ImportDecl))) (< (fClosedTime elements_17.61.39) alloc) (forall ((?s_7_ Int)) (=> (not (= ?s_7_ null)) (not (= (select1 elements_17.61.39 ?s_7_) null)))) (= FLOATLIT_pre_57.42.26 FLOATLIT_57.42.26) (= Smt.true (is FLOATLIT_57.42.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) (= count_pre_83.67.33 count_83.67.33) (= count_83.67.33 (asField count_83.67.33 T_int)) (= typeEnv_pre_35.323.32 typeEnv_35.323.32) (= Smt.true (is typeEnv_35.323.32 T_javafe.ast.ASTDecoration)) (isAllocated typeEnv_35.323.32 alloc) (= checkedField_pre_30.33 checkedField_30.33) (= Smt.true (is checkedField_30.33 T_javafe.ast.ASTDecoration)) (isAllocated checkedField_30.33 alloc) (= locOpenBrace_pre_88.36.13 locOpenBrace_88.36.13) (= locOpenBrace_88.36.13 (asField locOpenBrace_88.36.13 T_int)) (= BOOLEANLIT_pre_57.38.26 BOOLEANLIT_57.38.26) (= Smt.true (is BOOLEANLIT_57.38.26 T_int)) (= inst_pre_36.29.44 inst_36.29.44) (= Smt.true (is inst_36.29.44 T_javafe.ast.PrettyPrint)) (isAllocated inst_36.29.44 alloc) (not (= inst_36.29.44 null)) (= elements_pre_25.61.37 elements_25.61.37) (= elements_25.61.37 (asField elements_25.61.37 (array T_javafe.ast.TypeDecl))) (< (fClosedTime elements_25.61.37) alloc) (forall ((?s_8_ Int)) (=> (not (= ?s_8_ null)) (not (= (select1 elements_25.61.37 ?s_8_) null)))) (= body_pre_88.34.19 body_88.34.19) (= body_88.34.19 (asField body_88.34.19 T_javafe.ast.BlockStmt)) (< (fClosedTime body_88.34.19) alloc) (= modifiers_pre_26.28.13 modifiers_26.28.13) (= modifiers_26.28.13 (asField modifiers_26.28.13 T_int)) (= count_pre_82.67.33 count_82.67.33) (= count_82.67.33 (asField count_82.67.33 T_int)) (= id_pre_26.32.34 id_26.32.34) (= id_26.32.34 (asField id_26.32.34 T_javafe.ast.Identifier)) (< (fClosedTime id_26.32.34) alloc) (forall ((?s_9_ Int)) (=> (not (= ?s_9_ null)) (not (= (select1 id_26.32.34 ?s_9_) null)))) (= otherStrings_pre_56.193.30 otherStrings_56.193.30) (= Smt.true (is otherStrings_56.193.30 ?v_1)) (isAllocated otherStrings_56.193.30 alloc) (= MODIFIERPRAGMA_pre_56.25.26 MODIFIERPRAGMA_56.25.26) (= Smt.true (is MODIFIERPRAGMA_56.25.26 T_int)) (= decorationType_pre_5.48.27 decorationType_5.48.27) (= decorationType_5.48.27 (asField decorationType_5.48.27 T_.TYPE)) (= type_pre_86.35.28 type_86.35.28) (= type_86.35.28 (asField type_86.35.28 T_javafe.ast.Type)) (< (fClosedTime type_86.35.28) alloc) (forall ((?s_10_ Int)) (=> (not (= ?s_10_ null)) (not (= (select1 type_86.35.28 ?s_10_) null)))) (= loc_pre_88.40.13 loc_88.40.13) (= loc_88.40.13 (asField loc_88.40.13 T_int)) (= CHARLIT_pre_57.41.26 CHARLIT_57.41.26) (= Smt.true (is CHARLIT_57.41.26 T_int)) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= Smt.true (is cu_48.60 T_javafe.ast.CompilationUnit)) (isAllocated cu_48.60 alloc) ?v_7 (forall ((?i_56.147.29 Int)) (=> (and (<= 0 ?i_56.147.29) (<= ?i_56.147.29 (arrayLength punctuationCodes_56.164.19))) (not (= (select1 (select1 elems punctuationCodes_56.164.19) ?i_56.147.29) NULL_56.82.26)))) (forall ((?brokenObj Int)) (=> (and (= Smt.true (is ?brokenObj T_javafe.ast.TypeDeclVec)) (not (= ?brokenObj null))) (= (typeof (select1 elements_25.61.37 ?brokenObj)) (array T_javafe.ast.TypeDecl)))) (forall ((?brokenObj_1_ Int)) (=> (and (= Smt.true (is ?brokenObj_1_ T_javafe.ast.ImportDeclVec)) (not (= ?brokenObj_1_ null))) (= (select1 owner_4.35.28 (select1 elements_17.61.39 ?brokenObj_1_)) ?brokenObj_1_))) (= Smt.true (is ?v_2 T_javafe.parser.TagConstants)) (not (= ?v_2 null)) (= (arrayLength punctuationCodes_56.164.19) ?v_4) (forall ((?brokenObj_2_ Int)) (=> (and (= Smt.true (is ?brokenObj_2_ T_javafe.ast.ImportDeclVec)) (not (= ?brokenObj_2_ null))) (forall ((?i_17.62.31 Int)) (=> (and (<= 0 ?i_17.62.31) (< ?i_17.62.31 (select1 count_17.67.33 ?brokenObj_2_))) (not (= (select1 (select1 elems (select1 elements_17.61.39 ?brokenObj_2_)) ?i_17.62.31) null)))))) (= ?v_9 T_java.lang.Boolean) (= ?v_3 (- (+ 1 LAST_KEYWORD_56.103.26) FIRST_KEYWORD_56.51.26)) (forall ((?brokenObj_3_ Int)) (=> (and (= Smt.true (is ?brokenObj_3_ T_javafe.ast.CompilationUnit)) (not (= ?brokenObj_3_ null))) (not (= (select1 loc_6.30.13 ?brokenObj_3_) NULL_15.60.26)))) (forall ((?brokenObj_4_ Int)) (let ((?v_205 (select1 tokenType_23.90.8 ?brokenObj_4_))) (=> (and (= Smt.true (is ?brokenObj_4_ T_javafe.ast.Identifier)) (not (= ?brokenObj_4_ null))) (and (not (= ?v_205 BOOLEANLIT_57.38.26)) (not (= ?v_205 INTLIT_57.39.26)) (not (= ?v_205 LONGLIT_57.40.26)) (not (= ?v_205 FLOATLIT_57.42.26)) (not (= ?v_205 DOUBLELIT_57.43.26)) (not (= ?v_205 STRINGLIT_57.44.26)) (not (= ?v_205 CHARLIT_57.41.26)) (not (= ?v_205 LEXICALPRAGMA_56.24.26)) (not (= ?v_205 MODIFIERPRAGMA_56.25.26)) (not (= ?v_205 STMTPRAGMA_56.26.26)) (not (= ?v_205 TYPEDECLELEMPRAGMA_56.27.26)) (not (= ?v_205 TYPEMODIFIERPRAGMA_56.28.26)))))) (nonnullelements otherStrings_56.193.30 elems) ?v_6 (forall ((?brokenObj_5_ Int)) (=> (and (= Smt.true (is ?brokenObj_5_ T_javafe.ast.TypeDeclVec)) (not (= ?brokenObj_5_ null))) (<= 0 (select1 count_25.67.33 ?brokenObj_5_)))) (forall ((?brokenObj_6_ Int)) (=> (and (= Smt.true (is ?brokenObj_6_ T_javafe.ast.ImportDeclVec)) (not (= ?brokenObj_6_ null))) (<= (select1 count_17.67.33 ?brokenObj_6_) (arrayLength (select1 elements_17.61.39 ?brokenObj_6_))))) (= (arrayLength otherCodes_56.202.27) ?v_5) (forall ((?brokenObj_7_ Int)) (=> (and (= Smt.true (is ?brokenObj_7_ T_javafe.ast.ImportDeclVec)) (not (= ?brokenObj_7_ null))) (= (typeof (select1 elements_17.61.39 ?brokenObj_7_)) (array T_javafe.ast.ImportDecl)))) (forall ((?i_56.149.29 Int)) (let ((?v_206 (select1 (select1 elems punctuationCodes_56.164.19) ?i_56.149.29))) (=> (and (<= 0 ?i_56.149.29) (<= ?i_56.149.29 (arrayLength punctuationCodes_56.164.19))) (and (not (= ?v_206 IDENT_57.25.26)) (not (= ?v_206 BOOLEANLIT_57.38.26)) (not (= ?v_206 INTLIT_57.39.26)) (not (= ?v_206 LONGLIT_57.40.26)) (not (= ?v_206 FLOATLIT_57.42.26)) (not (= ?v_206 DOUBLELIT_57.43.26)) (not (= ?v_206 STRINGLIT_57.44.26)) (not (= ?v_206 CHARLIT_57.41.26)) (not (= ?v_206 LEXICALPRAGMA_56.24.26)) (not (= ?v_206 MODIFIERPRAGMA_56.25.26)) (not (= ?v_206 STMTPRAGMA_56.26.26)) (not (= ?v_206 TYPEDECLELEMPRAGMA_56.27.26)) (not (= ?v_206 TYPEMODIFIERPRAGMA_56.28.26)))))) (forall ((?brokenObj_8_ Int)) (=> (and (= Smt.true (is ?brokenObj_8_ T_javafe.ast.TypeDeclVec)) (not (= ?brokenObj_8_ null))) (= (select1 owner_4.35.28 (select1 elements_25.61.37 ?brokenObj_8_)) ?brokenObj_8_))) (forall ((?brokenObj_9_ Int)) (=> (and (= Smt.true (is ?brokenObj_9_ T_javafe.ast.ImportDecl)) (not (= ?brokenObj_9_ null))) (not (= (select1 loc_18.18.13 ?brokenObj_9_) NULL_15.60.26)))) (forall ((?brokenObj_10_ Int)) (=> (and (= Smt.true (is ?brokenObj_10_ T_javafe.ast.Name)) (not (= ?brokenObj_10_ null))) (>= (select1 length_22.50.25 ?brokenObj_10_) 1))) (forall ((?brokenObj_11_ Int)) (=> (and (= Smt.true (is ?brokenObj_11_ T_javafe.ast.TypeDeclVec)) (not (= ?brokenObj_11_ null))) (forall ((?i_25.62.31 Int)) (=> (and (<= 0 ?i_25.62.31) (< ?i_25.62.31 (select1 count_25.67.33 ?brokenObj_11_))) (not (= (select1 (select1 elems (select1 elements_25.61.37 ?brokenObj_11_)) ?i_25.62.31) null)))))) (forall ((?brokenObj_12_ Int)) (=> (and (= Smt.true (is ?brokenObj_12_ T_javafe.ast.TypeDecl)) (not (= ?brokenObj_12_ null))) (not (= (select1 loc_26.45.13 ?brokenObj_12_) NULL_15.60.26)))) (nonnullelements punctuationStrings_56.134.22 elems) (forall ((?brokenObj_13_ Int)) (=> (and (= Smt.true (is ?brokenObj_13_ T_javafe.ast.ImportDeclVec)) (not (= ?brokenObj_13_ null))) (<= 0 (select1 count_17.67.33 ?brokenObj_13_)))) (forall ((?brokenObj_14_ Int)) (=> (and (= Smt.true (is ?brokenObj_14_ T_javafe.ast.TypeDeclVec)) (not (= ?brokenObj_14_ null))) (<= (select1 count_25.67.33 ?brokenObj_14_) (arrayLength (select1 elements_25.61.37 ?brokenObj_14_))))) (nonnullelements keywordStrings_56.181.30 elems) (= noTokens_56.212.27 (+ (+ ?v_3 ?v_4) ?v_5)) (forall ((?brokenObj_15_ Int)) (=> (and (= Smt.true (is ?brokenObj_15_ T_javafe.ast.TypeDecl)) (not (= ?brokenObj_15_ null))) (not (= (select1 locCloseBrace_26.54.13 ?brokenObj_15_) NULL_15.60.26)))) (forall ((?brokenObj_16_ Int)) (=> (and (= Smt.true (is ?brokenObj_16_ T_javafe.ast.TypeDecl)) (not (= ?brokenObj_16_ null))) (not (= (select1 locId_26.48.13 ?brokenObj_16_) NULL_15.60.26)))) (forall ((?brokenObj_17_ Int)) (=> (and (= Smt.true (is ?brokenObj_17_ T_javafe.ast.TypeDecl)) (not (= ?brokenObj_17_ null))) (not (= (select1 locOpenBrace_26.51.13 ?brokenObj_17_) NULL_15.60.26)))) (or ?v_10 (and ?v_6 (or ?v_11 (and ?v_7 ?v_173 ?v_174 ?v_8 ?v_175 ?v_176 ?v_17 ?v_177 ?v_178 ?v_179 ?v_180 ?v_181 ?v_182 ?v_183 ?v_184 (or ?v_10 (and ?v_6 (or ?v_11 (and ?v_7 (not ?v_13)) (and ?v_7 ?v_13 ?v_185 (or ?v_11 (and ?v_7 (or (and ?v_14 (not ?v_15)) (and ?v_14 ?v_15 ?v_186 ?v_187 ?v_16 ?v_188 ?v_189 ?v_190 (or ?v_11 (and ?v_7 ?v_191 (or ?v_11 (and ?v_7 ?v_192 (or ?v_11 (and ?v_7 ?v_193 (or ?v_11 (and ?v_7 ?v_194 ?v_195 ?v_196 (or (and ?v_17 (or ?v_20 (and ?v_18 ?v_149 ?v_19 ?v_150 ?v_151 (or ?v_20 (and ?v_18 (or (not (and ?v_48 (< 0 ?v_21))) (and ?v_152 ?v_153 ?v_22 ?v_154 ?v_24 ?v_23 ?v_17 (or (not ?v_24) (and ?v_24 (or (not ?v_25) (and ?v_25 ?v_155 (or ?v_29 (and ?v_27 ?v_156 ?v_28 ?v_157 (or ?v_29 (and ?v_27 (or (and ?v_31 (not (and (<= 0 i_97.24_88.1_0_97.24_22.62.48) (< i_97.24_88.1_0_97.24_22.62.48 ?v_30)))) (and ?v_31 ?v_158 ?v_159 ?v_32 ?v_160 (or (and ?v_77 ?v_78 ?v_79 (or (and ?v_17 (or ?v_20 (and ?v_18 ?v_53 ?v_33 ?v_54 ?v_55 (or ?v_20 (and ?v_18 (or (not (and (<= 0 j_88.1_0_102.10) (< j_88.1_0_102.10 ?v_21))) (and ?v_56 ?v_57 ?v_34 ?v_58 ?v_36 ?v_35 ?v_17 (or (not ?v_36) (and ?v_36 (or (not ?v_37) (and ?v_37 ?v_59 (or ?v_41 (and ?v_39 ?v_60 ?v_40 ?v_61 (or ?v_41 (and ?v_39 (or (and ?v_43 (not (and (<= 0 i_111.21_88.1_0_102.5_0_111.21_22.62.48) (< i_111.21_88.1_0_102.5_0_111.21_22.62.48 ?v_42)))) (and ?v_43 ?v_62 ?v_63 ?v_44 ?v_64 (or (and ?v_45 ?v_29) (and ?v_65 tmp9_cand_113.13 ?v_17 (or ?v_29 (and ?v_27 (or ?v_110 (and ?v_66 ?v_49 ?v_67 (or ?v_29 (and ?v_27 ?v_68 ?v_69 ?v_50 ?v_70 ?v_71 (or ?v_41 (and ?v_39 ?v_72 ?v_73 ?v_51 ?v_74 ?v_75 (not ?v_52)))))))))))))))))))))))))))) (and ?v_17 ?v_18 ?v_53 ?v_33 ?v_54 ?v_55 ?v_82 ?v_83 ?v_17 ?v_20))) (and ?v_77 ?v_78 ?v_79 ?v_161 ?v_85 ?v_162 ?v_163 ?v_164 ?v_165 (or (and ?v_17 (or ?v_88 (and ?v_86 ?v_117 ?v_87 ?v_118 ?v_119 (or ?v_88 (and ?v_86 (or ?v_113 (and ?v_120 ?v_121 ?v_90 ?v_122 (or (not ?v_91) (and ?v_91 ?v_123 ?v_17 (or ?v_11 (and ?v_7 (or (and ?v_92 ?v_17 ?v_29) (and ?v_99 ?v_17 (or ?v_29 (and ?v_27 ?v_100 ?v_93 ?v_101 ?v_102 (or ?v_29 (and ?v_27 ?v_103 ?v_94 ?v_104 (or ?v_29 (and ?v_27 (or (and ?v_95 (not (and (< 0 len_136.7_88.1_0_126.5_0_136.7_22.171.36) (<= len_136.7_88.1_0_126.5_0_136.7_22.171.36 ?v_30)))) (and ?v_95 ?v_105 ?v_106 ?v_96 ?v_107 (or ?v_11 (and ?v_7 (not ?v_97)))))))))))) (and ?v_124 (or ?v_29 (and ?v_27 (or ?v_110 (and ?v_125 ?v_111 ?v_126 (or ?v_29 (and ?v_27 ?v_127 ?v_128 ?v_112 ?v_129 ?v_130 (or ?v_88 (and ?v_86 (or ?v_113 (and ?v_131 ?v_132 ?v_114 ?v_133 (or (not ?v_115) (and ?v_115 ?v_134 ?v_135 ?v_136 ?v_137 ?v_138 (not ?v_116)))))))))))))))))))))))))) (and ?v_17 ?v_86 ?v_117 ?v_87 ?v_118 ?v_119 ?v_167 ?v_168 ?v_17 ?v_88))))))))))))))))))))) (and ?v_17 ?v_18 ?v_149 ?v_19 ?v_150 ?v_151 ?v_198 ?v_199 ?v_17 ?v_20))))))))))))))))))))) (and (or (and ?v_6 ?v_7 ?v_173 ?v_174 ?v_8 ?v_175 ?v_176 ?v_17 ?v_177 ?v_178 ?v_179 ?v_180 ?v_181 ?v_182 ?v_183 ?v_184 ?v_6 ?v_7 ?v_13 ?v_185 ?v_7 ?v_14 ?v_15 ?v_186 ?v_187 ?v_16 ?v_188 ?v_189 ?v_190 ?v_7 ?v_191 ?v_7 ?v_192 ?v_7 ?v_193 ?v_7 ?v_194 ?v_195 ?v_196 ?v_203 ?v_201 (= EC_13_ EC_12_) ?v_204) (and ?v_6 ?v_7 ?v_173 ?v_174 ?v_8 ?v_175 (or (and ?v_202 ?v_17 ?v_17 (= EC_52.5_1_ ecReturn)) (and ?v_176 ?v_17 ?v_177 ?v_178 ?v_179 ?v_180 ?v_181 ?v_182 ?v_183 ?v_184 ?v_6 ?v_7 ?v_13 ?v_185 ?v_7 ?v_14 ?v_15 ?v_186 ?v_187 ?v_16 ?v_188 ?v_189 ?v_190 ?v_7 ?v_191 ?v_7 ?v_192 ?v_7 ?v_193 ?v_7 ?v_194 ?v_195 ?v_196 ?v_203 (not ?v_201) (= EC_52.5_1_ EC_12_))) (= EC_52.5 EC_52.5_1_))) (not ?v_204)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)