(NAME_PREFIX Examples.esc2.invalid)
(BG_PUSH
 (AND
  (< 1000000 |INTEGER.LAST|)
  (< |INTEGER.FIRST| -1000000)
  (DISTINCT |MUTEX.TYPECODE| |TEXT.TYPECODE| |REFANY.TYPECODE| |ROOT.TYPECODE| |NULL.TYPECODE|)
  (DISTINCT RETURN EXIT)
  (EQ (|Is$INTEGER| |Test11.g| |@DUMMY|) |@true|)
  (FORALL (map) (PATS (|Is$TYPE@24| map |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@24| map |@DUMMY|) |@true|) (FORALL (start num map2) (PATS (storeSub map start num map2)) (IMPLIES (EQ (|Is$TYPE@24| map2 |@DUMMY|) |@true|) (EQ (|Is$TYPE@24| (storeSub map start num map2) |@DUMMY|) |@true|)))))
  (FORALL (|map$1|) (PATS (|Is$TYPE@24| |map$1| |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@24| |map$1| |@DUMMY|) |@true|) (FORALL (ind val) (PATS (store |map$1| ind val)) (IMPLIES (EQ (|Is$INTEGER| ind |@DUMMY|) |@true|) (EQ (|Is$TYPE@24| (store |map$1| ind val) |@DUMMY|) |@true|)))))
  (FORALL (|@q| |@dummy1|) (IMPLIES (EQ (|Is$TYPE@24| |@q| |@dummy1|) |@true|) (FORALL (|@i|) (EQ (|Is$INTEGER| (select |@q| |@i| |@ARRAY|) |@dummy1|) |@true|))))
  (FORALL (|@q$1| |@dummy1$1|) (IMPLIES (EQ (|Is$TYPE@24| |@q$1| |@dummy1$1|) |@true|) (EQ (NUMBER (ADDR |@q$1|) 0) 4)))
  (FORALL (|@q$2| |@dummy|) (IMPLIES (EQ (|Is$TYPE@21| |@q$2| |@dummy|) |@true|) (EQ (|Is$ORDINAL| |@q$2| |@DUMMY|) |@true|)))
  (FORALL (|@q$3| |@dummy$1|) (IMPLIES (EQ (|Is$TYPE@21| |@q$3| |@dummy$1|) |@true|) (AND (<= 0 |@q$3|) (<= |@q$3| 3) (EQ (|Is$INTEGER| |@q$3| |@DUMMY|) |@true|))))
  (FORALL (|@q$4|) (PATS (SUBTYPE (TYPECODE |@q$4| |@DUMMY|) |REFANY.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |@q$4| |@DUMMY|) |REFANY.TYPECODE|) |@true|) (EQ (|Is$REFANY| |@q$4| |@DUMMY|) |@true|)))
  (FORALL (|@q$5|) (PATS (|Is$REFANY| |@q$5| |@DUMMY|)) (IMPLIES (EQ (|Is$REFANY| |@q$5| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |@q$5| |@DUMMY|) |REFANY.TYPECODE|) |@true|)))
  (FORALL (|@q$6| |@alloc|) (PATS (MPAT (|Is$REFANY| |@q$6| |@DUMMY|) (|Is$DCL| |@q$6| |@alloc| |@DUMMY|))) (IMPLIES (AND (EQ (|Is$REFANY| |@q$6| |@DUMMY|) |@true|) (EQ (|Is$DCL| |@q$6| |@alloc| |@DUMMY|) |@true|)) (EQ (select |@alloc| |@q$6| |@SPECIAL|) |@true|)))
  (EQ (SUBTYPE |NULL.TYPECODE| |REFANY.TYPECODE|) |@true|)
  (FORALL (|@q$7|) (PATS (|Is$MUTEX| |@q$7| |@DUMMY|)) (IMPLIES (EQ (|Is$MUTEX| |@q$7| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |@q$7| |@DUMMY|) |@true|)))
  (FORALL (|@q$8|) (PATS (SUBTYPE (TYPECODE |@q$8| |@DUMMY|) |MUTEX.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |@q$8| |@DUMMY|) |MUTEX.TYPECODE|) |@true|) (EQ (|Is$MUTEX| |@q$8| |@DUMMY|) |@true|)))
  (FORALL (|@q$9|) (PATS (|Is$MUTEX| |@q$9| |@DUMMY|)) (IMPLIES (EQ (|Is$MUTEX| |@q$9| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |@q$9| |@DUMMY|) |MUTEX.TYPECODE|) |@true|)))
  (FORALL (|@q$10| |@alloc$1|) (PATS (MPAT (|Is$MUTEX| |@q$10| |@DUMMY|) (|Is$DCL| |@q$10| |@alloc$1| |@DUMMY|))) (IMPLIES (AND (EQ (|Is$MUTEX| |@q$10| |@DUMMY|) |@true|) (EQ (|Is$DCL| |@q$10| |@alloc$1| |@DUMMY|) |@true|)) (EQ (select |@alloc$1| |@q$10| |@SPECIAL|) |@true|)))
  (EQ (SUBTYPE |NULL.TYPECODE| |MUTEX.TYPECODE|) |@true|)
  (FORALL (|@q$11| |@dummy$2|) (IMPLIES (EQ (|Is$CARDINAL| |@q$11| |@dummy$2|) |@true|) (EQ (|Is$ORDINAL| |@q$11| |@DUMMY|) |@true|)))
  (FORALL (|@q$12| |@dummy$3|) (IMPLIES (EQ (|Is$CARDINAL| |@q$12| |@dummy$3|) |@true|) (AND (<= 0 |@q$12|) (EQ (|Is$INTEGER| |@q$12| |@DUMMY|) |@true|))))
  (FORALL (|@q$13|) (PATS (SUBTYPE (TYPECODE |@q$13| |@DUMMY|) |TEXT.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |@q$13| |@DUMMY|) |TEXT.TYPECODE|) |@true|) (EQ (|Is$TEXT| |@q$13| |@DUMMY|) |@true|)))
  (FORALL (|@q$14|) (PATS (|Is$TEXT| |@q$14| |@DUMMY|)) (IMPLIES (EQ (|Is$TEXT| |@q$14| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |@q$14| |@DUMMY|) |TEXT.TYPECODE|) |@true|)))
  (FORALL (|@q$15| |@alloc$2|) (PATS (MPAT (|Is$TEXT| |@q$15| |@DUMMY|) (|Is$DCL| |@q$15| |@alloc$2| |@DUMMY|))) (IMPLIES (AND (EQ (|Is$TEXT| |@q$15| |@DUMMY|) |@true|) (EQ (|Is$DCL| |@q$15| |@alloc$2| |@DUMMY|) |@true|)) (EQ (select |@alloc$2| |@q$15| |@SPECIAL|) |@true|)))
  (EQ (SUBTYPE |NULL.TYPECODE| |TEXT.TYPECODE|) |@true|)
  (FORALL (|@q$16| |@dummy$4|) (IMPLIES (EQ (|Is$CHAR| |@q$16| |@dummy$4|) |@true|) (EQ (|Is$ORDINAL| |@q$16| |@DUMMY|) |@true|)))
  (FORALL (|@q$17| |@dummy$5|) (IMPLIES (EQ (|Is$CHAR| |@q$17| |@dummy$5|) |@true|) (AND (<= 0 (ORD |@q$17|)) (< (ORD |@q$17|) 256) (EQ (TYPECODE |@q$17| |@DUMMY|) |CHAR.TYPECODE|))))
  (FORALL (|@q$18| |@dummy$6|) (IMPLIES (EQ (|Is$BOOLEAN| |@q$18| |@dummy$6|) |@true|) (EQ (|Is$ORDINAL| |@q$18| |@DUMMY|) |@true|)))
  (FORALL (|@q$19| |@dummy$7|) (IMPLIES (EQ (|Is$BOOLEAN| |@q$19| |@dummy$7|) |@true|) (AND (<= 0 (ORD |@q$19|)) (< (ORD |@q$19|) 2) (EQ (TYPECODE |@q$19| |@DUMMY|) |BOOLEAN.TYPECODE|) (OR (EQ |@q$19| |BOOLEAN.FALSE|) (EQ |@q$19| |BOOLEAN.TRUE|)))))
  (EQ |BOOLEAN.FALSE| |@false|)
  (EQ |BOOLEAN.TRUE| |@true|)
  (EQ (SUBSET ALLOCATED ALLOCATED) |@true|)
  (FORALL (v dum) (IMPLIES (EQ (|Is$INTEGER| v dum) |@true|) (AND (>= v |INTEGER.FIRST|) (<= v |INTEGER.LAST|))))
  (EQ (SUBTYPE1 |ROOT.TYPECODE| |REFANY.TYPECODE|) |@true|)
  (EQ (SUBTYPE1 |MUTEX.TYPECODE| |ROOT.TYPECODE|) |@true|)
  (< |INTEGER.FIRST| 0)
  (> |INTEGER.LAST| 0)
  (NOT (EQ (MEMBER |$NIL| LL) |@true|))
  (EQ (select ALLOCATED |$NIL| |@SPECIAL|) |@true|)
  (NEQ |@true| |@false|)
  (FORALL (|@dummy$9| |@dummy$8| |RESIDUE.Text.Value'| |RESIDUE.Text.Value| i) (PATS (MPAT (select (|FUNC.Text.Value| |RESIDUE.Text.Value|) i |@dummy$8|) (select (|FUNC.Text.Value| |RESIDUE.Text.Value'|) i |@dummy$9|))) (IMPLIES (AND (EQ (|Is$TEXT| i |@DUMMY|) |@true|) (EQ (select |RESIDUE.Text.Value| i |@ARRAY|) (select |RESIDUE.Text.Value'| i |@ARRAY|))) (EQ (select (|FUNC.Text.Value| |RESIDUE.Text.Value|) i |@dummy$8|) (select (|FUNC.Text.Value| |RESIDUE.Text.Value'|) i |@dummy$9|))))
  (EQ (|Is$INTEGER| 2 |@DUMMY|) |@true|)
  (EQ (|Is$INTEGER| 1 |@DUMMY|) |@true|)
  (EQ (|Is$INTEGER| 0 |@DUMMY|) |@true|)
  (EQ (|Is$INTEGER| 3 |@DUMMY|) |@true|)
  )
 )

(FORALL (|Test11.g`| |b`| |ALLOCATED`| |LL`|) (IMPLIES (EQ (|Is$BOOLEAN| b |@DUMMY|) |@true|) (FORALL (|Test11.g$1|) (IMPLIES (OR (EXISTS (|Test11.g$2|) (AND (EQ |Test11.g$2| |Test11.g|) (NOT (EQ b |@true|)) (EQ |Test11.g$1| (+ |Test11.g$2| 1)))) (AND (NOT (NOT (EQ b |@true|))) (EQ |Test11.g$1| |Test11.g|))) (AND (LBL |ERROR.POSTCONDITION.15.0.Normal return| (IMPLIES (EQ RETURN RETURN) (AND (IMPLIES (EQ b |@true|) (EQ |Test11.g$1| (+ |Test11.g| 1))) (IMPLIES (NOT (EQ b |@true|)) (EQ |Test11.g$1| |Test11.g|))))) (LBL |ERROR.POSTCONDITION.15.0.RAISES| (EQ RETURN RETURN)) (LBL |ERROR.MOD_POST.15.0.Test11.g| TRUE) (LBL |ERROR.INV_POST.15.0| TRUE))))))

; XXX non-UTVPI
;(FORALL (|Test11.g`| |ALLOCATED`| |LL`|) (FORALL (y x) (IMPLIES (AND (EQ (|Is$INTEGER| y |@DUMMY|) |@true|) (EQ (|Is$TYPE@24| x |@DUMMY|) |@true|)) (FORALL (|EXCEPTION.code| b |ALLOCATED$1| |ALLOCATED'| |Test11.g$1| |Test11.g'|) (AND (LBL |ERROR.CALL.29.4| TRUE) (IMPLIES (AND (IMPLIES (EQ |EXCEPTION.code| RETURN) (AND (EQ |Test11.g'| (+ (- 0 1) 1)) (IMPLIES (NOT TRUE) (EQ |Test11.g'| (- 0 1))))) (EQ |EXCEPTION.code| RETURN) TRUE (EQ (SUBSET ALLOCATED |ALLOCATED'|) |@true|) (EQ (|Is$INTEGER| |Test11.g'| |@DUMMY|) |@true|)) (FORALL (|EXCEPTION.code$1| |x$1| |x'| |ALLOCATED$2| |ALLOCATED'$1|) (AND (LBL |ERROR.CALL.31.4| (> |Test11.g'| 0)) (IMPLIES (AND (IMPLIES (EQ |EXCEPTION.code$1| RETURN) (EQ |x'| (+ |Test11.g'| 1))) (EQ |EXCEPTION.code$1| RETURN) TRUE (EQ (SUBSET |ALLOCATED'| |ALLOCATED'$1|) |@true|) (EQ (|Is$INTEGER| |x'| |@DUMMY|) |@true|)) (FORALL (res) (FORALL (|res$1|) (FORALL (|EXCEPTION.code$2| |RES(Test11.Inc@32.11)| |x$2| |ALLOCATED$3| |ALLOCATED'$2|) (AND (LBL |ERROR.CALL.32.11| (> |x'| 0)) (IMPLIES (AND (IMPLIES (EQ |EXCEPTION.code$2| RETURN) (EQ |RES(Test11.Inc@32.11)| (+ |x'| 1))) (EQ |EXCEPTION.code$2| RETURN) (EQ (SUBSET |ALLOCATED'$1| |ALLOCATED'$2|) |@true|) (EQ (|Is$INTEGER| |RES(Test11.Inc@32.11)| |@DUMMY|) |@true|)) (AND (LBL |ERROR.INDEX.32.11| (AND (<= 0 |RES(Test11.Inc@32.11)|) (< |RES(Test11.Inc@32.11)| (+ 4 0)))) (LBL |ERROR.POSTCONDITION.24.0.RAISES| (EQ RETURN RETURN)) (LBL |ERROR.MOD_POST.24.0.Test11.g| TRUE) (LBL |ERROR.INV_POST.24.0| TRUE))))))))))))))))

(BG_POP)