(PROMPT_OFF)
;----------------------------------------------------------------------
; "Universal", or class-independent part, of the background predicate
; === ESCJ 8: Section 0.4
(BG_PUSH 
  (FORALL 
    (m i x)
    (EQ 
      (select 
        (store m i x)
        i)
      x)
    )
  )
(BG_PUSH 
  (FORALL 
    (m i j x)
    (IMPLIES 
      (NEQ i j)
      (EQ 
        (select 
          (store m i x)
          j)
        (select m j)
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (m i j k x)
    (IMPLIES 
      (OR 
        (< k i)
        (< j k)
        )
      (EQ 
        (select 
          (unset m i j)
          k)
        (select m k)
        )
      )
    )
  )
; === ESCJ 8: Section 1.1
(DEFPRED 
  (<: t0 t1)
  )
; <: reflexive
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t t)
      )
    (<: t t)
    )
  )
; a special case, for which the above may not fire
(BG_PUSH 
  (<: |T_java.lang.Object| |T_java.lang.Object|)
  )
; <: transitive	
(BG_PUSH 
  (FORALL 
    (t0 t1 t2)
    (PATS 
      (MPAT 
        (<: t0 t1)
        (<: t1 t2)
        )
      )
    (IMPLIES 
      (AND 
        (<: t0 t1)
        (<: t1 t2)
        )
      (<: t0 t2)
      )
    )
  )
;anti-symmetry
(BG_PUSH
  (FORALL
    (t0 t1)
    (PATS 
      (MPAT 
        (<: t0 t1)
        (<: t1 t0)
        )
      )
    (IMPLIES 
      (AND 
        (<: t0 t1)
        (<: t1 t0)
        )
      (EQ t0 t1)
      )
    )
  )
; primitive types are final
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_boolean|)
      )
    (IMPLIES 
      (<: t |T_boolean|)
      (EQ t |T_boolean|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_char|)
      )
    (IMPLIES 
      (<: t |T_char|)
      (EQ t |T_char|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_byte|)
      )
    (IMPLIES 
      (<: t |T_byte|)
      (EQ t |T_byte|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_short|)
      )
    (IMPLIES 
      (<: t |T_short|)
      (EQ t |T_short|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_int|)
      )
    (IMPLIES 
      (<: t |T_int|)
      (EQ t |T_int|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_long|)
      )
    (IMPLIES 
      (<: t |T_long|)
      (EQ t |T_long|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_float|)
      )
    (IMPLIES 
      (<: t |T_float|)
      (EQ t |T_float|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_double|)
      )
    (IMPLIES 
      (<: t |T_double|)
      (EQ t |T_double|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_bigint|)
      )
    (IMPLIES 
      (<: t |T_bigint|)
      (EQ t |T_bigint|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_real|)
      )
    (IMPLIES 
      (<: t |T_real|)
      (EQ t |T_real|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: t |T_void|)
      )
    (IMPLIES 
      (<: t |T_void|)
      (EQ t |T_void|)
      )
    )
  )
; (New as of 12 Dec 2000)
; primitive types have no proper supertypes
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_boolean| t)
      )
    (IMPLIES 
      (<: |T_boolean| t)
      (EQ t |T_boolean|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_char| t)
      )
    (IMPLIES 
      (<: |T_char| t)
      (EQ t |T_char|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_byte| t)
      )
    (IMPLIES 
      (<: |T_byte| t)
      (EQ t |T_byte|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_short| t)
      )
    (IMPLIES 
      (<: |T_short| t)
      (EQ t |T_short|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_int| t)
      )
    (IMPLIES 
      (<: |T_int| t)
      (EQ t |T_int|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_long| t)
      )
    (IMPLIES 
      (<: |T_long| t)
      (EQ t |T_long|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_float| t)
      )
    (IMPLIES 
      (<: |T_float| t)
      (EQ t |T_float|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_double| t)
      )
    (IMPLIES 
      (<: |T_double| t)
      (EQ t |T_double|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_bigint| t)
      )
    (IMPLIES 
      (<: |T_bigint| t)
      (EQ t |T_bigint|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_real| t)
      )
    (IMPLIES 
      (<: |T_real| t)
      (EQ t |T_real|)
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (t)
    (PATS 
      (<: |T_void| t)
      )
    (IMPLIES 
      (<: |T_void| t)
      (EQ t |T_void|)
      )
    )
  )
; === ESCJ 8: Section 1.2
(BG_PUSH
  (FORALL 
    (t0 t1 t2)
    (PATS 
      (<: t0 
        (asChild t1 t2)
        )
      )
    (IMPLIES
      (<: t0 
        (asChild t1 t2)
        )
      (EQ 
        (classDown t2 t0)
        (asChild t1 t2)
        )
      )
    )
  )
; === ESCJ 8: Section 1.3
; new
(BG_PUSH 
  (<: |T_java.lang.Cloneable| |T_java.lang.Object|)
  )
(BG_PUSH
  (FORALL 
    (t)
    (PATS 
      (|_array| t)
      )
    (<: 
      (|_array| t)
      |T_java.lang.Cloneable|)
    )
  )
(BG_PUSH
  (FORALL 
    (t)
    (PATS 
      (elemtype 
        (|_array| t)
        )
      )
    (EQ 
      (elemtype 
        (|_array| t)
        )
      t)
    )
  )
(BG_PUSH
  (FORALL 
    (t0 t1)
    (PATS 
      (<: t0 
        (|_array| t1)
        )
      )
    (IFF 
      (<: t0 
        (|_array| t1)
        )
      (AND
        (EQ t0 
          (|_array| 
            (elemtype t0)
            )
          )
        (<: 
          (elemtype t0)
          t1)
        )
      )
    )
  )
; === ESCJ 8: Section 2.1
(DEFPRED 
  (is x t)
  )
(BG_PUSH
  (FORALL 
    (x t)
    (PATS 
      (cast x t)
      )
    (is 
      (cast x t)
      t)
    )
  )
(BG_PUSH
  (FORALL 
    (x t)
    (PATS 
      (cast x t)
      )
    (IMPLIES 
      (is x t)
      (EQ 
        (cast x t)
        x)
      )
    )
  )
; === ESCJ 8: Section 2.2
(BG_PUSH 
  (DISTINCT |bool$false| |@true|)
  )
; === ESCJ 8: Section 2.2.1
(BG_PUSH 
  (FORALL 
    (x)
    (PATS 
      (is x |T_char|)
      )
    (IFF 
      (is x |T_char|)
      (AND 
        (<= 0 x)
        (<= x 65535)
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (x)
    (PATS 
      (is x |T_byte|)
      )
    (IFF 
      (is x |T_byte|)
      (AND 
        (<= -128 x)
        (<= x 127)
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (x)
    (PATS 
      (is x |T_short|)
      )
    (IFF 
      (is x |T_short|)
      (AND 
        (<= -32768 x)
        (<= x 32767)
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (x)
    (PATS 
      (is x |T_int|)
      )
    (IFF 
      (is x |T_int|)
      (AND 
        (<= intFirst x)
        (<= x intLast)
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (x)
    (PATS 
      (is x |T_long|)
      )
    (IFF 
      (is x |T_long|)
      (AND 
        (<= longFirst x)
        (<= x longLast)
        )
      )
    )
  )
(BG_PUSH 
  (< longFirst intFirst)
  )
(BG_PUSH 
  (< intFirst -1000000)
  )
(BG_PUSH 
  (< 1000000 intLast)
  )
(BG_PUSH 
  (< intLast longLast)
  )
; == Defining bigint
(BG_PUSH 
  (EQ |T_bigint| |T_long|)
  )
; FIXME - change this eventually
; === Define typeof for primitive types - DRCok
; Removed because numeric values can be more than one type -
; e.g. is(0,|T_byte|) and is(0,|T_int|) are both true
; Thus these axioms introduce an inconsistency.
; Pointed out by Michal Moskal 2/2006.
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   (IFF (is x |T_int|) (EQ (typeof x) |T_int|))
;    ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_short|))
;	   (IFF (is x |T_short|) (EQ (typeof x) |T_short|))
;    ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_long|))
;	   (IFF (is x |T_long|) (EQ (typeof x) |T_long|))
;     ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_byte|))
;	   (IFF (is x |T_byte|) (EQ (typeof x) |T_byte|))
;     ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_char|))
;	   (IFF (is x |T_char|) (EQ (typeof x) |T_char|))
;     ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_boolean|))
;	   (IFF (is x |T_boolean|) (EQ (typeof x) |T_boolean|))
;     ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_double|))
;	   (IFF (is x |T_double|) (EQ (typeof x) |T_double|))
;     ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_float|))
;	   (IFF (is x |T_float|) (EQ (typeof x) |T_float|))
;     ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_real|))
;	   (IFF (is x |T_real|) (EQ (typeof x) |T_real|))
;     ))
;(BG_PUSH (FORALL (x) 
;	   (PATS (typeof x))
;	   ;(PATS (is x |T_bigint|))
;	   (IFF (is x |T_bigint|) (EQ (typeof x) |T_bigint|))
;     ))
;; Not sure why (or if) this should be here
(BG_PUSH 
  (FORALL 
    (x)
    (PATS 
      (typeof x)
      )
    ;(PATS (is x |T_void|))
(IFF 
      (is x |T_void|)
      (EQ 
        (typeof x)
        |T_void|)
      )
    )
  )
; === ESCJ 8: Section 2.3
(BG_PUSH
  (FORALL 
    (x t)
    (PATS 
      (MPAT 
        (<: t |T_java.lang.Object|)
        (is x t)
        )
      )
    (IMPLIES 
      (<: t |T_java.lang.Object|)
      (IFF 
        (is x t)
        (OR 
          (EQ x null)
          (<: 
            (typeof x)
            t)
          )
        )
      )
    )
  )
; === ESCJ 8: Section 2.4
(BG_PUSH
  (FORALL 
    (f t x)
    (PATS 
      (select 
        (asField f t)
        x)
      )
    (is 
      (select 
        (asField f t)
        x)
      t)
    )
  )
; === ESCJ 8: Section 2.5
(BG_PUSH
  (FORALL 
    (e a i)
    (PATS 
      (select 
        (select 
          (asElems e)
          a)
        i)
      )
    (is 
      (select 
        (select 
          (asElems e)
          a)
        i)
      (elemtype 
        (typeof a)
        )
      )
    )
  )
; === ESCJ 8: Section 3.0
(DEFPRED 
  (isAllocated x a0)
  (< 
    (vAllocTime x)
    a0)
  )
; === ESCJ 8: Section 3.1
(BG_PUSH
  (FORALL 
    (x f a0)
    (PATS 
      (isAllocated 
        (select f x)
        a0)
      )
    (IMPLIES 
      (AND 
        (< 
          (fClosedTime f)
          a0)
        (isAllocated x a0)
        )
      (isAllocated 
        (select f x)
        a0)
      )
    )
  )
; === ESCJ 8: Section 3.2
(BG_PUSH
  (FORALL 
    (a e i a0)
    (PATS 
      (isAllocated 
        (select 
          (select e a)
          i)
        a0)
      )
    (IMPLIES 
      (AND 
        (< 
          (eClosedTime e)
          a0)
        (isAllocated a a0)
        )
      (isAllocated 
        (select 
          (select e a)
          i)
        a0)
      )
    )
  )
; === ESCJ 8: Section 4 
; max(lockset) is in lockset
(BG_PUSH
  (FORALL 
    (S)
    (PATS 
      (select 
        (asLockSet S)
        (max 
          (asLockSet S)
          )
        )
      )
    (EQ
      (select 
        (asLockSet S)
        (max 
          (asLockSet S)
          )
        )
      |@true|)
    )
  )
; null is in lockset (not in ESCJ 8)
(BG_PUSH
  (FORALL 
    (S)
    (PATS 
      (asLockSet S)
      )
    (EQ 
      (select 
        (asLockSet S)
        null)
      |@true|)
    )
  )
(DEFPRED 
  (lockLE x y)
  (<= x y)
  )
(DEFPRED 
  (lockLT x y)
  (< x y)
  )
; all locks in lockset are below max(lockset) (not in ESCJ 8)
(BG_PUSH
  (FORALL 
    (S mu)
    (IMPLIES
      (EQ 
        (select 
          (asLockSet S)
          mu)
        |@true|)
      (lockLE mu 
        (max 
          (asLockSet S)
          )
        )
      )
    )
  )
; null precedes all objects in locking order (not in ESCJ 8)
(BG_PUSH
  (FORALL 
    (x)
    (PATS 
      (lockLE null x)
      (lockLT null x)
      (lockLE x null)
      (lockLT x null)
      )
    (IMPLIES
      (<: 
        (typeof x)
        |T_java.lang.Object|)
      (lockLE null x)
      )
    )
  )
; === ESCJ 8: Section 5.0
(BG_PUSH
  (FORALL 
    (a)
    (PATS 
      (arrayLength a)
      )
    (AND 
      (<= 0 
        (arrayLength a)
        )
      (is 
        (arrayLength a)
        |T_int|)
      )
    )
  )
(DEFPRED 
  (arrayFresh a a0 b0 e s T v)
  )
(BG_PUSH
  (FORALL 
    (a a0 b0 e n s T v)
    (PATS 
      (arrayFresh a a0 b0 e 
        (arrayShapeMore n s)
        T v)
      )
    (IFF
      (arrayFresh a a0 b0 e 
        (arrayShapeMore n s)
        T v)
      (AND
        (<= a0 
          (vAllocTime a)
          )
        (isAllocated a b0)
        (NEQ a null)
        (EQ 
          (typeof a)
          T)
        (EQ 
          (arrayLength a)
          n)
        (FORALL 
          (i)
          (PATS 
            (select 
              (select e a)
              i)
            )
          (AND
            (arrayFresh 
              (select 
                (select e a)
                i)
              a0 b0 e s 
              (elemtype T)
              v)
            (EQ 
              (arrayParent 
                (select 
                  (select e a)
                  i)
                )
              a)
            (EQ 
              (arrayPosition 
                (select 
                  (select e a)
                  i)
                )
              i)
            )
          )
        )
      )
    )
  )
(BG_PUSH
  (FORALL 
    (a a0 b0 e n T v)
    (PATS 
      (arrayFresh a a0 b0 e 
        (arrayShapeOne n)
        T v)
      )
    (IFF
      (arrayFresh a a0 b0 e 
        (arrayShapeOne n)
        T v)
      (AND
        (<= a0 
          (vAllocTime a)
          )
        (isAllocated a b0)
        (NEQ a null)
        (EQ 
          (typeof a)
          T)
        (EQ 
          (arrayLength a)
          n)
        (FORALL 
          (i)
          (PATS 
            (select 
              (select e a)
              i)
            )
          (AND
            (EQ 
              (select 
                (select e a)
                i)
              v)
            )
          )
        )
      )
    )
  )
(BG_PUSH
  (FORALL 
    (a0 b0 e s T v)
    (PATS 
      (arrayMake a0 b0 s T v)
      )
    (arrayFresh
      (arrayMake a0 b0 s T v)
      a0 b0 elems s T v )
    )
  )
(BG_PUSH
  (FORALL 
    (a0 b0 a1 b1 s1 s2 T1 T2 v)
    (PATS 
      (MPAT 
        (arrayMake a0 b0 s1 T1 v)
        (arrayMake a1 b1 s2 T2 v)
        )
      )
    (IMPLIES
      (EQ 
        (arrayMake a0 b0 s1 T1 v)
        (arrayMake a1 b1 s2 T2 v)
        )
      (AND 
        (EQ b0 b1)
        (EQ T1 T2)
        (EQ s1 s2)
        )
      )
    )
  )
; === code to ensure that (isNewArray x) ==> x has no invariants
; arrayType is distinct from all types with invariants (due to the
; generated type-distinctness axiom)
(BG_PUSH
  (EQ arrayType 
    (asChild arrayType |T_java.lang.Object|)
    )
  )
(BG_PUSH
  (FORALL 
    (t)
    (PATS 
      (|_array| t)
      )
    (<: 
      (|_array| t)
      arrayType)
    )
  )
(BG_PUSH
  (FORALL 
    (s)
    (PATS 
      (isNewArray s)
      )
    (IMPLIES 
      (EQ |@true| 
        (isNewArray s)
        )
      (<: 
        (typeof s)
        arrayType)
      )
    )
  )
; === ESCJ 8: Section 5.1
; integralMod is the computer mod - the sign of the result is the sign of the
; first operand; it is not the mathematical mod, whose result is always positive
; j != 0 ==> ((i/j)*j + (i%j) == i
(BG_PUSH
  (FORALL 
    (i j)
    (PATS 
      (integralDiv i j)
      )
    ;(FORALL (i j) (PATS (integralMod i j) (integralDiv i j))
(IMPLIES 
      (NOT 
        ( EQ j 0)
        )
      (EQ 
        (+ 
          (* 
            (integralDiv i j)
            j)
          (integralMod i j)
          )
        i)
      )
    )
  )
;; FIXME? - If the above has a trigger of (integralMod i j) and the axiom
;; below is also included, then we get some inconsistency and a failure of
;; test 72
; (i>=0 && j>0) ==> (i%j >= 0 && i%j < j)
(BG_PUSH
  (FORALL 
    (i j)
    (PATS 
      (integralMod i j)
      )
    (IMPLIES 
      (AND 
        (< 0 j)
        (<= 0 i)
        )
      (AND 
        (<= 0 
          (integralMod i j)
          )
        (< 
          (integralMod i j)
          j)
        )
      )
    )
  )
; (j != 0) ==> (0%j == 0)
(BG_PUSH
  (FORALL 
    (i j)
    (PATS 
      (integralMod i j)
      )
    (IMPLIES 
      (AND 
        (NOT 
          (EQ j 0)
          )
        (EQ i 0)
        )
      (EQ 0 
        (integralMod i j)
        )
      )
    )
  )
; (j != 0) ==> ((i>=0) ==> (i%j)>=0 ))
(BG_PUSH
  (FORALL 
    (i j)
    (PATS 
      (integralMod i j)
      )
    (IMPLIES 
      (NOT 
        (EQ j 0)
        )
      (IMPLIES 
        (<= 0 i)
        (<= 0 
          (integralMod i j)
          )
        )
      )
    )
  )
; (j != 0) ==> ((i<=0) ==> (i%j)<=0 ))
(BG_PUSH
  (FORALL 
    (i j)
    (PATS 
      (integralMod i j)
      )
    (IMPLIES 
      (NOT 
        (EQ j 0)
        )
      (IMPLIES 
        (<= i 0)
        (<= 
          (integralMod i j)
          0)
        )
      )
    )
  )
; Only true for mathMod
;(BG_PUSH
; (FORALL (i j) 
;	 (PATS (integralMod (+ i j) j))
;	 (EQ (integralMod (+ i j) j) 
;	     (integralMod i j))))
;
;(BG_PUSH
; (FORALL (i j)
;	 (PATS (integralMod (+ j i) j))
;	 (EQ (integralMod (+ j i) j) 
;	     (integralMod i j))))
; to prevent a matching loop
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (* 
        (integralDiv 
          (* x y)
          y)
        y)
      )
    (EQ 
      (* 
        (integralDiv 
          (* x y)
          y)
        y)
      (* x y)
      )
    )
  )
; === ESCJ 8: Section 5.2
(DEFPRED 
  (boolAnd a b)
  (AND
    (EQ a |@true|)
    (EQ b |@true|)
    )
  )
(DEFPRED 
  (boolEq a b)
  (IFF
    (EQ a |@true|)
    (EQ b |@true|)
    )
  )
(DEFPRED 
  (boolImplies a b)
  (IMPLIES
    (EQ a |@true|)
    (EQ b |@true|)
    )
  )
(DEFPRED 
  (boolNE a b)
  (NOT 
    (IFF
      (EQ a |@true|)
      (EQ b |@true|)
      )
    )
  )
(DEFPRED 
  (boolNot a)
  (NOT 
    (EQ a |@true|)
    )
  )
(DEFPRED 
  (boolOr a b)
  (OR
    (EQ a |@true|)
    (EQ b |@true|)
    )
  )
; Axioms related to Strings - DRCok
(DEFPRED 
  (|interned:| s)
  )
(BG_PUSH
  (FORALL 
    (i k)
    (PATS 
      (|intern:| i k)
      )
    (AND 
      (NEQ 
        (|intern:| i k)
        null)
      (EQ 
        (typeof 
          (|intern:| i k)
          )
        |T_java.lang.String|)
      (isAllocated 
        (|intern:| i k)
        alloc)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (s)
    (PATS 
      (|interned:| s)
      )
    (is 
      (|interned:| s)
      |T_boolean|)
    )
  )
(BG_PUSH
  (FORALL 
    (i ii k kk)
    (PATS 
      (MPAT 
        (|intern:| i k)
        (|intern:| ii kk)
        )
      )
    (IFF 
      (EQ 
        (|intern:| i k)
        (|intern:| ii kk)
        )
      (EQ i ii)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (i k)
    (PATS 
      (|intern:| i k)
      )
    (|interned:| 
      (|intern:| i k)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y a)
    (PATS 
      (stringCat x y a)
      )
    (AND 
      (NEQ 
        (stringCat x y a)
        null)
      (NOT 
        (isAllocated 
          (stringCat x y a)
          a)
        )
      (EQ 
        (typeof 
          (stringCat x y a)
          )
        |T_java.lang.String|)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y a b)
    (PATS 
      (MPAT 
        (stringCat x y a)
        (stringCat x y b)
        )
      )
    (IFF 
      (EQ 
        (stringCat x y a)
        (stringCat x y b)
        )
      (EQ a b)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (a b i j)
    (PATS 
      (MPAT 
        (next a i)
        (next b j)
        )
      )
    (IFF 
      (EQ 
        (next a i)
        (next b j)
        )
      (AND 
        (EQ a b)
        (EQ i j)
        )
      )
    )
  )
(BG_PUSH
  (FORALL 
    (a i)
    (PATS 
      (next a i)
      )
    (< a 
      (next a i)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y xx yy a b)
    (PATS 
      (MPAT 
        (stringCat x y a)
        (stringCat xx yy b)
        )
      )
    (IMPLIES
      (EQ 
        (stringCat x y a)
        (stringCat xx yy b)
        )
      (EQ a b)
      )
    )
  )
(DEFPRED 
  (stringCatP r x y a0 a1)
  )
(BG_PUSH
  (FORALL 
    (r x y a0 a1)
    (PATS 
      (stringCatP r x y a0 a1)
      )
    (IMPLIES 
      (stringCatP r x y a0 a1)
      (AND 
        (NEQ r null)
        (isAllocated r a1)
        (NOT 
          (isAllocated r a0)
          )
        (< a0 a1)
        (EQ 
          (typeof r)
          |T_java.lang.String|)
        )
      )
    )
  )
; Not in ESCJ8, but should be
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralEQ x y)
      )
    (IFF
      (EQ 
        (integralEQ x y)
        |@true|)
      (EQ x y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralGE x y)
      )
    (IFF
      (EQ 
        (integralGE x y)
        |@true|)
      (>= x y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralGT x y)
      )
    (IFF
      (EQ 
        (integralGT x y)
        |@true|)
      (> x y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralLE x y)
      )
    (IFF
      (EQ 
        (integralLE x y)
        |@true|)
      (<= x y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralLT x y)
      )
    (IFF
      (EQ 
        (integralLT x y)
        |@true|)
      (< x y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralNE x y)
      )
    (IFF
      (EQ 
        (integralNE x y)
        |@true|)
      (NEQ x y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (refEQ x y)
      )
    (IFF
      (EQ 
        (refEQ x y)
        |@true|)
      (EQ x y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (refNE x y)
      )
    (IFF
      (EQ 
        (refNE x y)
        |@true|)
      (NEQ x y)
      )
    )
  )
; === ESCJ 8: Section 5.3
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (termConditional |@true| x y)
      )
    (EQ 
      (termConditional |@true| x y)
      x)
    )
  )
(BG_PUSH
  (FORALL 
    (b x y)
    (PATS 
      (termConditional b x y)
      )
    (IMPLIES 
      (NEQ b |@true|)
      (EQ 
        (termConditional b x y)
        y)
      )
    )
  )
; === Implementation of nonnullelements; not in ESCJ 8 (yet?):
(DEFPRED 
  (nonnullelements x e)
  (AND 
    (NEQ x null)
    (FORALL 
      (i)
      (IMPLIES 
        (AND 
          (<= 0 i)
          (< i 
            (arrayLength x)
            )
          )
        (NEQ 
          (select 
            (select e x)
            i)
          null)
        )
      )
    )
  )
; === Axioms about classLiteral; not in ESCJ 8 (yet?):
(BG_PUSH
  (FORALL 
    (t)
    (PATS 
      (classLiteral t)
      )
    (AND 
      (NEQ 
        (classLiteral t)
        null)
      (is 
        (classLiteral t)
        |T_java.lang.Class|)
      (isAllocated 
        (classLiteral t)
        alloc)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (t)
    (PATS 
      (classLiteral t)
      )
    (EQ 
      (classLiteral t)
      t)
    )
  )
; === Axioms about properties of integral &, |, and /
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralAnd x y)
      )
    (IMPLIES
      (OR 
        (<= 0 x)
        (<= 0 y)
        )
      (<= 0 
        (integralAnd x y)
        )
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralAnd x y)
      )
    (IMPLIES
      (<= 0 x)
      (<= 
        (integralAnd x y)
        x)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralAnd x y)
      )
    (IMPLIES
      (<= 0 y)
      (<= 
        (integralAnd x y)
        y)
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralOr x y)
      )
    (IMPLIES
      (AND 
        (<= 0 x)
        (<= 0 y)
        )
      (AND 
        (<= x 
          (integralOr x y)
          )
        (<= y 
          (integralOr x y)
          )
        )
      )
    )
  )
; ((x >= 0) & (y > 0)) ==> (x/y >= 0 & x >= (x/y) )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralDiv x y)
      )
    (IMPLIES
      (AND 
        (<= 0 x)
        (< 0 y)
        )
      (AND 
        (<= 0 
          (integralDiv x y)
          )
        (<= 
          (integralDiv x y)
          x)
        )
      )
    )
  )
; ((x <= 0) & (y > 0)) ==> (x/y <= 0 & x <= x/y))
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralDiv x y)
      )
    (IMPLIES
      (AND 
        (<= x 0)
        (< 0 y)
        )
      (AND 
        (<= 
          (integralDiv x y)
          0)
        (<= x 
          (integralDiv x y)
          )
        )
      )
    )
  )
; ((x <= z) & (y > 0)) ==> (x/y <= z/y))
(BG_PUSH
  (FORALL 
    (x y z)
    (PATS 
      (MPAT 
        (integralDiv z y)
        (LE x z)
        )
      )
    (IMPLIES
      (AND 
        (<= x z)
        (< 0 y)
        )
      (<= 
        (integralDiv x y)
        (integralDiv z y)
        )
      )
    )
  )
; ( x >= 0 & y < 0) ==> (x/y)<=0
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralDiv x y)
      )
    (IMPLIES
      (AND 
        (<= 0 x)
        (< y 0)
        )
      (<= 
        (integralDiv x y)
        0)
      )
    )
  )
; ( x <= 0 & y < 0 ) ==> (x/y) >= 0
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralDiv x y)
      )
    (IMPLIES
      (AND 
        (<= x 0)
        (< y 0)
        )
      (<= 0 
        (integralDiv x y)
        )
      )
    )
  )
; (x <= 0 & y > 0) ==> (x/y) <= 0
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralDiv x y)
      )
    (IMPLIES
      (AND 
        (<= x 0)
        (< 0 y)
        )
      (<= 
        (integralDiv x y)
        0)
      )
    )
  )
; (x == 0 & y != 0) ==> (x/y)==0
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralDiv x y)
      )
    (IMPLIES
      (AND 
        (EQ 0 x)
        (NOT 
          (EQ 0 y)
          )
        )
      (EQ 0 
        (integralDiv x y)
        )
      )
    )
  )
(BG_PUSH
  (FORALL 
    (x y)
    (PATS 
      (integralXor x y)
      )
    (IMPLIES
      (AND 
        (<= 0 x)
        (<= 0 y)
        )
      (<= 0 
        (integralXor x y)
        )
      )
    )
  )
(BG_PUSH
  (FORALL 
    (n)
    (PATS 
      (intShiftL 1 n)
      )
    (IMPLIES
      (AND 
        (<= 0 n)
        (< n 31)
        )
      (<= 1 
        (intShiftL 1 n)
        )
      )
    )
  )
(BG_PUSH
  (FORALL 
    (n)
    (PATS 
      (longShiftL 1 n)
      )
    (IMPLIES
      (AND 
        (<= 0 n)
        (< n 63)
        )
      (<= 1 
        (longShiftL 1 n)
        )
      )
    )
  )
; === A few floating point axioms - DRCok
;; FIXME - floatingLT etc are predicates here, but are functions in ESC/java - is that a problem?
;; FIXME - have to include NaN and infinity
;; Order axioms
(BG_PUSH
  (FORALL 
    (d dd)
    (AND
      (OR
        (EQ |@true| 
          (floatingLT d dd)
          )
        (EQ |@true| 
          (floatingEQ d dd)
          )
        (EQ |@true| 
          (floatingGT d dd)
          )
        )
      (IFF 
        (EQ |@true| 
          (floatingLE d dd)
          )
        (OR 
          (EQ |@true| 
            (floatingEQ d dd)
            )
          (EQ |@true| 
            (floatingLT d dd)
            )
          )
        )
      (IFF 
        (EQ |@true| 
          (floatingGE d dd)
          )
        (OR 
          (EQ |@true| 
            (floatingEQ d dd)
            )
          (EQ |@true| 
            (floatingGT d dd)
            )
          )
        )
      (IFF 
        (EQ |@true| 
          (floatingLT d dd)
          )
        (EQ |@true| 
          (floatingGT dd d)
          )
        )
      (IFF 
        (EQ |@true| 
          (floatingLE d dd)
          )
        (EQ |@true| 
          (floatingGE dd d)
          )
        )
      (NOT 
        (IFF 
          (EQ |@true| 
            (floatingLT d dd)
            )
          (EQ |@true| 
            (floatingGE d dd)
            )
          )
        )
      (NOT 
        (IFF 
          (EQ |@true| 
            (floatingGT d dd)
            )
          (EQ |@true| 
            (floatingLE d dd)
            )
          )
        )
      )
    )
  )
;; floatingNE
(BG_PUSH 
  (FORALL 
    (d dd)
    (IFF 
      (EQ |@true| 
        (floatingEQ d dd)
        )
      (NOT 
        (EQ |@true| 
          (floatingNE d dd)
          )
        )
      )
    )
  )
;; floatADD
(BG_PUSH 
  (FORALL 
    (d dd)
    (IMPLIES 
      (EQ |@true| 
        (floatingGT d 
          (floatingNEG dd)
          )
        )
      (EQ |@true| 
        (floatingGT 
          (floatingADD d dd)
          |F_0.0|)
        )
      )
    )
  )
;; floatMUL
;;(BG_PUSH (FORALL (d dd) (AND
;;(IFF (OR (floatingEQ d |F_0.0|) (floatingEQ dd |F_0.0|)) (floatingEQ (floatingMUL d dd) |F_0.0|))
;;(IMPLIES (AND (floatingGT d |F_0.0|) (floatingGT dd |F_0.0|)) (floatingGT (floatingMUL d dd) |F_0.0|))
;;(IMPLIES (AND (floatingLT d |F_0.0|) (floatingLT dd |F_0.0|)) (floatingGT (floatingMUL d dd) |F_0.0|))
;;(IMPLIES (AND (floatingLT d |F_0.0|) (floatingGT dd |F_0.0|)) (floatingLT (floatingMUL d dd) |F_0.0|))
;;(IMPLIES (AND (floatingGT d |F_0.0|) (floatingLT dd |F_0.0|)) (floatingLT (floatingMUL d dd) |F_0.0|))
;;)))
;; floatingMOD
(BG_PUSH
  (FORALL 
    (d dd)
    (IMPLIES 
      (EQ |@true| 
        (floatingNE dd |F_0.0|)
        )
      (AND
        (IMPLIES 
          (EQ |@true| 
            (floatingGE d |F_0.0|)
            )
          (EQ |@true| 
            (floatingGE 
              (floatingMOD d dd)
              |F_0.0|)
            )
          )
        (IMPLIES 
          (EQ |@true| 
            (floatingLE d |F_0.0|)
            )
          (EQ |@true| 
            (floatingLE 
              (floatingMOD d dd)
              |F_0.0|)
            )
          )
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (d dd)
    (IMPLIES 
      (EQ |@true| 
        (floatingGT dd |F_0.0|)
        )
      (AND
        (EQ |@true| 
          (floatingGT 
            (floatingMOD d dd)
            (floatingNEG dd)
            )
          )
        (EQ |@true| 
          (floatingLT 
            (floatingMOD d dd)
            dd)
          )
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (d dd)
    (IMPLIES 
      (EQ |@true| 
        (floatingLT dd |F_0.0|)
        )
      (EQ |@true| 
        (floatingLT 
          (floatingMOD d dd)
          (floatingNEG dd)
          )
        )
      )
    )
  )
(BG_PUSH 
  (FORALL 
    (d dd)
    (IMPLIES 
      (EQ |@true| 
        (floatingLT dd |F_0.0|)
        )
      (EQ |@true| 
        (floatingGT 
          (floatingMOD d dd)
          dd)
        )
      )
    )
  )
; === Temporary kludge to speed up distinguishing small integers:
(BG_PUSH
  (DISTINCT -10 -9 -8 -7 -6 -5 -4 -3 -2 -1 0 1 2 3 4 5 6 7 8 9
    10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
    30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
    50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
    70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
    90 91 92 93 94 95 96 97 98 99
    100 101 102 103 104 105 106 107 108 109
    110 111 112 113 114 115 116 117 118 119
    120 121 122 123 124 125 126 127 128 129
    130 131 132 133 134 135 136 137 138 139
    140 141 142 143 144 145 146 147 148 149
    150 151 152 153 154 155 156 157 158 159
    160 161 162 163 164 165 166 167 168 169
    170 171 172 173 174 175 176 177 178 179
    180 181 182 183 184 185 186 187 188 189
    190 191 192 193 194 195 196 197 198 199
    200 201 202 203 204 205 206 207 208 209
    210 211 212 213 214 215 216 217 218 219
    220 221 222 223 224 225 226 227 228 229
    230 231 232 233 234 235 236 237 238 239
    240 241 242 243 244 245 246 247 248 249
    250 251 252 253 254 255 256 257 258 259
    260 261 262 263 264 265 266 267 268 269
    270 271 272 273 274 275 276 277 278 279
    280 281 282 283 284 285 286 287 288 289
    290 291 292 293 294 295 296 297 298 299
    300 301 302 303 304 305 306 307 308 309
    310 311 312 313 314 315 316 317 318 319
    320 321 322 323 324 325 326 327 328 329
    330 331 332 333 334 335 336 337 338 339
    340 341 342 343 344 345 346 347 348 349
    350 351 352 353 354 355 356 357 358 359
    360 361 362 363 364 365 366 367 368 369
    370 371 372 373 374 375 376 377 378 379
    380 381 382 383 384 385 386 387 388 389
    390 391 392 393 394 395 396 397 398 399)
  )
;----------------------------------------------------------------------
; End of Universal background predicate
;----------------------------------------------------------------------
(PROMPT_ON)
(BG_PUSH 
  (AND 
    (<: |T_java.lang.Exception| |T_java.lang.Throwable|)
    (EQ |T_java.lang.Exception| 
      (asChild |T_java.lang.Exception| |T_java.lang.Throwable|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Exception| t)
        )
      (IFF 
        (<: |T_java.lang.Exception| t)
        (OR 
          (EQ t |T_java.lang.Exception|)
          (<: |T_java.lang.Throwable| t)
          )
        )
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Object| t)
        )
      (IFF 
        (<: |T_java.lang.Object| t)
        (OR 
          (EQ t |T_java.lang.Object|)
          )
        )
      )
    (<: T_Pub |T_java.lang.Object|)
    (EQ T_Pub 
      (asChild T_Pub |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: T_Pub t)
        )
      (IFF 
        (<: T_Pub t)
        (OR 
          (EQ t T_Pub)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: |T_java.lang.Math| |T_java.lang.Object|)
    (EQ |T_java.lang.Math| 
      (asChild |T_java.lang.Math| |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: t |T_java.lang.Math|)
        )
      (IFF 
        (<: t |T_java.lang.Math|)
        (EQ t |T_java.lang.Math|)
        )
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Math| t)
        )
      (IFF 
        (<: |T_java.lang.Math| t)
        (OR 
          (EQ t |T_java.lang.Math|)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: |T_java.lang.Throwable| |T_java.lang.Object|)
    (EQ |T_java.lang.Throwable| 
      (asChild |T_java.lang.Throwable| |T_java.lang.Object|)
      )
    (<: |T_java.lang.Throwable| |T_java.io.Serializable|)
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Throwable| t)
        )
      (IFF 
        (<: |T_java.lang.Throwable| t)
        (OR 
          (EQ t |T_java.lang.Throwable|)
          (<: |T_java.lang.Object| t)
          (<: |T_java.io.Serializable| t)
          )
        )
      )
    (<: |T_java.io.Serializable| |T_java.lang.Object|)
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.io.Serializable| t)
        )
      (IFF 
        (<: |T_java.io.Serializable| t)
        (OR 
          (EQ t |T_java.io.Serializable|)
          (EQ t |T_java.lang.Object|)
          )
        )
      )
    (DISTINCT arrayType |T_boolean| |T_char| |T_byte| |T_short| |T_int| |T_long| |T_float| |T_double| |T_void| |T_.TYPE| |T_java.lang.Exception| |T_java.lang.Object| T_Pub |T_java.lang.Math| |T_java.lang.Throwable| |T_java.io.Serializable|)
    )
  )
(BG_POP)
(BG_PUSH 
  (AND 
    (<: |T_java.io.Serializable| |T_java.lang.Object|)
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.io.Serializable| t)
        )
      (IFF 
        (<: |T_java.io.Serializable| t)
        (OR 
          (EQ t |T_java.io.Serializable|)
          (EQ t |T_java.lang.Object|)
          )
        )
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Object| t)
        )
      (IFF 
        (<: |T_java.lang.Object| t)
        (OR 
          (EQ t |T_java.lang.Object|)
          )
        )
      )
    (<: |T_java.lang.Throwable| |T_java.lang.Object|)
    (EQ |T_java.lang.Throwable| 
      (asChild |T_java.lang.Throwable| |T_java.lang.Object|)
      )
    (<: |T_java.lang.Throwable| |T_java.io.Serializable|)
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Throwable| t)
        )
      (IFF 
        (<: |T_java.lang.Throwable| t)
        (OR 
          (EQ t |T_java.lang.Throwable|)
          (<: |T_java.lang.Object| t)
          (<: |T_java.io.Serializable| t)
          )
        )
      )
    (<: |T_java.lang.String| |T_java.lang.Object|)
    (EQ |T_java.lang.String| 
      (asChild |T_java.lang.String| |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: t |T_java.lang.String|)
        )
      (IFF 
        (<: t |T_java.lang.String|)
        (EQ t |T_java.lang.String|)
        )
      )
    (<: |T_java.lang.String| |T_java.io.Serializable|)
    (<: |T_java.lang.String| |T_java.lang.Comparable|)
    (<: |T_java.lang.String| |T_java.lang.CharSequence|)
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.String| t)
        )
      (IFF 
        (<: |T_java.lang.String| t)
        (OR 
          (EQ t |T_java.lang.String|)
          (<: |T_java.lang.Object| t)
          (<: |T_java.io.Serializable| t)
          (<: |T_java.lang.Comparable| t)
          (<: |T_java.lang.CharSequence| t)
          )
        )
      )
    (<: |T_java.lang.Exception| |T_java.lang.Throwable|)
    (EQ |T_java.lang.Exception| 
      (asChild |T_java.lang.Exception| |T_java.lang.Throwable|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Exception| t)
        )
      (IFF 
        (<: |T_java.lang.Exception| t)
        (OR 
          (EQ t |T_java.lang.Exception|)
          (<: |T_java.lang.Throwable| t)
          )
        )
      )
    (<: |T_java.lang.System| |T_java.lang.Object|)
    (EQ |T_java.lang.System| 
      (asChild |T_java.lang.System| |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: t |T_java.lang.System|)
        )
      (IFF 
        (<: t |T_java.lang.System|)
        (EQ t |T_java.lang.System|)
        )
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.System| t)
        )
      (IFF 
        (<: |T_java.lang.System| t)
        (OR 
          (EQ t |T_java.lang.System|)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: |T_java.lang.CharSequence| |T_java.lang.Object|)
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.CharSequence| t)
        )
      (IFF 
        (<: |T_java.lang.CharSequence| t)
        (OR 
          (EQ t |T_java.lang.CharSequence|)
          (EQ t |T_java.lang.Object|)
          )
        )
      )
    (<: |T_java.lang.Comparable| |T_java.lang.Object|)
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.lang.Comparable| t)
        )
      (IFF 
        (<: |T_java.lang.Comparable| t)
        (OR 
          (EQ t |T_java.lang.Comparable|)
          (EQ t |T_java.lang.Object|)
          )
        )
      )
    (<: T_Ex |T_java.lang.Object|)
    (EQ T_Ex 
      (asChild T_Ex |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: T_Ex t)
        )
      (IFF 
        (<: T_Ex t)
        (OR 
          (EQ t T_Ex)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: |T_java.io.OutputStream| |T_java.lang.Object|)
    (EQ |T_java.io.OutputStream| 
      (asChild |T_java.io.OutputStream| |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.io.OutputStream| t)
        )
      (IFF 
        (<: |T_java.io.OutputStream| t)
        (OR 
          (EQ t |T_java.io.OutputStream|)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: |T_java.io.PrintStream| |T_java.io.FilterOutputStream|)
    (EQ |T_java.io.PrintStream| 
      (asChild |T_java.io.PrintStream| |T_java.io.FilterOutputStream|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.io.PrintStream| t)
        )
      (IFF 
        (<: |T_java.io.PrintStream| t)
        (OR 
          (EQ t |T_java.io.PrintStream|)
          (<: |T_java.io.FilterOutputStream| t)
          )
        )
      )
    (<: |T_java.io.InputStream| |T_java.lang.Object|)
    (EQ |T_java.io.InputStream| 
      (asChild |T_java.io.InputStream| |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.io.InputStream| t)
        )
      (IFF 
        (<: |T_java.io.InputStream| t)
        (OR 
          (EQ t |T_java.io.InputStream|)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: T_Pub |T_java.lang.Object|)
    (EQ T_Pub 
      (asChild T_Pub |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: T_Pub t)
        )
      (IFF 
        (<: T_Pub t)
        (OR 
          (EQ t T_Pub)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: |T_org.jmlspecs.lang.JMLDataGroup| |T_java.lang.Object|)
    (EQ |T_org.jmlspecs.lang.JMLDataGroup| 
      (asChild |T_org.jmlspecs.lang.JMLDataGroup| |T_java.lang.Object|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: t |T_org.jmlspecs.lang.JMLDataGroup|)
        )
      (IFF 
        (<: t |T_org.jmlspecs.lang.JMLDataGroup|)
        (EQ t |T_org.jmlspecs.lang.JMLDataGroup|)
        )
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_org.jmlspecs.lang.JMLDataGroup| t)
        )
      (IFF 
        (<: |T_org.jmlspecs.lang.JMLDataGroup| t)
        (OR 
          (EQ t |T_org.jmlspecs.lang.JMLDataGroup|)
          (<: |T_java.lang.Object| t)
          )
        )
      )
    (<: |T_java.io.FilterOutputStream| |T_java.io.OutputStream|)
    (EQ |T_java.io.FilterOutputStream| 
      (asChild |T_java.io.FilterOutputStream| |T_java.io.OutputStream|)
      )
    (FORALL 
      (t)
      (PATS 
        (<: |T_java.io.FilterOutputStream| t)
        )
      (IFF 
        (<: |T_java.io.FilterOutputStream| t)
        (OR 
          (EQ t |T_java.io.FilterOutputStream|)
          (<: |T_java.io.OutputStream| t)
          )
        )
      )
    (DISTINCT arrayType |T_boolean| |T_char| |T_byte| |T_short| |T_int| |T_long| |T_float| |T_double| |T_void| |T_.TYPE| |T_java.io.Serializable| |T_java.lang.Object| |T_java.lang.Throwable| |T_java.lang.String| |T_java.lang.Exception| |T_java.lang.System| |T_java.lang.CharSequence| |T_java.lang.Comparable| T_Ex |T_java.io.OutputStream| |T_java.io.PrintStream| |T_java.io.InputStream| T_Pub |T_org.jmlspecs.lang.JMLDataGroup| |T_java.io.FilterOutputStream|)
    (EQ |@true| 
      (is |allowNullStreams:15.37.42| T_boolean)
      )
    (IFF 
      (EQ |@true| |allowNullStreams:15.37.42|)
      (EQ |@true| |bool$false|)
      )
    )
  )
(EXPLIES 
  (LBLNEG |vc.Ex.drink.20.2| 
    (IMPLIES 
      (AND 
        (EQ |out@pre:16..| |out:16..|)
        (EQ |@true| 
          (is |out:16..| |T_java.io.PrintStream|)
          )
        (EQ |@true| 
          (isAllocated |out:16..| alloc)
          )
        (NEQ |out:16..| null)
        (EQ |eol@pre:61.32.50| |eol:61.32.50|)
        (EQ |@true| 
          (is |eol:61.32.50| |T_java.lang.String|)
          )
        (EQ |@true| 
          (isAllocated |eol:61.32.50| alloc)
          )
        (NEQ |eol:61.32.50| null)
        (EQ |endsInNewLine@pre:61.31.29| |endsInNewLine:61.31.29|)
        (EQ |endsInNewLine:61.31.29| 
          (asField |endsInNewLine:61.31.29| T_boolean)
          )
        (EQ |output@pre:65.36.34| |output:65.36.34|)
        (EQ |output:65.36.34| 
          (asField |output:65.36.34| |T_org.jmlspecs.lang.JMLDataGroup|)
          )
        (< 
          (fClosedTime |output:65.36.34|)
          alloc)
        (EQ |in@pre:16..| |in:16..|)
        (EQ |@true| 
          (is |in:16..| |T_java.io.InputStream|)
          )
        (EQ |@true| 
          (isAllocated |in:16..| alloc)
          )
        (NEQ |in:16..| null)
        (EQ |allowNullStreams@pre:15.37.42| |allowNullStreams:15.37.42|)
        (EQ |@true| 
          (is |allowNullStreams:15.37.42| T_boolean)
          )
        (EQ |isOpen@pre:65.42.29| |isOpen:65.42.29|)
        (EQ |isOpen:65.42.29| 
          (asField |isOpen:65.42.29| T_boolean)
          )
        (EQ |outputText@pre:61.30.37| |outputText:61.30.37|)
        (EQ |outputText:61.30.37| 
          (asField |outputText:61.30.37| |T_java.lang.String|)
          )
        (< 
          (fClosedTime |outputText:61.30.37|)
          alloc)
        (FORALL 
          (s)
          (IMPLIES 
            (NEQ s null)
            (NEQ 
              (select |outputText:61.30.37| s)
              null)
            )
          )
        (EQ |readPosition@pre:86.47.29| |readPosition:86.47.29|)
        (EQ |readPosition:86.47.29| 
          (asField |readPosition:86.47.29| T_bigint)
          )
        (EQ |charArray@pre:35.29.46| |charArray:35.29.46|)
        (EQ |charArray:35.29.46| 
          (asField |charArray:35.29.46| 
            (|_array| T_char)
            )
          )
        (< 
          (fClosedTime |charArray:35.29.46|)
          alloc)
        (FORALL 
          (|s<1>|)
          (IMPLIES 
            (NEQ |s<1>| null)
            (NEQ 
              (select |charArray:35.29.46| |s<1>|)
              null)
            )
          )
        (EQ |availableBytes@pre:86.53.25| |availableBytes:86.53.25|)
        (EQ |availableBytes:86.53.25| 
          (asField |availableBytes:86.53.25| T_int)
          )
        (EQ |objectState@pre:4.35.43| |objectState:4.35.43|)
        (EQ |objectState:4.35.43| 
          (asField |objectState:4.35.43| |T_org.jmlspecs.lang.JMLDataGroup|)
          )
        (< 
          (fClosedTime |objectState:4.35.43|)
          alloc)
        (FORALL 
          (|s<2>|)
          (IMPLIES 
            (NEQ |s<2>| null)
            (NEQ 
              (select |objectState:4.35.43| |s<2>|)
              null)
            )
          )
        (EQ |inputBytes@pre:86.41.44| |inputBytes:86.41.44|)
        (EQ |inputBytes:86.41.44| 
          (asField |inputBytes:86.41.44| 
            (|_array| T_byte)
            )
          )
        (< 
          (fClosedTime |inputBytes:86.41.44|)
          alloc)
        (FORALL 
          (|s<3>|)
          (IMPLIES 
            (NEQ |s<3>| null)
            (NEQ 
              (select |inputBytes:86.41.44| |s<3>|)
              null)
            )
          )
        (EQ |wasClosed@pre:65.45.29| |wasClosed:65.45.29|)
        (EQ |wasClosed:65.45.29| 
          (asField |wasClosed:65.45.29| T_boolean)
          )
        (EQ |owner@pre:4.44.37| |owner:4.44.37|)
        (EQ |owner:4.44.37| 
          (asField |owner:4.44.37| |T_java.lang.Object|)
          )
        (< 
          (fClosedTime |owner:4.44.37|)
          alloc)
        (EQ |err@pre:16..| |err:16..|)
        (EQ |@true| 
          (is |err:16..| |T_java.io.PrintStream|)
          )
        (EQ |@true| 
          (isAllocated |err:16..| alloc)
          )
        (NEQ |err:16..| null)
        (EQ |streamState@pre:86.35.34| |streamState:86.35.34|)
        (EQ |streamState:86.35.34| 
          (asField |streamState:86.35.34| |T_org.jmlspecs.lang.JMLDataGroup|)
          )
        (< 
          (fClosedTime |streamState:86.35.34|)
          alloc)
        (EQ |outputBytes@pre:65.39.37| |outputBytes:65.39.37|)
        (EQ |outputBytes:65.39.37| 
          (asField |outputBytes:65.39.37| 
            (|_array| T_byte)
            )
          )
        (< 
          (fClosedTime |outputBytes:65.39.37|)
          alloc)
        (FORALL 
          (|s<4>|)
          (IMPLIES 
            (NEQ |s<4>| null)
            (NEQ 
              (select |outputBytes:65.39.37| |s<4>|)
              null)
            )
          )
        (EQ |length@pre:unknown| |length:unknown|)
        (EQ |length:unknown| 
          (asField |length:unknown| T_int)
          )
        (EQ |elems@pre| elems)
        (EQ elems 
          (asElems elems)
          )
        (< 
          (eClosedTime elems)
          alloc)
        (EQ LS 
          (asLockSet LS)
          )
        (EQ |alloc@pre| alloc)
        (EQ |state@pre| state)
        )
      (NOT 
        (AND 
          (EQ |@true| 
            (is this T_Ex)
            )
          (EQ |@true| 
            (isAllocated this alloc)
            )
          (NEQ this null)
          (EQ |@true| 
            (is |pubs:22.25| 
              (|_array| T_Pub)
              )
            )
          (EQ |@true| 
            (isAllocated |pubs:22.25| alloc)
            )
          (LBLNEG |Pre:0.20.6| 
            (AND 
              (EQ |@true| 
                (is this T_Ex)
                )
              (NEQ this null)
              )
            )
          (LBLNEG |Pre:0.20.6| 
            (EQ |@true| 
              (nonnullelements |pubs:22.25| elems)
              )
            )
          (IMPLIES 
            (NOT 
              (EQ |@true| |allowNullStreams:15.37.42|)
              )
            (NEQ |err:16..| null)
            )
          (FORALL 
            (brokenObj)
            (NOPATS 
              (is brokenObj |T_java.io.InputStream|)
              (NEQ brokenObj null)
              )
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is brokenObj |T_java.io.InputStream|)
                  )
                (NEQ brokenObj null)
                )
              (>= 
                (select |readPosition:86.47.29| brokenObj)
                0)
              )
            )
          (FORALL 
            (|brokenObj<1>|)
            (NOPATS 
              (is |brokenObj<1>| |T_java.io.InputStream|)
              (NEQ |brokenObj<1>| null)
              )
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |brokenObj<1>| |T_java.io.InputStream|)
                  )
                (NEQ |brokenObj<1>| null)
                )
              (<= 
                (+ 
                  (select |readPosition:86.47.29| |brokenObj<1>|)
                  (select |availableBytes:86.53.25| |brokenObj<1>|)
                  )
                (arrayLength 
                  (select |inputBytes:86.41.44| |brokenObj<1>|)
                  )
                )
              )
            )
          (FORALL 
            (|brokenObj<2>|)
            (NOPATS 
              (is |brokenObj<2>| |T_java.io.OutputStream|)
              (NEQ |brokenObj<2>| null)
              )
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |brokenObj<2>| |T_java.io.OutputStream|)
                  )
                (NEQ |brokenObj<2>| null)
                (EQ |@true| 
                  (select |isOpen:65.42.29| |brokenObj<2>|)
                  )
                )
              (NOT 
                (EQ |@true| 
                  (select |wasClosed:65.45.29| |brokenObj<2>|)
                  )
                )
              )
            )
          (FORALL 
            (|brokenObj<3>|)
            (NOPATS 
              (is |brokenObj<3>| |T_java.io.InputStream|)
              (NEQ |brokenObj<3>| null)
              )
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |brokenObj<3>| |T_java.io.InputStream|)
                  )
                (NEQ |brokenObj<3>| null)
                )
              (EQ 
                (select |owner:4.44.37| 
                  (select |inputBytes:86.41.44| |brokenObj<3>|)
                  )
                |brokenObj<3>|)
              )
            )
          (FORALL 
            (|brokenObj<4>|)
            (NOPATS 
              (is |brokenObj<4>| |T_java.io.OutputStream|)
              (NEQ |brokenObj<4>| null)
              )
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |brokenObj<4>| |T_java.io.OutputStream|)
                  )
                (NEQ |brokenObj<4>| null)
                (EQ |@true| 
                  (select |wasClosed:65.45.29| |brokenObj<4>|)
                  )
                )
              (NOT 
                (EQ |@true| 
                  (select |isOpen:65.42.29| |brokenObj<4>|)
                  )
                )
              )
            )
          (FORALL 
            (|brokenObj<5>|)
            (NOPATS 
              (is |brokenObj<5>| |T_java.io.InputStream|)
              (NEQ |brokenObj<5>| null)
              )
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |brokenObj<5>| |T_java.io.InputStream|)
                  )
                (NEQ |brokenObj<5>| null)
                )
              (>= 
                (select |availableBytes:86.53.25| |brokenObj<5>|)
                0)
              )
            )
          (IMPLIES 
            (NOT 
              (EQ |@true| |allowNullStreams:15.37.42|)
              )
            (NEQ |in:16..| null)
            )
          (FORALL 
            (|brokenObj<6>|)
            (NOPATS 
              (is |brokenObj<6>| |T_java.lang.CharSequence|)
              (NEQ |brokenObj<6>| null)
              )
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |brokenObj<6>| |T_java.lang.CharSequence|)
                  )
                (NEQ |brokenObj<6>| null)
                )
              (EQ 
                (select |owner:4.44.37| 
                  (select |charArray:35.29.46| |brokenObj<6>|)
                  )
                |brokenObj<6>|)
              )
            )
          (IMPLIES 
            (NOT 
              (EQ |@true| |allowNullStreams:15.37.42|)
              )
            (NEQ |out:16..| null)
            )
          (FORALL 
            (|brokenObj<7>|)
            (EQ 
              (|java.lang.Throwable#_stackTrace| state |brokenObj<7>|)
              (|getStackTrace##state| state |brokenObj<7>|)
              )
            )
          (FORALL 
            (|s:30.282.30| |ss:30.282.32|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |s:30.282.30| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |s:30.282.30| alloc)
                  )
                (NEQ |s:30.282.30| null)
                (EQ |@true| 
                  (is |ss:30.282.32| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |ss:30.282.32| alloc)
                  )
                (NEQ |ss:30.282.32| null)
                (EQ |@true| 
                  ( |equals##state#java.lang.Object| state |s:30.282.30| |ss:30.282.32| )
                  )
                )
              (EQ 
                (|length##state| state |s:30.282.30|)
                (|length##state| state |ss:30.282.32|)
                )
              )
            )
          (FORALL 
            (|s:30.396.30| |ss:30.396.32|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |s:30.396.30| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |s:30.396.30| alloc)
                  )
                (NEQ |s:30.396.30| null)
                (EQ |@true| 
                  (is |ss:30.396.32| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |ss:30.396.32| alloc)
                  )
                (NEQ |ss:30.396.32| null)
                (EQ |@true| 
                  ( |java.lang.String.equals.393.28| |s:30.396.30| |ss:30.396.32| )
                  )
                )
              (EQ 
                (|length##state| state |s:30.396.30|)
                (|length##state| state |ss:30.396.32|)
                )
              )
            )
          (FORALL 
            (|s:30.398.30| |ss:30.398.32|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |s:30.398.30| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |s:30.398.30| alloc)
                  )
                (NEQ |s:30.398.30| null)
                (EQ |@true| 
                  (is |ss:30.398.32| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |ss:30.398.32| alloc)
                  )
                (NEQ |ss:30.398.32| null)
                (EQ |@true| 
                  ( |java.lang.String.equals.393.28| |s:30.398.30| |ss:30.398.32| )
                  )
                )
              (EQ |@true| 
                ( |java.lang.String.equals.393.28| |ss:30.398.32| |s:30.398.30| )
                )
              )
            )
          (FORALL 
            (|s1:30.400.30| |s2:30.400.33| |s3:30.400.36|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |s1:30.400.30| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |s1:30.400.30| alloc)
                  )
                (NEQ |s1:30.400.30| null)
                (EQ |@true| 
                  (is |s2:30.400.33| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |s2:30.400.33| alloc)
                  )
                (NEQ |s2:30.400.33| null)
                (EQ |@true| 
                  (is |s3:30.400.36| |T_java.lang.String|)
                  )
                (EQ |@true| 
                  (isAllocated |s3:30.400.36| alloc)
                  )
                (NEQ |s3:30.400.36| null)
                (EQ |@true| 
                  ( |java.lang.String.equals.393.28| |s1:30.400.30| |s2:30.400.33| )
                  )
                )
              (IFF 
                (EQ |@true| 
                  ( |java.lang.String.equals.393.28| |s1:30.400.30| |s3:30.400.36| )
                  )
                (EQ |@true| 
                  ( |java.lang.String.equals.393.28| |s2:30.400.33| |s3:30.400.36| )
                  )
                )
              )
            )
          (FORALL 
            (|s1:30.512.30| |s2:30.512.34|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |s1:30.512.30| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |s1:30.512.30| alloc)
                  )
                (NEQ |s1:30.512.30| null)
                (EQ |@true| 
                  (is |s2:30.512.34| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |s2:30.512.34| alloc)
                  )
                (NEQ |s2:30.512.34| null)
                (NEQ |s1:30.512.30| null)
                (NEQ |s2:30.512.34| null)
                (NOT 
                  (EQ |@true| 
                    ( |java.lang.CharSequence.equal.41.33| state |s1:30.512.30| |s2:30.512.34| )
                    )
                  )
                )
              (IFF 
                (EQ |@true| 
                  ( |java.lang.String.lessThan.479.29| state |s1:30.512.30| |s2:30.512.34| )
                  )
                (NOT 
                  (EQ |@true| 
                    ( |java.lang.String.lessThan.479.29| state |s2:30.512.34| |s1:30.512.30| )
                    )
                  )
                )
              )
            )
          (FORALL 
            (|i:30.1097.28| |k:30.1097.30|)
            (EQ 
              (|java.lang.String.length.272.33| 
                (|intern:| |i:30.1097.28| |k:30.1097.30|)
                )
              |k:30.1097.30|)
            )
          (FORALL 
            (|brokenObj<8>|)
            (EQ 
              (|java.lang.Throwable#_stackTrace| state |brokenObj<8>|)
              (|getStackTrace##state| state |brokenObj<8>|)
              )
            )
          (FORALL 
            (|a:35.52.30|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |a:35.52.30| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |a:35.52.30| alloc)
                  )
                (NEQ |a:35.52.30| null)
                )
              (EQ |@true| 
                ( |java.lang.CharSequence.equal.41.33| state |a:35.52.30| |a:35.52.30| )
                )
              )
            )
          (FORALL 
            (|a:35.53.30| |b:35.53.32|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |a:35.53.30| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |a:35.53.30| alloc)
                  )
                (NEQ |a:35.53.30| null)
                (EQ |@true| 
                  (is |b:35.53.32| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |b:35.53.32| alloc)
                  )
                (NEQ |b:35.53.32| null)
                )
              (IFF 
                (EQ |@true| 
                  ( |java.lang.CharSequence.equal.41.33| state |a:35.53.30| |b:35.53.32| )
                  )
                (EQ |@true| 
                  ( |java.lang.CharSequence.equal.41.33| state |b:35.53.32| |a:35.53.30| )
                  )
                )
              )
            )
          (FORALL 
            (|a:35.54.30| |b:35.54.32| |c:35.54.34|)
            (IMPLIES 
              (AND 
                (EQ |@true| 
                  (is |a:35.54.30| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |a:35.54.30| alloc)
                  )
                (NEQ |a:35.54.30| null)
                (EQ |@true| 
                  (is |b:35.54.32| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |b:35.54.32| alloc)
                  )
                (NEQ |b:35.54.32| null)
                (EQ |@true| 
                  (is |c:35.54.34| 
                    (|_array| T_char)
                    )
                  )
                (EQ |@true| 
                  (isAllocated |c:35.54.34| alloc)
                  )
                (NEQ |c:35.54.34| null)
                (EQ |@true| 
                  ( |java.lang.CharSequence.equal.41.33| state |a:35.54.30| |b:35.54.32| )
                  )
                (EQ |@true| 
                  ( |java.lang.CharSequence.equal.41.33| state |b:35.54.32| |c:35.54.34| )
                  )
                )
              (EQ |@true| 
                ( |java.lang.CharSequence.equal.41.33| state |a:35.54.30| |c:35.54.34| )
                )
              )
            )
          (FORALL 
            (|brokenObj<9>|)
            (EQ 
              (|java.io.FilterOutputStream#underlyingStream| state |brokenObj<9>|)
              (select |out:64..| |brokenObj<9>|)
              )
            )
          (FORALL 
            (|brokenObj<10>|)
            (IFF 
              (EQ |@true| 
                ( |java.io.InputStream#wasClosed| state |brokenObj<10>| )
                )
              (NOT 
                (EQ |@true| 
                  (select |isOpen:86.54.29| |brokenObj<10>|)
                  )
                )
              )
            )
          (FORALL 
            (|brokenObj<11>|)
            (EQ 
              (|java.io.FilterOutputStream#underlyingStream| state |brokenObj<11>|)
              (select |out:64..| |brokenObj<11>|)
              )
            )
          (OR 
            (NOT 
              (LBLNEG |Null@23.26| 
                (NEQ |pubs:22.25| null)
                )
              )
            (AND 
              (LBLNEG |Null@23.26| 
                (NEQ |pubs:22.25| null)
                )
              (OR 
                (NOT 
                  (LBLNEG |NegSize@23.21| 
                    (<= 0 
                      (arrayLength |pubs:22.25|)
                      )
                    )
                  )
                (AND 
                  (LBLNEG |NegSize@23.21| 
                    (<= 0 
                      (arrayLength |pubs:22.25|)
                      )
                    )
                  (EQ |@true| 
                    (arrayFresh |tmp0!new!int[]:23.14| alloc |alloc<1>| elems 
                      (arrayShapeOne 
                        (arrayLength |pubs:22.25|)
                        )
                      (|_array| T_int)
                      0)
                    )
                  (FORALL 
                    (o)
                    (IMPLIES 
                      (AND 
                        (NOT 
                          (EQ |@true| 
                            (isAllocated o alloc)
                            )
                          )
                        (EQ |@true| 
                          (isAllocated o |alloc<1>|)
                          )
                        )
                      (EQ |@true| 
                        (isNewArray o)
                        )
                      )
                    )
                  (OR 
                    (AND 
                      (EQ elems |elems@loopold|)
                      (EQ 0 |i@loopold:24.8|)
                      (EQ EC |EC@loopold|)
                      (EQ state |state@loopold|)
                      (OR 
                        (AND 
                          (LBLPOS |trace.LoopIter^0,25.4#0| 
                            (EQ |@true| |@true|)
                            )
                          (OR 
                            (NOT 
                              (LBLNEG |Null@25.24| 
                                (NEQ |pubs:22.25| null)
                                )
                              )
                            (AND 
                              (LBLNEG |Null@25.24| 
                                (NEQ |pubs:22.25| null)
                                )
                              (< 0 
                                (arrayLength |pubs:22.25|)
                                )
                              (OR 
                                (NOT 
                                  (LBLNEG |Null@26.17| 
                                    (NEQ |pubs:22.25| null)
                                    )
                                  )
                                (AND 
                                  (LBLNEG |Null@26.17| 
                                    (NEQ |pubs:22.25| null)
                                    )
                                  (OR 
                                    (NOT 
                                      (LBLNEG |IndexNegative@26.17| 
                                        (<= 0 0)
                                        )
                                      )
                                    (AND 
                                      (LBLNEG |IndexNegative@26.17| 
                                        (<= 0 0)
                                        )
                                      (OR 
                                        (NOT 
                                          (LBLNEG |IndexTooBig@26.17| 
                                            (< 0 
                                              (arrayLength |pubs:22.25|)
                                              )
                                            )
                                          )
                                        (AND 
                                          (LBLNEG |IndexTooBig@26.17| 
                                            (< 0 
                                              (arrayLength |pubs:22.25|)
                                              )
                                            )
                                          (EQ |tmp3-25.4#0:26.17| 
                                            (select 
                                              (select elems |pubs:22.25|)
                                              0)
                                            )
                                          (OR 
                                            (NOT 
                                              (LBLNEG |Null@26.20| 
                                                (NEQ |tmp3-25.4#0:26.17| null)
                                                )
                                              )
                                            (AND 
                                              (LBLNEG |Null@26.20| 
                                                (NEQ |tmp3-25.4#0:26.17| null)
                                                )
                                              (OR 
                                                (AND 
                                                  (EQ |x@26.21-25.4#0-26.21:12.25| 
                                                    (+ 0 1)
                                                    )
                                                  (NOT 
                                                    (AND 
                                                      (LBLNEG |Pre:0.10.6@26.28| 
                                                        (AND 
                                                          (EQ |@true| 
                                                            (is |tmp3-25.4#0:26.17| T_Pub)
                                                            )
                                                          (NEQ |tmp3-25.4#0:26.17| null)
                                                          )
                                                        )
                                                      (LBLNEG |Pre:0.10.6@26.28| 
                                                        (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                                        )
                                                      )
                                                    )
                                                  )
                                                (AND 
                                                  (EQ |x@26.21-25.4#0-26.21:12.25| 
                                                    (+ 0 1)
                                                    )
                                                  (OR 
                                                    (AND 
                                                      (EQ |@true| 
                                                        (is |tmp3-25.4#0:26.17| T_Pub)
                                                        )
                                                      (NEQ |tmp3-25.4#0:26.17| null)
                                                      (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                                      (EQ |state<1>| |after@26.21-25.4#0-26.21|)
                                                      )
                                                    (AND 
                                                      (NOT 
                                                        (AND 
                                                          (EQ |@true| 
                                                            (is |tmp3-25.4#0:26.17| T_Pub)
                                                            )
                                                          (NEQ |tmp3-25.4#0:26.17| null)
                                                          (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                                          )
                                                        )
                                                      (EQ |state<1>| state)
                                                      )
                                                    )
                                                  (OR 
                                                    (EQ |EC-25.4#0-26.21:26.21| |ecReturn|)
                                                    (AND 
                                                      (EQ |EC-25.4#0-26.21:26.21| |ecThrow|)
                                                      (<: 
                                                        (typeof |XRES-25.4#0-26.21:26.21|)
                                                        |T_java.lang.Exception|)
                                                      )
                                                    )
                                                  (EQ elems 
                                                    (asElems elems)
                                                    )
                                                  (< 
                                                    (eClosedTime elems)
                                                    |alloc<1>|)
                                                  (EQ |@true| 
                                                    (is |state-25.4#0-26.21:26.21| T_anytype)
                                                    )
                                                  (EQ |@true| 
                                                    (is |RES-25.4#0-26.21:26.21| T_int)
                                                    )
                                                  (IMPLIES 
                                                    (AND 
                                                      (EQ |EC-25.4#0-26.21:26.21| |ecReturn|)
                                                      (EQ |@true| 
                                                        (is |tmp3-25.4#0:26.17| T_Pub)
                                                        )
                                                      (NEQ |tmp3-25.4#0:26.17| null)
                                                      (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                                      )
                                                    (>= |RES-25.4#0-26.21:26.21| 0)
                                                    )
                                                  (IMPLIES 
                                                    (AND 
                                                      (EQ |EC-25.4#0-26.21:26.21| |ecThrow|)
                                                      (<: 
                                                        (typeof |XRES-25.4#0-26.21:26.21|)
                                                        |T_java.lang.Exception|)
                                                      )
                                                    (NOT 
                                                      (AND 
                                                        (EQ |@true| 
                                                          (is |tmp3-25.4#0:26.17| T_Pub)
                                                          )
                                                        (NEQ |tmp3-25.4#0:26.17| null)
                                                        (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                                        )
                                                      )
                                                    )
                                                  (OR 
                                                    (NOT 
                                                      (LBLNEG |Null@26.7| 
                                                        (NEQ |tmp0!new!int[]:23.14| null)
                                                        )
                                                      )
                                                    (AND 
                                                      (LBLNEG |Null@26.7| 
                                                        (NEQ |tmp0!new!int[]:23.14| null)
                                                        )
                                                      (OR 
                                                        (NOT 
                                                          (LBLNEG |IndexNegative@26.7| 
                                                            (<= 0 0)
                                                            )
                                                          )
                                                        (AND 
                                                          (LBLNEG |IndexNegative@26.7| 
                                                            (<= 0 0)
                                                            )
                                                          (NOT 
                                                            (LBLNEG |IndexTooBig@26.7| 
                                                              (< 0 
                                                                (arrayLength |tmp0!new!int[]:23.14|)
                                                                )
                                                              )
                                                            )
                                                          )
                                                        )
                                                      )
                                                    )
                                                  )
                                                )
                                              )
                                            )
                                          )
                                        )
                                      )
                                    )
                                  )
                                )
                              )
                            )
                          )
                        (AND 
                          (LBLPOS |trace.LoopIter^0,25.4#0| 
                            (EQ |@true| |@true|)
                            )
                          (LBLNEG |Null@25.24| 
                            (NEQ |pubs:22.25| null)
                            )
                          (< 0 
                            (arrayLength |pubs:22.25|)
                            )
                          (LBLNEG |Null@26.17| 
                            (NEQ |pubs:22.25| null)
                            )
                          (LBLNEG |IndexNegative@26.17| 
                            (<= 0 0)
                            )
                          (LBLNEG |IndexTooBig@26.17| 
                            (< 0 
                              (arrayLength |pubs:22.25|)
                              )
                            )
                          (EQ |tmp3-25.4#0:26.17| 
                            (select 
                              (select elems |pubs:22.25|)
                              0)
                            )
                          (LBLNEG |Null@26.20| 
                            (NEQ |tmp3-25.4#0:26.17| null)
                            )
                          (EQ |x@26.21-25.4#0-26.21:12.25| 
                            (+ 0 1)
                            )
                          (OR 
                            (AND 
                              (EQ |@true| 
                                (is |tmp3-25.4#0:26.17| T_Pub)
                                )
                              (NEQ |tmp3-25.4#0:26.17| null)
                              (>= |x@26.21-25.4#0-26.21:12.25| 0)
                              (EQ |state<1>| |after@26.21-25.4#0-26.21|)
                              )
                            (AND 
                              (NOT 
                                (AND 
                                  (EQ |@true| 
                                    (is |tmp3-25.4#0:26.17| T_Pub)
                                    )
                                  (NEQ |tmp3-25.4#0:26.17| null)
                                  (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                  )
                                )
                              (EQ |state<1>| state)
                              )
                            )
                          (OR 
                            (EQ |EC-25.4#0-26.21:26.21| |ecReturn|)
                            (AND 
                              (EQ |EC-25.4#0-26.21:26.21| |ecThrow|)
                              (<: 
                                (typeof |XRES-25.4#0-26.21:26.21|)
                                |T_java.lang.Exception|)
                              )
                            )
                          (EQ elems 
                            (asElems elems)
                            )
                          (< 
                            (eClosedTime elems)
                            |alloc<1>|)
                          (EQ |@true| 
                            (is |state-25.4#0-26.21:26.21| T_anytype)
                            )
                          (EQ |@true| 
                            (is |RES-25.4#0-26.21:26.21| T_int)
                            )
                          (IMPLIES 
                            (AND 
                              (EQ |EC-25.4#0-26.21:26.21| |ecReturn|)
                              (EQ |@true| 
                                (is |tmp3-25.4#0:26.17| T_Pub)
                                )
                              (NEQ |tmp3-25.4#0:26.17| null)
                              (>= |x@26.21-25.4#0-26.21:12.25| 0)
                              )
                            (>= |RES-25.4#0-26.21:26.21| 0)
                            )
                          (IMPLIES 
                            (AND 
                              (EQ |EC-25.4#0-26.21:26.21| |ecThrow|)
                              (<: 
                                (typeof |XRES-25.4#0-26.21:26.21|)
                                |T_java.lang.Exception|)
                              )
                            (NOT 
                              (AND 
                                (EQ |@true| 
                                  (is |tmp3-25.4#0:26.17| T_Pub)
                                  )
                                (NEQ |tmp3-25.4#0:26.17| null)
                                (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                )
                              )
                            )
                          (LBLNEG |Null@26.7| 
                            (NEQ |tmp0!new!int[]:23.14| null)
                            )
                          (LBLNEG |IndexNegative@26.7| 
                            (<= 0 0)
                            )
                          (LBLNEG |IndexTooBig@26.7| 
                            (< 0 
                              (arrayLength |tmp0!new!int[]:23.14|)
                              )
                            )
                          (EQ |elems-25.4#0| 
                            (store elems |tmp0!new!int[]:23.14| 
                              (store 
                                (select elems |tmp0!new!int[]:23.14|)
                                0 |RES-25.4#0-26.21:26.21|)
                              )
                            )
                          (EQ |i-25.4#0:25.35| 
                            (+ 0 1)
                            )
                          (LBLPOS |trace.LoopIter^1,25.4#1| 
                            (EQ |@true| |@true|)
                            )
                          (NOT 
                            (LBLNEG |Null@25.24| 
                              (NEQ |pubs:22.25| null)
                              )
                            )
                          )
                        )
                      )
                    (AND 
                      (EQ elems |elems@loopold|)
                      (EQ 0 |i@loopold:24.8|)
                      (EQ EC |EC@loopold|)
                      (EQ state |state@loopold|)
                      (OR 
                        (AND 
                          (LBLPOS |trace.LoopIter^0,25.4#0| 
                            (EQ |@true| |@true|)
                            )
                          (LBLNEG |Null@25.24| 
                            (NEQ |pubs:22.25| null)
                            )
                          (NOT 
                            (< 0 
                              (arrayLength |pubs:22.25|)
                              )
                            )
                          (EQ |i:24.8| 0)
                          (EQ RES |RES<1>|)
                          (EQ |elems<1>| elems)
                          (EQ |state<2>| state)
                          (EQ XRES |XRES<1>|)
                          )
                        (AND 
                          (LBLPOS |trace.LoopIter^0,25.4#0| 
                            (EQ |@true| |@true|)
                            )
                          (LBLNEG |Null@25.24| 
                            (NEQ |pubs:22.25| null)
                            )
                          (< 0 
                            (arrayLength |pubs:22.25|)
                            )
                          (LBLNEG |Null@26.17| 
                            (NEQ |pubs:22.25| null)
                            )
                          (LBLNEG |IndexNegative@26.17| 
                            (<= 0 0)
                            )
                          (LBLNEG |IndexTooBig@26.17| 
                            (< 0 
                              (arrayLength |pubs:22.25|)
                              )
                            )
                          (EQ |tmp3-25.4#0:26.17| 
                            (select 
                              (select elems |pubs:22.25|)
                              0)
                            )
                          (LBLNEG |Null@26.20| 
                            (NEQ |tmp3-25.4#0:26.17| null)
                            )
                          (EQ |x@26.21-25.4#0-26.21:12.25| 
                            (+ 0 1)
                            )
                          (OR 
                            (AND 
                              (EQ |@true| 
                                (is |tmp3-25.4#0:26.17| T_Pub)
                                )
                              (NEQ |tmp3-25.4#0:26.17| null)
                              (>= |x@26.21-25.4#0-26.21:12.25| 0)
                              (EQ |state<1>| |after@26.21-25.4#0-26.21|)
                              )
                            (AND 
                              (NOT 
                                (AND 
                                  (EQ |@true| 
                                    (is |tmp3-25.4#0:26.17| T_Pub)
                                    )
                                  (NEQ |tmp3-25.4#0:26.17| null)
                                  (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                  )
                                )
                              (EQ |state<1>| state)
                              )
                            )
                          (OR 
                            (EQ |EC-25.4#0-26.21:26.21| |ecReturn|)
                            (AND 
                              (EQ |EC-25.4#0-26.21:26.21| |ecThrow|)
                              (<: 
                                (typeof |XRES-25.4#0-26.21:26.21|)
                                |T_java.lang.Exception|)
                              )
                            )
                          (EQ elems 
                            (asElems elems)
                            )
                          (< 
                            (eClosedTime elems)
                            |alloc<1>|)
                          (EQ |@true| 
                            (is |state-25.4#0-26.21:26.21| T_anytype)
                            )
                          (EQ |@true| 
                            (is |RES-25.4#0-26.21:26.21| T_int)
                            )
                          (IMPLIES 
                            (AND 
                              (EQ |EC-25.4#0-26.21:26.21| |ecReturn|)
                              (EQ |@true| 
                                (is |tmp3-25.4#0:26.17| T_Pub)
                                )
                              (NEQ |tmp3-25.4#0:26.17| null)
                              (>= |x@26.21-25.4#0-26.21:12.25| 0)
                              )
                            (>= |RES-25.4#0-26.21:26.21| 0)
                            )
                          (IMPLIES 
                            (AND 
                              (EQ |EC-25.4#0-26.21:26.21| |ecThrow|)
                              (<: 
                                (typeof |XRES-25.4#0-26.21:26.21|)
                                |T_java.lang.Exception|)
                              )
                            (NOT 
                              (AND 
                                (EQ |@true| 
                                  (is |tmp3-25.4#0:26.17| T_Pub)
                                  )
                                (NEQ |tmp3-25.4#0:26.17| null)
                                (>= |x@26.21-25.4#0-26.21:12.25| 0)
                                )
                              )
                            )
                          (LBLNEG |Null@26.7| 
                            (NEQ |tmp0!new!int[]:23.14| null)
                            )
                          (LBLNEG |IndexNegative@26.7| 
                            (<= 0 0)
                            )
                          (LBLNEG |IndexTooBig@26.7| 
                            (< 0 
                              (arrayLength |tmp0!new!int[]:23.14|)
                              )
                            )
                          (EQ |elems-25.4#0| 
                            (store elems |tmp0!new!int[]:23.14| 
                              (store 
                                (select elems |tmp0!new!int[]:23.14|)
                                0 |RES-25.4#0-26.21:26.21|)
                              )
                            )
                          (EQ |i-25.4#0:25.35| 
                            (+ 0 1)
                            )
                          (LBLPOS |trace.LoopIter^1,25.4#1| 
                            (EQ |@true| |@true|)
                            )
                          (LBLNEG |Null@25.24| 
                            (NEQ |pubs:22.25| null)
                            )
                          (NOT 
                            (< |i-25.4#0:25.35| 
                              (arrayLength |pubs:22.25|)
                              )
                            )
                          (EQ |i:24.8| |i-25.4#0:25.35|)
                          (EQ RES |RES-25.4#0-26.21:26.21|)
                          (EQ |elems<1>| |elems-25.4#0|)
                          (EQ |state<2>| |state-25.4#0:26.11|)
                          (EQ XRES |XRES-25.4#0-26.21:26.21|)
                          )
                        )
                      (EQ |L_25.4| |L_25.4|)
                      (EQ |EC<1>| |L_25.4|)
                      (EQ |i:24.8<1>| |i:24.8|)
                      (EQ |RES<2>| RES)
                      (EQ |elems<2>| |elems<1>|)
                      (EQ |state<3>| |state<2>|)
                      (EQ |XRES<2>| XRES)
                      (OR 
                        (NOT 
                          (LBLNEG |Null@27.17| 
                            (NEQ |pubs:22.25| null)
                            )
                          )
                        (AND 
                          (LBLNEG |Null@27.17| 
                            (NEQ |pubs:22.25| null)
                            )
                          (EQ |i:27.9| 
                            (- 
                              (arrayLength |pubs:22.25|)
                              1)
                            )
                          (OR 
                            (AND 
                              (EQ |i:27.9| |i@loopold:24.8<1>|)
                              (EQ |EC<1>| |EC@loopold<1>|)
                              (OR 
                                (AND 
                                  (LBLPOS |trace.LoopIter^2,27.4#0| 
                                    (EQ |@true| |@true|)
                                    )
                                  (>= |i:27.9| 0)
                                  (OR 
                                    (NOT 
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      )
                                    (AND 
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      (OR 
                                        (NOT 
                                          (LBLNEG |IndexNegative@27.41| 
                                            (<= 0 |i:27.9|)
                                            )
                                          )
                                        (AND 
                                          (LBLNEG |IndexNegative@27.41| 
                                            (<= 0 |i:27.9|)
                                            )
                                          (NOT 
                                            (LBLNEG |IndexTooBig@27.41| 
                                              (< |i:27.9| 
                                                (arrayLength |tmp0!new!int[]:23.14|)
                                                )
                                              )
                                            )
                                          )
                                        )
                                      )
                                    )
                                  )
                                (AND 
                                  (LBLPOS |trace.LoopIter^2,27.4#0| 
                                    (EQ |@true| |@true|)
                                    )
                                  (OR 
                                    (AND 
                                      (>= |i:27.9| 0)
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      (LBLNEG |IndexNegative@27.41| 
                                        (<= 0 |i:27.9|)
                                        )
                                      (LBLNEG |IndexTooBig@27.41| 
                                        (< |i:27.9| 
                                          (arrayLength |tmp0!new!int[]:23.14|)
                                          )
                                        )
                                      (EQ |tmp4!cand-27.4#0:27.30| 
                                        (integralNE 
                                          (select 
                                            (select |elems<2>| |tmp0!new!int[]:23.14|)
                                            |i:27.9|)
                                          0)
                                        )
                                      (EQ |tmp4!cand:27.37| |tmp4!cand-27.4#0:27.30|)
                                      )
                                    (AND 
                                      (NOT 
                                        (>= |i:27.9| 0)
                                        )
                                      (LBLPOS |trace.FirstOpOnly^3,27.37| 
                                        (EQ |@true| |@true|)
                                        )
                                      (EQ |tmp4!cand:27.37| |bool$false|)
                                      )
                                    )
                                  (EQ |@true| |tmp4!cand:27.37|)
                                  (EQ |i-27.4#0:27.53| 
                                    (- |i:27.9| 1)
                                    )
                                  (LBLPOS |trace.LoopIter^4,27.4#1| 
                                    (EQ |@true| |@true|)
                                    )
                                  (>= |i-27.4#0:27.53| 0)
                                  (OR 
                                    (NOT 
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      )
                                    (AND 
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      (OR 
                                        (NOT 
                                          (LBLNEG |IndexNegative@27.41| 
                                            (<= 0 |i-27.4#0:27.53|)
                                            )
                                          )
                                        (AND 
                                          (LBLNEG |IndexNegative@27.41| 
                                            (<= 0 |i-27.4#0:27.53|)
                                            )
                                          (NOT 
                                            (LBLNEG |IndexTooBig@27.41| 
                                              (< |i-27.4#0:27.53| 
                                                (arrayLength |tmp0!new!int[]:23.14|)
                                                )
                                              )
                                            )
                                          )
                                        )
                                      )
                                    )
                                  )
                                )
                              )
                            (AND 
                              (EQ |i:27.9| |i@loopold:24.8<1>|)
                              (EQ |EC<1>| |EC@loopold<1>|)
                              (OR 
                                (AND 
                                  (LBLPOS |trace.LoopIter^2,27.4#0| 
                                    (EQ |@true| |@true|)
                                    )
                                  (OR 
                                    (AND 
                                      (>= |i:27.9| 0)
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      (LBLNEG |IndexNegative@27.41| 
                                        (<= 0 |i:27.9|)
                                        )
                                      (LBLNEG |IndexTooBig@27.41| 
                                        (< |i:27.9| 
                                          (arrayLength |tmp0!new!int[]:23.14|)
                                          )
                                        )
                                      (EQ |tmp4!cand-27.4#0:27.30| 
                                        (integralNE 
                                          (select 
                                            (select |elems<2>| |tmp0!new!int[]:23.14|)
                                            |i:27.9|)
                                          0)
                                        )
                                      (EQ |tmp4!cand:27.37| |tmp4!cand-27.4#0:27.30|)
                                      )
                                    (AND 
                                      (NOT 
                                        (>= |i:27.9| 0)
                                        )
                                      (LBLPOS |trace.FirstOpOnly^3,27.37| 
                                        (EQ |@true| |@true|)
                                        )
                                      (EQ |tmp4!cand:27.37| |bool$false|)
                                      )
                                    )
                                  (NOT 
                                    (EQ |@true| |tmp4!cand:27.37|)
                                    )
                                  (EQ |i:24.8<2>| |i:27.9|)
                                  )
                                (AND 
                                  (LBLPOS |trace.LoopIter^2,27.4#0| 
                                    (EQ |@true| |@true|)
                                    )
                                  (OR 
                                    (AND 
                                      (>= |i:27.9| 0)
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      (LBLNEG |IndexNegative@27.41| 
                                        (<= 0 |i:27.9|)
                                        )
                                      (LBLNEG |IndexTooBig@27.41| 
                                        (< |i:27.9| 
                                          (arrayLength |tmp0!new!int[]:23.14|)
                                          )
                                        )
                                      (EQ |tmp4!cand-27.4#0:27.30| 
                                        (integralNE 
                                          (select 
                                            (select |elems<2>| |tmp0!new!int[]:23.14|)
                                            |i:27.9|)
                                          0)
                                        )
                                      (EQ |tmp4!cand:27.37| |tmp4!cand-27.4#0:27.30|)
                                      )
                                    (AND 
                                      (NOT 
                                        (>= |i:27.9| 0)
                                        )
                                      (LBLPOS |trace.FirstOpOnly^3,27.37| 
                                        (EQ |@true| |@true|)
                                        )
                                      (EQ |tmp4!cand:27.37| |bool$false|)
                                      )
                                    )
                                  (EQ |@true| |tmp4!cand:27.37|)
                                  (EQ |i-27.4#0:27.53| 
                                    (- |i:27.9| 1)
                                    )
                                  (LBLPOS |trace.LoopIter^4,27.4#1| 
                                    (EQ |@true| |@true|)
                                    )
                                  (OR 
                                    (AND 
                                      (>= |i-27.4#0:27.53| 0)
                                      (LBLNEG |Null@27.41| 
                                        (NEQ |tmp0!new!int[]:23.14| null)
                                        )
                                      (LBLNEG |IndexNegative@27.41| 
                                        (<= 0 |i-27.4#0:27.53|)
                                        )
                                      (LBLNEG |IndexTooBig@27.41| 
                                        (< |i-27.4#0:27.53| 
                                          (arrayLength |tmp0!new!int[]:23.14|)
                                          )
                                        )
                                      (EQ |tmp4!cand-27.4#1:27.30| 
                                        (integralNE 
                                          (select 
                                            (select |elems<2>| |tmp0!new!int[]:23.14|)
                                            |i-27.4#0:27.53|)
                                          0)
                                        )
                                      (EQ |tmp4!cand:27.37<1>| |tmp4!cand-27.4#1:27.30|)
                                      )
                                    (AND 
                                      (NOT 
                                        (>= |i-27.4#0:27.53| 0)
                                        )
                                      (LBLPOS |trace.FirstOpOnly^5,27.37| 
                                        (EQ |@true| |@true|)
                                        )
                                      (EQ |tmp4!cand:27.37<1>| |bool$false|)
                                      )
                                    )
                                  (NOT 
                                    (EQ |@true| |tmp4!cand:27.37<1>|)
                                    )
                                  (EQ |i:24.8<2>| |i-27.4#0:27.53|)
                                  )
                                )
                              (EQ |L_27.4| |L_27.4|)
                              (EQ |EC<2>| |L_27.4|)
                              (EQ |i:24.8<3>| |i:24.8<2>|)
                              (OR 
                                (AND 
                                  (EQ |s@28.15-28.15:61.102.31| 
                                    (|intern:| |1| |30|)
                                    )
                                  (NOT 
                                    (LBLNEG |Pre:61.98.10@28.22| 
                                      (AND 
                                        (EQ |@true| 
                                          (is |out:16..| |T_java.io.PrintStream|)
                                          )
                                        (NEQ |out:16..| null)
                                        )
                                      )
                                    )
                                  )
                                (AND 
                                  (EQ |s@28.15-28.15:61.102.31| 
                                    (|intern:| |1| |30|)
                                    )
                                  (OR 
                                    (AND 
                                      (EQ |@true| 
                                        (is |out:16..| |T_java.io.PrintStream|)
                                        )
                                      (NEQ |out:16..| null)
                                      (EQ |outputText-28.15:61.99.19| 
                                        (store |outputText:61.30.37| |out:16..| |after@28.15-28.15:61.99.19|)
                                        )
                                      (EQ |endsInNewLine-28.15:61.99.31| 
                                        (store |endsInNewLine:61.31.29| |out:16..| |after@28.15-28.15:61.99.31|)
                                        )
                                      (EQ |endsInNewLine:61.31.29<1>| |endsInNewLine-28.15:61.99.31|)
                                      (EQ |outputText:61.30.37<1>| |outputText-28.15:61.99.19|)
                                      (EQ |state<4>| |after@28.15-28.15|)
                                      )
                                    (AND 
                                      (NOT 
                                        (AND 
                                          (EQ |@true| 
                                            (is |out:16..| |T_java.io.PrintStream|)
                                            )
                                          (NEQ |out:16..| null)
                                          )
                                        )
                                      (EQ |endsInNewLine:61.31.29<1>| |endsInNewLine:61.31.29|)
                                      (EQ |outputText:61.30.37<1>| |outputText:61.30.37|)
                                      (EQ |state<4>| |state<3>|)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (NEQ 
                                        (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                        null)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (PATS 
                                      (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                      )
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (NEQ 
                                        (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                        null)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (NEQ 
                                        (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                        null)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (PATS 
                                      (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                      )
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (NEQ 
                                        (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                        null)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (AND 
                                        (NEQ 
                                          (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                          null)
                                        (NOT 
                                          (EQ |@true| 
                                            (isAllocated 
                                              (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                              |alloc<1>|)
                                            )
                                          )
                                        )
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (PATS 
                                      (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                      )
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (AND 
                                        (NEQ 
                                          (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                          null)
                                        (NOT 
                                          (EQ |@true| 
                                            (isAllocated 
                                              (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                              |alloc<1>|)
                                            )
                                          )
                                        )
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (NOT 
                                        (EQ |@true| 
                                          ( |java.lang.String.isInterned.1095.33| 
                                            (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                            )
                                          )
                                        )
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (PATS 
                                      (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                      )
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (NOT 
                                        (EQ |@true| 
                                          ( |java.lang.String.isInterned.1095.33| 
                                            (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                            )
                                          )
                                        )
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (EQ |@true| 
                                        ( |equals##state#java.lang.Object| |state-28.15:28.15| 
                                          (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                          (|java.lang.String.concat.820.40| 
                                            (|java.lang.String.nonnull.827.42| |s:30.839.62|)
                                            (|java.lang.String.nonnull.827.42| |ss:30.839.72|)
                                            )
                                          )
                                        )
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (PATS 
                                      (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                      )
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (EQ |@true| |bool$false|)
                                            )
                                          )
                                        )
                                      (EQ |@true| 
                                        ( |equals##state#java.lang.Object| |state-28.15:28.15| 
                                          (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                          (|java.lang.String.concat.820.40| 
                                            (|java.lang.String.nonnull.827.42| |s:30.839.62|)
                                            (|java.lang.String.nonnull.827.42| |ss:30.839.72|)
                                            )
                                          )
                                        )
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (EQ |@true| 
                                      (is 
                                        (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                        |T_java.lang.String|)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.839.62| |ss:30.839.72|)
                                    (PATS 
                                      (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                      )
                                    (EQ |@true| 
                                      (is 
                                        (|java.lang.String._infixConcat_.838.42| |s:30.839.62| |ss:30.839.72|)
                                        |T_java.lang.String|)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.820.61| |ss:30.820.71|)
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (NOT 
                                              (AND 
                                                (NEQ |s:30.820.61| null)
                                                (NEQ |ss:30.820.71| null)
                                                )
                                              )
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (NOT 
                                              (AND 
                                                (NEQ |s:30.820.61| null)
                                                (NEQ |ss:30.820.71| null)
                                                )
                                              )
                                            )
                                          )
                                        (NEQ |s:30.820.61| null)
                                        (NEQ |ss:30.820.71| null)
                                        )
                                      (NEQ 
                                        (|java.lang.String.concat.820.40| |s:30.820.61| |ss:30.820.71|)
                                        null)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.820.61| |ss:30.820.71|)
                                    (PATS 
                                      (|java.lang.String.concat.820.40| |s:30.820.61| |ss:30.820.71|)
                                      )
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (NOT 
                                              (AND 
                                                (NEQ |s:30.820.61| null)
                                                (NEQ |ss:30.820.71| null)
                                                )
                                              )
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (NOT 
                                              (AND 
                                                (NEQ |s:30.820.61| null)
                                                (NEQ |ss:30.820.71| null)
                                                )
                                              )
                                            )
                                          )
                                        (NEQ |s:30.820.61| null)
                                        (NEQ |ss:30.820.71| null)
                                        )
                                      (NEQ 
                                        (|java.lang.String.concat.820.40| |s:30.820.61| |ss:30.820.71|)
                                        null)
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.820.61| |ss:30.820.71|)
                                    (IMPLIES 
                                      (AND 
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (NOT 
                                              (AND 
                                                (NEQ |s:30.820.61| null)
                                                (NEQ |ss:30.820.71| null)
                                                )
                                              )
                                            )
                                          )
                                        (NOT 
                                          (AND 
                                            (EQ |@true| |@true|)
                                            (NOT 
                                              (AND 
                                                (NEQ |s:30.820.61| null)
                                                (NEQ |ss:30.820.71| null)
                                                )
                                              )
                                            )
                                          )
                                        (NEQ |s:30.820.61| null)
                                        (NEQ |ss:30.820.71| null)
                                        )
                                      (EQ |@true| 
                                        ( |java.lang.CharSequence.equal.49.33| |state-28.15:28.15| 
                                          (select |charArray:35.29.46| 
                                            (|java.lang.String.concat.820.40| |s:30.820.61| |ss:30.820.71|)
                                            )
                                          0 
                                          (select |charArray:35.29.46| |s:30.820.61|)
                                          0 
                                          (|length##state| |state-28.15:28.15| |s:30.820.61|)
                                          )
                                        )
                                      )
                                    )
                                  (FORALL 
                                    (|s:30.820.61| |ss:30.820.71|)
                                    (PATS 
                                      (|java.lang.String.concat.820.40| |s:30.820.61| |ss:30.820.71|)
                                      )
                                    (IMPLIES 
                                      (AND