path: root/test/regress/regress1/quantifiers/arith-snorm.smt2

(set-info :smt-lib-version 2.6)
(set-logic UFLIA)
(set-info :source | Simplify Theorem Prover Benchmark Suite |)
(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_tc_FieldDeclVec () Int)
(declare-fun T_javafe_ast_ASTDecoration () Int)
(declare-fun T_javafe_parser_TagConstants () Int)
(declare-fun T_javafe_ast_TagConstants () Int)
(declare-fun T_javafe_ast_Identifier () Int)
(declare-fun T_javafe_tc_MethodDeclVec () Int)
(declare-fun T_java_io_FilterOutputStream () Int)
(declare-fun T_java_io_OutputStream () Int)
(declare-fun T_java_lang_Comparable () Int)
(declare-fun T_java_util_Properties () Int)
(declare-fun T_java_util_Hashtable () Int)
(declare-fun T_javafe_ast_GenericVarDecl () Int)
(declare-fun T_javafe_ast_ASTNode () Int)
(declare-fun T_javafe_ast_Type () Int)
(declare-fun T_java_util_EscjavaKeyValue () Int)
(declare-fun T_javafe_ast_TypeDecl () Int)
(declare-fun T_javafe_ast_TypeDeclElem () Int)
(declare-fun T_javafe_tc_Env () Int)
(declare-fun T_javafe_ast_OperatorTags () Int)
(declare-fun T_javafe_ast_GeneratedTags () Int)
(declare-fun T_javafe_ast_GenericBlockStmt () Int)
(declare-fun T_javafe_ast_Stmt () Int)
(declare-fun T_java_lang_System () Int)
(declare-fun T_javafe_ast_CompilationUnit () Int)
(declare-fun T_java_io_Serializable () Int)
(declare-fun T_javafe_tc_EnvForCU () Int)
(declare-fun T_javafe_ast_RoutineDecl () Int)
(declare-fun T_javafe_util_Location () Int)
(declare-fun T_javafe_tc_EnvForTypeSig () Int)
(declare-fun T_javafe_tc_TypeSig () Int)
(declare-fun T_javafe_ast_MethodDecl () Int)
(declare-fun T_java_util_Map () Int)
(declare-fun T_javafe_ast_BlockStmt () Int)
(declare-fun T_java_util_Dictionary () Int)
(declare-fun T_javafe_ast_FieldDecl () Int)
(declare-fun T_java_io_PrintStream () Int)
(declare-fun DIST_ZERO_1 () Int)
(declare-fun T__TYPE () Int)
(declare-fun keywordStrings_63_181_30 () Int)
(declare-fun STRINGLIT_64_44_26 () Int)
(declare-fun IDENT_64_25_26 () Int)
(declare-fun MODIFIERPRAGMA_63_25_26 () Int)
(declare-fun NULL_63_82_26 () Int)
(declare-fun otherCodes_63_202_27 () Int)
(declare-fun otherStrings_63_193_30 () Int)
(declare-fun LONGLIT_64_40_26 () Int)
(declare-fun noTokens_63_212_27 () Int)
(declare-fun TYPEMODIFIERPRAGMA_63_28_26 () Int)
(declare-fun DOUBLELIT_64_43_26 () Int)
(declare-fun LEXICALPRAGMA_63_24_26 () Int)
(declare-fun out_20_83_49 () Int)
(declare-fun punctuationStrings_63_134_22 () Int)
(declare-fun INTLIT_64_39_26 () Int)
(declare-fun TYPEDECLELEMPRAGMA_63_27_26 () Int)
(declare-fun punctuationCodes_63_164_19 () Int)
(declare-fun FIRST_KEYWORD_63_51_26 () Int)
(declare-fun FLOATLIT_64_42_26 () Int)
(declare-fun PARSED_6_772_28 () Int)
(declare-fun LAST_KEYWORD_63_103_26 () Int)
(declare-fun PREPPED_6_775_28 () Int)
(declare-fun BOOLEANLIT_64_38_26 () Int)
(declare-fun STMTPRAGMA_63_26_26 () Int)
(declare-fun CHARLIT_64_41_26 () Int)
(assert (let ((?v_0 (array T_java_lang_String)) (?v_1 (array T_int))) (and (= (PO_LT T_javafe_tc_FieldDeclVec T_java_lang_Object) true_term) (= T_javafe_tc_FieldDeclVec (asChild T_javafe_tc_FieldDeclVec T_java_lang_Object)) (= (PO_LT T_javafe_ast_ASTDecoration T_java_lang_Object) true_term) (= T_javafe_ast_ASTDecoration (asChild T_javafe_ast_ASTDecoration 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_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_tc_MethodDeclVec T_java_lang_Object) true_term) (= T_javafe_tc_MethodDeclVec (asChild T_javafe_tc_MethodDeclVec T_java_lang_Object)) (= (PO_LT T_java_io_FilterOutputStream T_java_io_OutputStream) true_term) (= T_java_io_FilterOutputStream (asChild T_java_io_FilterOutputStream T_java_io_OutputStream)) (= (PO_LT T_java_lang_Comparable T_java_lang_Object) true_term) (= (PO_LT T_java_util_Properties T_java_util_Hashtable) true_term) (= T_java_util_Properties (asChild T_java_util_Properties T_java_util_Hashtable)) (= (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_Type T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_Type (asChild T_javafe_ast_Type T_javafe_ast_ASTNode)) (= (PO_LT T_java_util_EscjavaKeyValue T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_TypeDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_TypeDecl (asChild T_javafe_ast_TypeDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_TypeDecl T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_javafe_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_OperatorTags T_java_lang_Object) true_term) (= T_javafe_ast_OperatorTags (asChild T_javafe_ast_OperatorTags T_java_lang_Object)) (= (PO_LT T_javafe_ast_OperatorTags T_javafe_ast_GeneratedTags) true_term) (= (PO_LT T_javafe_ast_TagConstants T_javafe_ast_OperatorTags) true_term) (= T_javafe_ast_TagConstants (asChild T_javafe_ast_TagConstants T_javafe_ast_OperatorTags)) (= (PO_LT T_javafe_ast_GenericBlockStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_GenericBlockStmt (asChild T_javafe_ast_GenericBlockStmt T_javafe_ast_Stmt)) (= (PO_LT T_java_lang_System T_java_lang_Object) true_term) (= T_java_lang_System (asChild T_java_lang_System T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_System) true_term) (= ?t T_java_lang_System))) (= (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_Stmt T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_Stmt (asChild T_javafe_ast_Stmt T_javafe_ast_ASTNode)) (= (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_tc_EnvForCU T_javafe_tc_Env) true_term) (= T_javafe_tc_EnvForCU (asChild T_javafe_tc_EnvForCU T_javafe_tc_Env)) (= (PO_LT T_java_io_Serializable T_java_lang_Object) true_term) (= (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_GeneratedTags 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_Cloneable T_java_lang_Object) 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_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_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_TypeDeclElem T_java_lang_Object) true_term) (= (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_BlockStmt T_javafe_ast_GenericBlockStmt) true_term) (= T_javafe_ast_BlockStmt (asChild T_javafe_ast_BlockStmt T_javafe_ast_GenericBlockStmt)) (= (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_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_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_java_io_OutputStream T_java_lang_Object) true_term) (= T_java_io_OutputStream (asChild T_java_io_OutputStream T_java_lang_Object)) (= (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_io_PrintStream T_java_io_FilterOutputStream) true_term) (= T_java_io_PrintStream (asChild T_java_io_PrintStream T_java_io_FilterOutputStream)) (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_tc_FieldDeclVec (+ DIST_ZERO_1 10)) (= T_javafe_ast_ASTDecoration (+ DIST_ZERO_1 11)) (= T_javafe_parser_TagConstants (+ DIST_ZERO_1 12)) (= T_javafe_ast_Identifier (+ DIST_ZERO_1 13)) (= T_javafe_tc_MethodDeclVec (+ DIST_ZERO_1 14)) (= T_java_io_FilterOutputStream (+ DIST_ZERO_1 15)) (= T_java_lang_Comparable (+ DIST_ZERO_1 16)) (= T_java_util_Properties (+ DIST_ZERO_1 17)) (= T_javafe_ast_GenericVarDecl (+ DIST_ZERO_1 18)) (= T_javafe_ast_Type (+ DIST_ZERO_1 19)) (= T_java_util_EscjavaKeyValue (+ DIST_ZERO_1 20)) (= T_javafe_ast_TypeDecl (+ DIST_ZERO_1 21)) (= T_javafe_tc_Env (+ DIST_ZERO_1 22)) (= T_javafe_ast_OperatorTags (+ DIST_ZERO_1 23)) (= T_javafe_ast_TagConstants (+ DIST_ZERO_1 24)) (= T_javafe_ast_GenericBlockStmt (+ DIST_ZERO_1 25)) (= T_java_lang_System (+ DIST_ZERO_1 26)) (= T_javafe_ast_CompilationUnit (+ DIST_ZERO_1 27)) (= T_javafe_ast_Stmt (+ DIST_ZERO_1 28)) (= T_java_lang_String (+ DIST_ZERO_1 29)) (= T_javafe_tc_EnvForCU (+ DIST_ZERO_1 30)) (= T_java_io_Serializable (+ DIST_ZERO_1 31)) (= T_javafe_ast_RoutineDecl (+ DIST_ZERO_1 32)) (= T_javafe_ast_GeneratedTags (+ DIST_ZERO_1 33)) (= T_javafe_util_Location (+ DIST_ZERO_1 34)) (= T_java_lang_Cloneable (+ DIST_ZERO_1 35)) (= T_javafe_tc_EnvForTypeSig (+ DIST_ZERO_1 36)) (= T_javafe_tc_TypeSig (+ DIST_ZERO_1 37)) (= T_javafe_ast_MethodDecl (+ DIST_ZERO_1 38)) (= T_javafe_ast_TypeDeclElem (+ DIST_ZERO_1 39)) (= T_java_lang_Object (+ DIST_ZERO_1 40)) (= T_java_util_Map (+ DIST_ZERO_1 41)) (= T_javafe_ast_BlockStmt (+ DIST_ZERO_1 42)) (= T_java_util_Hashtable (+ DIST_ZERO_1 43)) (= T_javafe_ast_ASTNode (+ DIST_ZERO_1 44)) (= T_javafe_ast_FieldDecl (+ DIST_ZERO_1 45)) (= T_java_io_OutputStream (+ DIST_ZERO_1 46)) (= T_java_util_Dictionary (+ DIST_ZERO_1 47)) (= T_java_io_PrintStream (+ DIST_ZERO_1 48))) (= true_term (is keywordStrings_63_181_30 ?v_0)) (not (= keywordStrings_63_181_30 null)) (= (typeof keywordStrings_63_181_30) ?v_0) (= (arrayLength keywordStrings_63_181_30) 51) (= true_term (is STRINGLIT_64_44_26 T_int)) (= STRINGLIT_64_44_26 110) (= true_term (is IDENT_64_25_26 T_int)) (= IDENT_64_25_26 93) (= true_term (is MODIFIERPRAGMA_63_25_26 T_int)) (= MODIFIERPRAGMA_63_25_26 115) (= true_term (is NULL_63_82_26 T_int)) (= NULL_63_82_26 163) (= true_term (is otherCodes_63_202_27 ?v_1)) (not (= otherCodes_63_202_27 null)) (= (typeof otherCodes_63_202_27) ?v_1) (= (arrayLength otherCodes_63_202_27) 15) (= true_term (is otherStrings_63_193_30 ?v_0)) (not (= otherStrings_63_193_30 null)) (= (typeof otherStrings_63_193_30) ?v_0) (= (arrayLength otherStrings_63_193_30) 15) (= true_term (is LONGLIT_64_40_26 T_int)) (= LONGLIT_64_40_26 106) (= true_term (is noTokens_63_212_27 T_int)) (= true_term (is TYPEMODIFIERPRAGMA_63_28_26 T_int)) (= TYPEMODIFIERPRAGMA_63_28_26 118) (= true_term (is DOUBLELIT_64_43_26 T_int)) (= DOUBLELIT_64_43_26 109) (= true_term (is LEXICALPRAGMA_63_24_26 T_int)) (= LEXICALPRAGMA_63_24_26 114) (= true_term (is out_20_83_49 T_java_io_PrintStream)) (= true_term (is punctuationStrings_63_134_22 ?v_0)) (not (= punctuationStrings_63_134_22 null)) (= (typeof punctuationStrings_63_134_22) ?v_0) (= (arrayLength punctuationStrings_63_134_22) 48) (= true_term (is INTLIT_64_39_26 T_int)) (= INTLIT_64_39_26 105) (= true_term (is TYPEDECLELEMPRAGMA_63_27_26 T_int)) (= TYPEDECLELEMPRAGMA_63_27_26 117) (= true_term (is punctuationCodes_63_164_19 ?v_1)) (not (= punctuationCodes_63_164_19 null)) (= (typeof punctuationCodes_63_164_19) ?v_1) (= (arrayLength punctuationCodes_63_164_19) 48) (= true_term (is FIRST_KEYWORD_63_51_26 T_int)) (= FIRST_KEYWORD_63_51_26 133) (= true_term (is FLOATLIT_64_42_26 T_int)) (= FLOATLIT_64_42_26 108) (= true_term (is PARSED_6_772_28 T_int)) (= PARSED_6_772_28 2) (= true_term (is LAST_KEYWORD_63_103_26 T_int)) (= LAST_KEYWORD_63_103_26 183) (= true_term (is PREPPED_6_775_28 T_int)) (= PREPPED_6_775_28 5) (= true_term (is BOOLEANLIT_64_38_26 T_int)) (= BOOLEANLIT_64_38_26 104) (= true_term (is STMTPRAGMA_63_26_26 T_int)) (= STMTPRAGMA_63_26_26 116) (= true_term (is CHARLIT_64_41_26 T_int)) (= CHARLIT_64_41_26 107))))
(declare-fun staticContext_pre_46_22 () Int)
(declare-fun staticContext_46_22 () Int)
(declare-fun keywordStrings_pre_63_181_30 () Int)
(declare-fun STRINGLIT_pre_64_44_26 () Int)
(declare-fun enclosingEnv_pre_6_52_36 () Int)
(declare-fun enclosingEnv_6_52_36 () Int)
(declare-fun id_pre_16_15_34 () Int)
(declare-fun id_16_15_34 () Int)
(declare-fun IDENT_pre_64_25_26 () Int)
(declare-fun CU_pre_6_71_30 () Int)
(declare-fun CU_6_71_30 () Int)
(declare-fun MODIFIERPRAGMA_pre_63_25_26 () Int)
(declare-fun NULL_pre_63_82_26 () Int)
(declare-fun otherCodes_pre_63_202_27 () Int)
(declare-fun member_pre_6_44_39 () Int)
(declare-fun member_6_44_39 () Int)
(declare-fun methods_pre_6_883_26 () Int)
(declare-fun methods_6_883_26 () Int)
(declare-fun otherStrings_pre_63_193_30 () Int)
(declare-fun LONGLIT_pre_64_40_26 () Int)
(declare-fun simpleName_pre_6_37_38 () Int)
(declare-fun simpleName_6_37_38 () Int)
(declare-fun noTokens_pre_63_212_27 () Int)
(declare-fun elements_pre_15_61_39 () Int)
(declare-fun elements_15_61_39 () Int)
(declare-fun TYPEMODIFIERPRAGMA_pre_63_28_26 () Int)
(declare-fun id_pre_28_32_34 () Int)
(declare-fun id_28_32_34 () Int)
(declare-fun DOUBLELIT_pre_64_43_26 () Int)
(declare-fun fields_pre_6_875_27 () Int)
(declare-fun fields_6_875_27 () Int)
(declare-fun LEXICALPRAGMA_pre_63_24_26 () Int)
(declare-fun owner_pre_5_35_28 () Int)
(declare-fun owner_5_35_28 () Int)
(declare-fun out_pre_20_83_49 () Int)
(declare-fun parent_pre_33_32 () Int)
(declare-fun parent_33_32 () Int)
(declare-fun punctuationStrings_pre_63_134_22 () Int)
(declare-fun INTLIT_pre_64_39_26 () Int)
(declare-fun count_pre_56_67_33 () Int)
(declare-fun count_56_67_33 () Int)
(declare-fun TYPEDECLELEMPRAGMA_pre_63_27_26 () Int)
(declare-fun punctuationCodes_pre_63_164_19 () Int)
(declare-fun FIRST_KEYWORD_pre_63_51_26 () Int)
(declare-fun peer_pre_38_36 () Int)
(declare-fun peer_38_36 () Int)
(declare-fun FLOATLIT_pre_64_42_26 () Int)
(declare-fun state_pre_6_787_15 () Int)
(declare-fun state_6_787_15 () Int)
(declare-fun myTypeDecl_pre_6_63_40 () Int)
(declare-fun myTypeDecl_6_63_40 () Int)
(declare-fun enclosingType_pre_6_32_39 () Int)
(declare-fun enclosingType_6_32_39 () Int)
(declare-fun PARSED_pre_6_772_28 () Int)
(declare-fun LAST_KEYWORD_pre_63_103_26 () Int)
(declare-fun tokenType_pre_19_90_8 () Int)
(declare-fun tokenType_19_90_8 () Int)
(declare-fun count_pre_15_67_33 () Int)
(declare-fun count_15_67_33 () Int)
(declare-fun PREPPED_pre_6_775_28 () Int)
(declare-fun BOOLEANLIT_pre_64_38_26 () Int)
(declare-fun STMTPRAGMA_pre_63_26_26 () Int)
(declare-fun elements_pre_56_61_38 () Int)
(declare-fun elements_56_61_38 () Int)
(declare-fun CHARLIT_pre_64_41_26 () 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 RES () Int)
(declare-fun ecReturn () Int)
(assert (let ((?v_0 (array T_java_lang_String)) (?v_1 (array T_int)) (?v_3 (not (= this null))) (?v_2 (= ecReturn ecReturn))) (not (=> true (=> (and (= staticContext_pre_46_22 staticContext_46_22) (= staticContext_46_22 (asField staticContext_46_22 T_boolean)) (= keywordStrings_pre_63_181_30 keywordStrings_63_181_30) (= true_term (is keywordStrings_63_181_30 ?v_0)) (= true_term (isAllocated keywordStrings_63_181_30 alloc)) (= STRINGLIT_pre_64_44_26 STRINGLIT_64_44_26) (= true_term (is STRINGLIT_64_44_26 T_int)) (= enclosingEnv_pre_6_52_36 enclosingEnv_6_52_36) (= enclosingEnv_6_52_36 (asField enclosingEnv_6_52_36 T_javafe_tc_Env)) (< (fClosedTime enclosingEnv_6_52_36) alloc) (= id_pre_16_15_34 id_16_15_34) (= id_16_15_34 (asField id_16_15_34 T_javafe_ast_Identifier)) (< (fClosedTime id_16_15_34) alloc) (forall ((?s Int)) (=> (not (= ?s null)) (not (= (S_select id_16_15_34 ?s) null)))) (= IDENT_pre_64_25_26 IDENT_64_25_26) (= true_term (is IDENT_64_25_26 T_int)) (= CU_pre_6_71_30 CU_6_71_30) (= CU_6_71_30 (asField CU_6_71_30 T_javafe_ast_CompilationUnit)) (< (fClosedTime CU_6_71_30) alloc) (= MODIFIERPRAGMA_pre_63_25_26 MODIFIERPRAGMA_63_25_26) (= true_term (is MODIFIERPRAGMA_63_25_26 T_int)) (= NULL_pre_63_82_26 NULL_63_82_26) (= true_term (is NULL_63_82_26 T_int)) (= otherCodes_pre_63_202_27 otherCodes_63_202_27) (= true_term (is otherCodes_63_202_27 ?v_1)) (= true_term (isAllocated otherCodes_63_202_27 alloc)) (= member_pre_6_44_39 member_6_44_39) (= member_6_44_39 (asField member_6_44_39 T_boolean)) (= methods_pre_6_883_26 methods_6_883_26) (= methods_6_883_26 (asField methods_6_883_26 T_javafe_tc_MethodDeclVec)) (< (fClosedTime methods_6_883_26) alloc) (= otherStrings_pre_63_193_30 otherStrings_63_193_30) (= true_term (is otherStrings_63_193_30 ?v_0)) (= true_term (isAllocated otherStrings_63_193_30 alloc)) (= LONGLIT_pre_64_40_26 LONGLIT_64_40_26) (= true_term (is LONGLIT_64_40_26 T_int)) (= simpleName_pre_6_37_38 simpleName_6_37_38) (= simpleName_6_37_38 (asField simpleName_6_37_38 T_java_lang_String)) (< (fClosedTime simpleName_6_37_38) alloc) (= noTokens_pre_63_212_27 noTokens_63_212_27) (= true_term (is noTokens_63_212_27 T_int)) (= elements_pre_15_61_39 elements_15_61_39) (= elements_15_61_39 (asField elements_15_61_39 (array T_javafe_ast_MethodDecl))) (< (fClosedTime elements_15_61_39) alloc) (forall ((?s_1_ Int)) (=> (not (= ?s_1_ null)) (not (= (S_select elements_15_61_39 ?s_1_) null)))) (= TYPEMODIFIERPRAGMA_pre_63_28_26 TYPEMODIFIERPRAGMA_63_28_26) (= true_term (is TYPEMODIFIERPRAGMA_63_28_26 T_int)) (= id_pre_28_32_34 id_28_32_34) (= id_28_32_34 (asField id_28_32_34 T_javafe_ast_Identifier)) (< (fClosedTime id_28_32_34) alloc) (forall ((?s_2_ Int)) (=> (not (= ?s_2_ null)) (not (= (S_select id_28_32_34 ?s_2_) null)))) (= DOUBLELIT_pre_64_43_26 DOUBLELIT_64_43_26) (= true_term (is DOUBLELIT_64_43_26 T_int)) (= fields_pre_6_875_27 fields_6_875_27) (= fields_6_875_27 (asField fields_6_875_27 T_javafe_tc_FieldDeclVec)) (< (fClosedTime fields_6_875_27) alloc) (= LEXICALPRAGMA_pre_63_24_26 LEXICALPRAGMA_63_24_26) (= true_term (is LEXICALPRAGMA_63_24_26 T_int)) (= owner_pre_5_35_28 owner_5_35_28) (= owner_5_35_28 (asField owner_5_35_28 T_java_lang_Object)) (< (fClosedTime owner_5_35_28) alloc) (= out_pre_20_83_49 out_20_83_49) (= true_term (is out_20_83_49 T_java_io_PrintStream)) (= true_term (isAllocated out_20_83_49 alloc)) (not (= out_20_83_49 null)) (= parent_pre_33_32 parent_33_32) (= parent_33_32 (asField parent_33_32 T_javafe_tc_Env)) (< (fClosedTime parent_33_32) alloc) (forall ((?s_3_ Int)) (=> (not (= ?s_3_ null)) (not (= (S_select parent_33_32 ?s_3_) null)))) (= punctuationStrings_pre_63_134_22 punctuationStrings_63_134_22) (= true_term (is punctuationStrings_63_134_22 ?v_0)) (= true_term (isAllocated punctuationStrings_63_134_22 alloc)) (= INTLIT_pre_64_39_26 INTLIT_64_39_26) (= true_term (is INTLIT_64_39_26 T_int)) (= count_pre_56_67_33 count_56_67_33) (= count_56_67_33 (asField count_56_67_33 T_int)) (= TYPEDECLELEMPRAGMA_pre_63_27_26 TYPEDECLELEMPRAGMA_63_27_26) (= true_term (is TYPEDECLELEMPRAGMA_63_27_26 T_int)) (= punctuationCodes_pre_63_164_19 punctuationCodes_63_164_19) (= true_term (is punctuationCodes_63_164_19 ?v_1)) (= true_term (isAllocated punctuationCodes_63_164_19 alloc)) (= FIRST_KEYWORD_pre_63_51_26 FIRST_KEYWORD_63_51_26) (= true_term (is FIRST_KEYWORD_63_51_26 T_int)) (= peer_pre_38_36 peer_38_36) (= peer_38_36 (asField peer_38_36 T_javafe_tc_TypeSig)) (< (fClosedTime peer_38_36) alloc) (forall ((?s_4_ Int)) (=> (not (= ?s_4_ null)) (not (= (S_select peer_38_36 ?s_4_) null)))) (= FLOATLIT_pre_64_42_26 FLOATLIT_64_42_26) (= true_term (is FLOATLIT_64_42_26 T_int)) (= state_pre_6_787_15 state_6_787_15) (= state_6_787_15 (asField state_6_787_15 T_int)) (= myTypeDecl_pre_6_63_40 myTypeDecl_6_63_40) (= myTypeDecl_6_63_40 (asField myTypeDecl_6_63_40 T_javafe_ast_TypeDecl)) (< (fClosedTime myTypeDecl_6_63_40) alloc) (= enclosingType_pre_6_32_39 enclosingType_6_32_39) (= enclosingType_6_32_39 (asField enclosingType_6_32_39 T_javafe_tc_TypeSig)) (< (fClosedTime enclosingType_6_32_39) alloc) (= PARSED_pre_6_772_28 PARSED_6_772_28) (= true_term (is PARSED_6_772_28 T_int)) (= LAST_KEYWORD_pre_63_103_26 LAST_KEYWORD_63_103_26) (= true_term (is LAST_KEYWORD_63_103_26 T_int)) (= tokenType_pre_19_90_8 tokenType_19_90_8) (= tokenType_19_90_8 (asField tokenType_19_90_8 T_int)) (= count_pre_15_67_33 count_15_67_33) (= count_15_67_33 (asField count_15_67_33 T_int)) (= PREPPED_pre_6_775_28 PREPPED_6_775_28) (= true_term (is PREPPED_6_775_28 T_int)) (= BOOLEANLIT_pre_64_38_26 BOOLEANLIT_64_38_26) (= true_term (is BOOLEANLIT_64_38_26 T_int)) (= STMTPRAGMA_pre_63_26_26 STMTPRAGMA_63_26_26) (= true_term (is STMTPRAGMA_63_26_26 T_int)) (= elements_pre_56_61_38 elements_56_61_38) (= elements_56_61_38 (asField elements_56_61_38 (array T_javafe_ast_FieldDecl))) (< (fClosedTime elements_56_61_38) alloc) (forall ((?s_5_ Int)) (=> (not (= ?s_5_ null)) (not (= (S_select elements_56_61_38 ?s_5_) null)))) (= CHARLIT_pre_64_41_26 CHARLIT_64_41_26) (= true_term (is CHARLIT_64_41_26 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_EnvForTypeSig)) (= true_term (isAllocated this alloc)) ?v_3 (= RES (S_select peer_38_36 this)) (= true_term true_term) (or (not ?v_2) (and ?v_2 (not (=> ?v_2 (= (and (= true_term (is this T_javafe_tc_EnvForCU)) ?v_3) (= RES null)))))))))))))
(check-sat)
(exit)