path: root/test/regress/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2

; COMMAND-LINE: --qcf-tconstraint
; EXPECT: unsat
(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 EC_134.22_134.22 () Int)
(declare-fun integralOr (Int Int) Int)
(declare-fun this_95.46_87.8_0_95.46 () Int)
(declare-fun EC_183.16_183.16 () Int)
(declare-fun arrayShapeMore (Int Int) Int)
(declare-fun integralAnd (Int Int) Int)
(declare-fun T_.TYPE () Int)
(declare-fun EC_156.1_0_158.5_0_159.22_159.22 () Int)
(declare-fun intFirst () Int)
(declare-fun after_192.22_192.22 () Int)
(declare-fun T_javafe.filespace.HashTree () Int)
(declare-fun lookAhead_4.43.19 () Int)
(declare-fun after_90.24_87.8_0_90.24_5.89.17 () Int)
(declare-fun eClosedTime (Int) Int)
(declare-fun int_m9223372036854775808 () Int)
(declare-fun C_87.8 () Int)
(declare-fun int_m2147483648 () Int)
(declare-fun T_java.lang.Comparable () Int)
(declare-fun arrayPosition (Int) Int)
(declare-fun treeName_186.1 () Int)
(declare-fun remainingNodes_loopold_48.26 () Int)
(declare-fun after_189.12_189.12 () Int)
(declare-fun this_159.11_156.1_0_158.5_0_159.11 () Int)
(declare-fun select1 (Int Int) Int)
(declare-fun select2 (Int Int Int) Int)
(declare-fun EC_192.22_192.22 () Int)
(declare-fun L_158.5 () Int)
(declare-fun T_java.util.EscjavaKeyValue () Int)
(declare-fun elems_1_ () Int)
(declare-fun c_loopold_133.5 () Int)
(declare-fun T_long () Int)
(declare-fun EC_121.8_121.8 () Int)
(declare-fun EC_65.1_65.1 () Int)
(declare-fun moreElements_192.1_0_193.28_5.89.17 () Int)
(declare-fun after_121.8_121.8 () Int)
(declare-fun T_javafe.filespace.LookAheadEnum () Int)
(declare-fun lockLE (Int Int) Bool)
(declare-fun classLiteral (Int) Int)
(declare-fun lockLT (Int Int) Bool)
(declare-fun T_javafe.filespace.Tree () Int)
(declare-fun elems_2_ () Int)
(declare-fun EC_189.12_189.12 () Int)
(declare-fun T_float () Int)
(declare-fun alloc () Int)
(declare-fun T_java.io.OutputStream () Int)
(declare-fun EC_87.8_0_89.24_89.24 () Int)
(declare-fun S_194.56 () Int)
(declare-fun asChild (Int Int) Int)
(declare-fun CONCVARSYM (Int) Int)
(declare-fun T_int () Int)
(declare-fun after_65.1_65.1 () Int)
(declare-fun int_2147483647 () Int)
(declare-fun RES_130.35 () Int)
(declare-fun remainingNodes_48.26_1_ () Int)
(declare-fun int_9223372036854775807 () Int)
(declare-fun this () Int)
(declare-fun T_byte () Int)
(declare-fun T_java.lang.System () Int)
(declare-fun store1 (Int Int Int) Int)
(declare-fun store2 (Int Int Int Int) Int)
(declare-fun RES_loopold () Int)
(declare-fun remainingNodes_48.26_2_ () Int)
(declare-fun max (Int) Int)
(declare-fun elems_156.1_0_158.5_0_1_ () Int)
(declare-fun moreElements_pre_5.58.29 () Int)
(declare-fun moreElements_87.8_0_90.24_5.89.17 () Int)
(declare-fun objectToBeConstructed () Int)
(declare-fun T_java.util.Map () Int)
(declare-fun tmp4_156.1_0_158.5_0_163.8 () Int)
(declare-fun T_javafe.filespace.TreeWalker () Int)
(declare-fun after_189.25_189.25 () Int)
(declare-fun integralDiv (Int Int) Int)
(declare-fun i_156.1_0_158.5_0_158.33 () Int)
(declare-fun after_135.35_134.1_0_135.35_5.89.17 () Int)
(declare-fun EC_130.36_130.36 () Int)
(declare-fun RES_121.33_121.33 () Int)
(declare-fun moreElements_loopold_5.58.29 () Int)
(declare-fun RES_134.22_134.22 () Int)
(declare-fun list_210.13 () Int)
(declare-fun EC_189.25_189.25 () Int)
(declare-fun T_java.lang.Class () Int)
(declare-fun T_java.lang.Object () Int)
(declare-fun tmp_156.1_0_158.5_0_161.6 () Int)
(declare-fun remainingChildren_pre_39.26 () Int)
(declare-fun EC_192.1_1_192.45_192.45 () Int)
(declare-fun RES_192.1_1_192.45_192.45 () Int)
(declare-fun RES_156.1_0_158.5_0_160.18_160.18 () Int)
(declare-fun longLast () Int)
(declare-fun termConditional (Int Int Int) Int)
(declare-fun T_java.util.Dictionary () Int)
(declare-fun C_156.1 () Int)
(declare-fun bool_false () Int)
(declare-fun RES_192.22_192.22 () Int)
(declare-fun T_javafe.filespace.FileTree () Int)
(declare-fun alloc_loopold () Int)
(declare-fun Smt.true () Int)
(declare-fun returnsNull_5.79.29 () Int)
(declare-fun c_134.1_0_135.20 () Int)
(declare-fun asLockSet (Int) Int)
(declare-fun integralMod (Int Int) Int)
(declare-fun RES_67.21_67.21 () Int)
(declare-fun RES_156.1_0_158.5_0_159.11_159.11 () Int)
(declare-fun Smt.false () Int)
(declare-fun typeof (Int) Int)
(declare-fun int_18446744073709551615 () Int)
(declare-fun RES_189.12_189.12 () Int)
(declare-fun this_160.18_156.1_0_158.5_0_160.18 () Int)
(declare-fun EC_134.1_0_134.36_134.36 () Int)
(declare-fun RES_89.23 () Int)
(declare-fun RES_134.1_0_134.36_134.36 () Int)
(declare-fun RES_87.8_0_93.28_93.28 () Int)
(declare-fun elementType_5.74.27 () Int)
(declare-fun stringCat (Int Int) Int)
(declare-fun remainingChildren_39.26_1_ () Int)
(declare-fun RES_87.8_0_95.46_95.46 () Int)
(declare-fun lookAheadValid_4.40.20 () Int)
(declare-fun T_boolean () Int)
(declare-fun longFirst () Int)
(declare-fun elems_loopold_156.1_0 () Int)
(declare-fun T_java.util.Hashtable () Int)
(declare-fun elems_loopold () Int)
(declare-fun T_java.util.Properties () Int)
(declare-fun L_87.8 () Int)
(declare-fun RES_68.21_68.21 () Int)
(declare-fun RES_65.1_65.1 () Int)
(declare-fun arrayFresh (Int Int Int Int Int Int Int) Bool)
(declare-fun RES () Int)
(declare-fun elementType_pre_5.74.27 () Int)
(declare-fun L_156.1 () Int)
(declare-fun intLast () Int)
(declare-fun RES_130.36_130.36 () Int)
(declare-fun RES_87.8_0_90.24_90.24 () Int)
(declare-fun arrayType () Int)
(declare-fun RES_189.25_189.25 () Int)
(declare-fun boolEq (Int Int) Bool)
(declare-fun EC_134.1_0_135.35_135.35 () Int)
(declare-fun after_193.28_192.1_0_193.28_5.89.17 () Int)
(declare-fun RES_134.1_0_135.35_135.35 () Int)
(declare-fun T_129.49 () Int)
(declare-fun arrayLength (Int) Int)
(declare-fun cast (Int Int) Int)
(declare-fun nextChild_87.8_0_95.5 () Int)
(declare-fun elementType_71.16 () Int)
(declare-fun asElems (Int) Int)
(declare-fun T_javafe.filespace.PreloadedTree () Int)
(declare-fun moreElements_5.58.29 () Int)
(declare-fun T_char () Int)
(declare-fun EC_192.1_0_194.16_194.16 () Int)
(declare-fun owner_pre_6.35.28 () Int)
(declare-fun RES_156.1_0_158.5_0_159.22_159.22 () Int)
(declare-fun EC_140.1_140.1 () Int)
(declare-fun divides (Int Int) Int)
(declare-fun returnsNull_72.16 () Int)
(declare-fun remainingChildren_39.26 () Int)
(declare-fun remainingNodes_68.1 () Int)
(declare-fun T_javafe.filespace.TreeWalker_ArrayEnum () Int)
(declare-fun arg0_194.16_192.1_0_194.16_17.. () Int)
(declare-fun InRange (Int Int) Bool)
(declare-fun moreElements_87.8_0_95.46_5.89.17 () Int)
(declare-fun sorted_157.13 () Int)
(declare-fun moreElements_134.1_0_135.35_5.89.17 () Int)
(declare-fun out_pre_16.83.49 () Int)
(declare-fun elementType_69.24 () Int)
(declare-fun RES_121.8_121.8 () Int)
(declare-fun lookAheadValid_pre_4.40.20 () Int)
(declare-fun refEQ (Int Int) Int)
(declare-fun EC_loopold () Int)
(declare-fun EC_157.5 () Int)
(declare-fun remainingNodes_pre_48.26 () Int)
(declare-fun EC_156.1_0_158.5_0_160.18_160.18 () Int)
(declare-fun subtree_192.1_0_193.5 () Int)
(declare-fun is (Int Int) Int)
(declare-fun i_loopold_156.1_0_158.14 () Int)
(declare-fun integralEQ (Int Int) Int)
(declare-fun RES_87.8_0_89.24_89.24 () Int)
(declare-fun boolNE (Int Int) Bool)
(declare-fun EC_134.1_1_134.36_134.36 () Int)
(declare-fun RES_134.1_1_134.36_134.36 () Int)
(declare-fun T_java.io.FilterOutputStream () Int)
(declare-fun remainingNodes_48.26 () Int)
(declare-fun tmp0_new_Tree___130.25 () Int)
(declare-fun isNewArray (Int) Int)
(declare-fun L_192.1 () Int)
(declare-fun elems_pre () Int)
(declare-fun T_63.27 () Int)
(declare-fun intShiftL (Int Int) Int)
(declare-fun nonnullelements (Int Int) Bool)
(declare-fun multiply (Int Int) Int)
(declare-fun integralGE (Int Int) Int)
(declare-fun lookAhead_pre_4.43.19 () Int)
(declare-fun T_short () Int)
(declare-fun EC_67.21_67.21 () Int)
(declare-fun alloc_pre () Int)
(declare-fun integralGT (Int Int) Int)
(declare-fun EC () Int)
(declare-fun boolAnd (Int Int) Bool)
(declare-fun EC_156.1_0_158.5_0_159.11_159.11 () Int)
(declare-fun EC_1_ () Int)
(declare-fun EC_192.1_0_194.32_194.32 () Int)
(declare-fun RES_192.1_0_194.32_194.32 () Int)
(declare-fun arrayShapeOne (Int) Int)
(declare-fun T_double () Int)
(declare-fun out_16.83.49 () Int)
(declare-fun owner_6.35.28 () Int)
(declare-fun longShiftL (Int Int) Int)
(declare-fun list_pre_210.13 () Int)
(declare-fun T_java.io.Serializable () Int)
(declare-fun boolOr (Int Int) Bool)
(declare-fun L_134.1 () Int)
(declare-fun int_4294967295 () Int)
(declare-fun modulo (Int Int) Int)
(declare-fun EC_87.8_0_93.28_93.28 () Int)
(declare-fun EC_2_ () Int)
(declare-fun EC_130.35 () Int)
(declare-fun elems_134.1_0 () Int)
(declare-fun T_120.50 () Int)
(declare-fun returnsNull_pre_5.79.29 () Int)
(declare-fun EC_152.6 () Int)
(declare-fun EC_87.8_0_95.46_95.46 () Int)
(declare-fun EC_182.16 () Int)
(declare-fun after_95.46_87.8_0_95.46_5.89.17 () Int)
(declare-fun null () Int)
(declare-fun args_181.36 () Int)
(declare-fun EC_152.6_1_ () Int)
(declare-fun T_java.lang.String () Int)
(declare-fun asField (Int Int) Int)
(declare-fun a_150.36 () Int)
(declare-fun EC_68.21_68.21 () Int)
(declare-fun T_java.io.File () Int)
(declare-fun after_68.21_68.21 () Int)
(declare-fun boolImplies (Int Int) Bool)
(declare-fun sorted_157.13_1_ () Int)
(declare-fun integralLE (Int Int) Int)
(declare-fun RES_1_ () Int)
(declare-fun tmp0_remainingNodes_69.9 () Int)
(declare-fun elems_156.1_0_158.5_0 () Int)
(declare-fun integralLT (Int Int) Int)
(declare-fun this_93.28_87.8_0_93.28 () Int)
(declare-fun T_java.util.Enumeration () Int)
(declare-fun vAllocTime (Int) Int)
(declare-fun EC_192.1_0_193.28_193.28 () Int)
(declare-fun sorted_157.13_2_ () Int)
(declare-fun this_89.24_87.8_0_89.24 () Int)
(declare-fun T_java.lang.Cloneable () Int)
(declare-fun RES_192.1_0_193.28_193.28 () 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 EC_loopold_156.1_0 () Int)
(declare-fun sorted_loopold_156.1_0_157.13 () Int)
(declare-fun this_90.24_87.8_0_90.24 () Int)
(declare-fun integralNE (Int Int) Int)
(declare-fun T_java.io.PrintStream () Int)
(declare-fun EC_87.8_0_90.24_90.24 () Int)
(declare-fun arrayParent (Int) Int)
(declare-fun elemtype (Int) Int)
(declare-fun fClosedTime (Int) Int)
(declare-fun alloc_1_ () Int)
(declare-fun EC_192.1_0_192.45_192.45 () Int)
(declare-fun array (Int) Int)
(declare-fun RES_192.1_0_192.45_192.45 () Int)
(declare-fun LS () Int)
(declare-fun remainingChildren_67.1 () Int)
(declare-fun ecReturn () Int)
(declare-fun isAllocated (Int Int) Bool)
(declare-fun alloc_2_ () Int)
(declare-fun elems () Int)
(declare-fun subtypes (Int Int) Bool)
(declare-fun T_javafe.filespace.EmptyEnum () Int)
(declare-fun EC_182.16_1_ () Int)
(declare-fun EC_121.33_121.33 () Int)
(assert (subtypes T_java.io.OutputStream T_java.lang.Object))
(assert (= T_java.io.OutputStream (asChild T_java.io.OutputStream T_java.lang.Object)))
(assert (subtypes T_java.io.FilterOutputStream T_java.io.OutputStream))
(assert (= T_java.io.FilterOutputStream (asChild T_java.io.FilterOutputStream T_java.io.OutputStream)))
(assert (subtypes T_javafe.filespace.TreeWalker T_javafe.filespace.LookAheadEnum))
(assert (= T_javafe.filespace.TreeWalker (asChild T_javafe.filespace.TreeWalker T_javafe.filespace.LookAheadEnum)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_javafe.filespace.TreeWalker) (= ?t T_javafe.filespace.TreeWalker)) :pattern ((subtypes ?t T_javafe.filespace.TreeWalker)) )))
(assert (subtypes T_javafe.filespace.FileTree T_javafe.filespace.PreloadedTree))
(assert (= T_javafe.filespace.FileTree (asChild T_javafe.filespace.FileTree T_javafe.filespace.PreloadedTree)))
(assert (subtypes T_javafe.filespace.LookAheadEnum T_java.lang.Object))
(assert (= T_javafe.filespace.LookAheadEnum (asChild T_javafe.filespace.LookAheadEnum T_java.lang.Object)))
(assert (subtypes T_javafe.filespace.LookAheadEnum T_java.util.Enumeration))
(assert (subtypes T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.LookAheadEnum))
(assert (= T_javafe.filespace.TreeWalker_ArrayEnum (asChild T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.LookAheadEnum)))
(assert (subtypes T_javafe.filespace.HashTree T_javafe.filespace.Tree))
(assert (= T_javafe.filespace.HashTree (asChild T_javafe.filespace.HashTree T_javafe.filespace.Tree)))
(assert (subtypes T_java.lang.System T_java.lang.Object))
(assert (= T_java.lang.System (asChild T_java.lang.System T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.System) (= ?t T_java.lang.System)) :pattern ((subtypes ?t T_java.lang.System)) )))
(assert (subtypes T_java.util.EscjavaKeyValue T_java.lang.Object))
(assert (subtypes T_java.util.Properties T_java.util.Hashtable))
(assert (= T_java.util.Properties (asChild T_java.util.Properties T_java.util.Hashtable)))
(assert (subtypes T_javafe.filespace.Tree T_java.lang.Object))
(assert (= T_javafe.filespace.Tree (asChild T_javafe.filespace.Tree T_java.lang.Object)))
(assert (subtypes T_java.lang.String T_java.lang.Object))
(assert (= T_java.lang.String (asChild T_java.lang.String T_java.lang.Object)))
(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.String) (= ?t T_java.lang.String)) :pattern ((subtypes ?t T_java.lang.String)) )))
(assert (subtypes T_java.lang.String T_java.io.Serializable))
(assert (subtypes T_java.lang.String T_java.lang.Comparable))
(assert (subtypes T_java.util.Enumeration T_java.lang.Object))
(assert (subtypes T_java.lang.Comparable T_java.lang.Object))
(assert (subtypes T_java.util.Map T_java.lang.Object))
(assert (subtypes T_java.util.Map T_java.util.EscjavaKeyValue))
(assert (subtypes T_java.util.Dictionary T_java.lang.Object))
(assert (= T_java.util.Dictionary (asChild T_java.util.Dictionary T_java.lang.Object)))
(assert (subtypes T_java.util.Dictionary T_java.util.EscjavaKeyValue))
(assert (subtypes T_java.io.Serializable T_java.lang.Object))
(assert (subtypes T_java.io.PrintStream T_java.io.FilterOutputStream))
(assert (= T_java.io.PrintStream (asChild T_java.io.PrintStream T_java.io.FilterOutputStream)))
(assert (subtypes T_javafe.filespace.PreloadedTree T_javafe.filespace.HashTree))
(assert (= T_javafe.filespace.PreloadedTree (asChild T_javafe.filespace.PreloadedTree T_javafe.filespace.HashTree)))
(assert (subtypes T_java.util.Hashtable T_java.util.Dictionary))
(assert (= T_java.util.Hashtable (asChild T_java.util.Hashtable T_java.util.Dictionary)))
(assert (subtypes T_java.util.Hashtable T_java.util.Map))
(assert (subtypes T_java.util.Hashtable T_java.lang.Cloneable))
(assert (subtypes T_java.util.Hashtable T_java.io.Serializable))
(assert (subtypes T_java.lang.Cloneable T_java.lang.Object))
(assert (subtypes T_javafe.filespace.EmptyEnum T_java.lang.Object))
(assert (= T_javafe.filespace.EmptyEnum (asChild T_javafe.filespace.EmptyEnum T_java.lang.Object)))
(assert (subtypes T_javafe.filespace.EmptyEnum T_java.util.Enumeration))
(assert (subtypes T_java.io.File T_java.lang.Object))
(assert (= T_java.io.File (asChild T_java.io.File T_java.lang.Object)))
(assert (subtypes T_java.io.File T_java.io.Serializable))
(assert (subtypes T_java.io.File T_java.lang.Comparable))
(assert (distinct arrayType T_boolean T_char T_byte T_short T_int T_long T_float T_double T_.TYPE T_java.io.OutputStream T_java.io.FilterOutputStream T_javafe.filespace.TreeWalker T_javafe.filespace.FileTree T_javafe.filespace.LookAheadEnum T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.HashTree T_java.lang.System T_java.util.EscjavaKeyValue T_java.util.Properties T_javafe.filespace.Tree T_java.lang.String T_java.util.Enumeration T_java.lang.Comparable T_java.util.Map T_java.util.Dictionary T_java.io.Serializable T_java.io.PrintStream T_javafe.filespace.PreloadedTree T_java.util.Hashtable T_java.lang.Cloneable T_javafe.filespace.EmptyEnum T_java.io.File T_java.lang.Object))
(assert (= Smt.true (is out_16.83.49 T_java.io.PrintStream)))
(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 (not (= args_181.36 null)))) (let ((?v_1 (not ?v_0)) (?v_3 (arrayLength args_181.36))) (let ((?v_61 (not (= ?v_3 1)))) (let ((?v_29 (not ?v_61)) (?v_8 (= Smt.true Smt.true)) (?v_2 (<= 0 0)) (?v_4 (< 0 ?v_3)) (?v_30 (= treeName_186.1 (select1 (select1 elems args_181.36) 0))) (?v_5 (not (= treeName_186.1 null))) (?v_31 (< alloc after_189.25_189.25)) (?v_6 (not (= RES_189.25_189.25 null))) (?v_32 (not (isAllocated RES_189.25_189.25 alloc))) (?v_33 (= Smt.true (is RES_189.25_189.25 T_java.io.File))) (?v_34 (isAllocated RES_189.25_189.25 after_189.25_189.25)) (?v_35 (= EC_189.25_189.25 ecReturn)) (?v_36 (= (select1 owner_6.35.28 RES_189.25_189.25) null)) (?v_37 (= (typeof RES_189.25_189.25) T_java.io.File)) (?v_38 (< after_189.25_189.25 after_189.12_189.12)) (?v_7 (not (= RES_189.12_189.12 null))) (?v_39 (not (isAllocated RES_189.12_189.12 after_189.25_189.25))) (?v_40 (= Smt.true (is RES_189.12_189.12 T_javafe.filespace.FileTree))) (?v_41 (isAllocated RES_189.12_189.12 after_189.12_189.12)) (?v_42 (= EC_189.12_189.12 ecReturn)) (?v_43 (= (select1 owner_6.35.28 RES_189.12_189.12) null)) (?v_44 (= (typeof RES_189.12_189.12) T_javafe.filespace.FileTree)) (?v_45 (< after_189.12_189.12 after_192.22_192.22)) (?v_9 (not (= RES_192.22_192.22 null))) (?v_46 (not (isAllocated RES_192.22_192.22 after_189.12_189.12))) (?v_47 (= Smt.true (is RES_192.22_192.22 T_javafe.filespace.TreeWalker))) (?v_48 (isAllocated RES_192.22_192.22 after_192.22_192.22)) (?v_49 (= EC_192.22_192.22 ecReturn)) (?v_50 (= (select1 owner_6.35.28 RES_192.22_192.22) null)) (?v_51 (= (typeof RES_192.22_192.22) T_javafe.filespace.TreeWalker)) (?v_52 (= EC_192.22_192.22 EC_loopold)) (?v_53 (= moreElements_5.58.29 moreElements_loopold_5.58.29))) (let ((?v_12 (not ?v_9)) (?v_17 (= Smt.true (is RES_192.1_0_192.45_192.45 T_boolean))) (?v_10 (= EC_192.1_0_192.45_192.45 ecReturn)) (?v_11 (= Smt.true RES_192.1_0_192.45_192.45)) (?v_13 (= Smt.true (select1 moreElements_5.58.29 RES_192.22_192.22)))) (let ((?v_18 (=> ?v_10 (= ?v_11 ?v_13))) (?v_19 (= moreElements_192.1_0_193.28_5.89.17 (store1 moreElements_5.58.29 RES_192.22_192.22 after_193.28_192.1_0_193.28_5.89.17))) (?v_20 (= moreElements_192.1_0_193.28_5.89.17 (asField moreElements_192.1_0_193.28_5.89.17 T_boolean))) (?v_21 (= Smt.true (is RES_192.1_0_193.28_193.28 T_java.lang.Object))) (?v_22 (isAllocated RES_192.1_0_193.28_193.28 after_192.22_192.22)) (?v_14 (= EC_192.1_0_193.28_193.28 ecReturn)) (?v_15 (= RES_192.1_0_193.28_193.28 null))) (let ((?v_23 (=> ?v_14 (or (subtypes (typeof RES_192.1_0_193.28_193.28) (select1 elementType_5.74.27 RES_192.22_192.22)) ?v_15))) (?v_24 (=> (and ?v_14 (not (= Smt.true (select1 returnsNull_5.79.29 RES_192.22_192.22)))) (not ?v_15))) (?v_25 (forall ((?brokenObj_11_ Int)) (let ((?v_65 (= Smt.true (select1 lookAheadValid_4.40.20 ?brokenObj_11_))) (?v_66 (not (= (select1 lookAhead_4.43.19 ?brokenObj_11_) null)))) (=> (and (= Smt.true (is ?brokenObj_11_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_11_ null)) (=> ?v_65 (= (= Smt.true (select1 moreElements_5.58.29 ?brokenObj_11_)) ?v_66)) ?v_65) (= (= Smt.true (select1 moreElements_192.1_0_193.28_5.89.17 ?brokenObj_11_)) ?v_66))))) (?v_16 (= Smt.true (is RES_192.1_0_193.28_193.28 T_javafe.filespace.Tree))) (?v_26 (= subtree_192.1_0_193.5 (cast RES_192.1_0_193.28_193.28 T_javafe.filespace.Tree))) (?v_27 (not (= subtree_192.1_0_193.5 null))) (?v_54 (= Smt.true (is RES_192.1_0_194.32_194.32 T_java.lang.String))) (?v_55 (isAllocated RES_192.1_0_194.32_194.32 after_192.22_192.22)) (?v_28 (= EC_192.1_0_194.32_194.32 ecReturn))) (let ((?v_56 (=> ?v_28 (not (= RES_192.1_0_194.32_194.32 null)))) (?v_57 (= arg0_194.16_192.1_0_194.16_17.. (stringCat RES_192.1_0_194.32_194.32 S_194.56))) (?v_58 (= EC_192.1_0_194.16_194.16 ecReturn)) (?v_59 (= EC_192.1_1_192.45_192.45 ecReturn)) (?v_60 (= Smt.true RES_192.1_1_192.45_192.45))) (let ((?v_62 (or (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 (not ?v_11)) (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 ?v_9 ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 ?v_16 ?v_26 ?v_27 ?v_54 ?v_55 ?v_28 ?v_56 ?v_57 ?v_58 ?v_8 ?v_9 (= Smt.true (is RES_192.1_1_192.45_192.45 T_boolean)) ?v_59 (=> ?v_59 (= ?v_60 (= Smt.true (select1 moreElements_192.1_0_193.28_5.89.17 RES_192.22_192.22)))) (not ?v_60)))) (?v_63 (= L_192.1 L_192.1)) (?v_64 (= EC_182.16 ecReturn))) (not (=> (and (distinct ecReturn L_192.1) (not (= S_194.56 null)) (= (typeof S_194.56) T_java.lang.String)) (=> (and (= elementType_pre_5.74.27 elementType_5.74.27) (= elementType_5.74.27 (asField elementType_5.74.27 T_.TYPE)) (= owner_pre_6.35.28 owner_6.35.28) (= owner_6.35.28 (asField owner_6.35.28 T_java.lang.Object)) (< (fClosedTime owner_6.35.28) alloc) (= list_pre_210.13 list_210.13) (= list_210.13 (asField list_210.13 (array T_java.lang.Object))) (< (fClosedTime list_210.13) alloc) (= lookAheadValid_pre_4.40.20 lookAheadValid_4.40.20) (= lookAheadValid_4.40.20 (asField lookAheadValid_4.40.20 T_boolean)) (= remainingNodes_pre_48.26 remainingNodes_48.26) (= remainingNodes_48.26 (asField remainingNodes_48.26 T_java.util.Enumeration)) (< (fClosedTime remainingNodes_48.26) alloc) (= out_pre_16.83.49 out_16.83.49) (= Smt.true (is out_16.83.49 T_java.io.PrintStream)) (isAllocated out_16.83.49 alloc) (not (= out_16.83.49 null)) (= lookAhead_pre_4.43.19 lookAhead_4.43.19) (= lookAhead_4.43.19 (asField lookAhead_4.43.19 T_java.lang.Object)) (< (fClosedTime lookAhead_4.43.19) alloc) (= returnsNull_pre_5.79.29 returnsNull_5.79.29) (= returnsNull_5.79.29 (asField returnsNull_5.79.29 T_boolean)) (= moreElements_pre_5.58.29 moreElements_5.58.29) (= moreElements_5.58.29 (asField moreElements_5.58.29 T_boolean)) (= remainingChildren_pre_39.26 remainingChildren_39.26) (= remainingChildren_39.26 (asField remainingChildren_39.26 T_java.util.Enumeration)) (< (fClosedTime remainingChildren_39.26) alloc) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= Smt.true (is args_181.36 (array T_java.lang.String))) (isAllocated args_181.36 alloc) (nonnullelements args_181.36 elems) (forall ((?brokenObj Int)) (=> (and (= Smt.true (is ?brokenObj T_javafe.filespace.TreeWalker)) (not (= ?brokenObj null))) (= (select1 elementType_5.74.27 (select1 remainingChildren_39.26 ?brokenObj)) T_javafe.filespace.Tree))) (forall ((?brokenObj_1_ Int)) (=> (and (= Smt.true (is ?brokenObj_1_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_1_ null))) (not (= (select1 remainingChildren_39.26 ?brokenObj_1_) null)))) (forall ((?brokenObj_2_ Int)) (=> (and (= Smt.true (is ?brokenObj_2_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_2_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 ?brokenObj_2_))))) (forall ((?brokenObj_3_ Int)) (=> (and (= Smt.true (is ?brokenObj_3_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_3_ null))) (= (select1 elementType_5.74.27 (select1 remainingNodes_48.26 ?brokenObj_3_)) T_javafe.filespace.Tree))) (forall ((?brokenObj_4_ Int)) (=> (and (= Smt.true (is ?brokenObj_4_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_4_ null)) (= Smt.true (select1 lookAheadValid_4.40.20 ?brokenObj_4_))) (= (= Smt.true (select1 moreElements_5.58.29 ?brokenObj_4_)) (not (= (select1 lookAhead_4.43.19 ?brokenObj_4_) null))))) (forall ((?brokenObj_5_ Int)) (=> (and (= Smt.true (is ?brokenObj_5_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_5_ null))) (not (= (select1 remainingNodes_48.26 ?brokenObj_5_) null)))) (forall ((?brokenObj_6_ Int)) (=> (and (= Smt.true (is ?brokenObj_6_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_6_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 (select1 remainingChildren_39.26 ?brokenObj_6_)))))) (forall ((?brokenObj_7_ Int)) (=> (and (= Smt.true (is ?brokenObj_7_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_7_ null))) (= (select1 elementType_5.74.27 ?brokenObj_7_) T_javafe.filespace.Tree))) (forall ((?brokenObj_8_ Int)) (let ((?v_67 (select1 lookAhead_4.43.19 ?brokenObj_8_))) (=> (and (= Smt.true (is ?brokenObj_8_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_8_ null))) (or (subtypes (typeof ?v_67) (select1 elementType_5.74.27 ?brokenObj_8_)) (= ?v_67 null))))) (forall ((?brokenObj_9_ Int)) (=> (and (= Smt.true (is ?brokenObj_9_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_9_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 (select1 remainingNodes_48.26 ?brokenObj_9_)))))) (forall ((?brokenObj_10_ Int)) (=> (and (= Smt.true (is ?brokenObj_10_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_10_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 ?brokenObj_10_))))) (or ?v_1 (and ?v_0 ?v_29 ?v_8 (or ?v_1 (and ?v_0 (or (not ?v_2) (and ?v_2 (or (not ?v_4) (and ?v_4 ?v_30 (or (not ?v_5) (and ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 (or (not ?v_6) (and ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 (or (not ?v_7) (and ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 (or (and ?v_8 (or ?v_12 (and ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 (or ?v_12 (and ?v_9 (or (not ?v_13) (and ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 (or (not ?v_16) (and ?v_16 ?v_26 (not ?v_27)))))))))) (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 ?v_9 ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 ?v_16 ?v_26 ?v_27 ?v_54 ?v_55 ?v_28 ?v_56 ?v_57 ?v_58 ?v_8 ?v_12))))))))))))))) (and (or (and ?v_0 ?v_29 ?v_8 ?v_0 ?v_2 ?v_4 ?v_30 ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 ?v_62 ?v_63 (= EC L_192.1) ?v_64) (and ?v_0 (or (and ?v_61 ?v_8 (= EC_183.16_183.16 ecReturn) ?v_8 (= EC_182.16_1_ ecReturn)) (and ?v_29 ?v_8 ?v_0 ?v_2 ?v_4 ?v_30 ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 ?v_62 (not ?v_63) (= EC_182.16_1_ L_192.1))) (= EC_182.16 EC_182.16_1_))) (not ?v_64))))))))))))))))))
(check-sat)
(exit)