bloat5.smt2

; Starting query at ./bloat5.fst(8,18-8,68)
(declare-fun label_2 () Bool)
(declare-fun label_1 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))
;;;;;;;;;;;;;;;;query
(assert (!
(not 
;; def=./bloat5.fst(8,18-8,68); use=./bloat5.fst(8,18-8,68)
(and (forall ((@x0 Term))
 (implies (and (HasType @x0
Tm_type)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=./bloat5.fst(8,18-8,68)
(Valid 
;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=./bloat5.fst(8,18-8,68)
(Prims.hasEq @x0)
)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=./bloat5.fst(8,18-8,68)
(or label_1

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=./bloat5.fst(8,18-8,68)
(Valid 
;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=./bloat5.fst(8,18-8,68)
(Prims.hasEq @x0)
)
)
));;no pats


;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=./bloat5.fst(8,18-8,68)
(or label_2

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43)
(Valid 
;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(224,36-224,43)
(Prims.hasEq Prims.int)
)
)
)
)
:named @query))
(set-option :rlimit 2723280)
(check-sat)
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "Done!")
(pop)

; Ending query at ./bloat5.fst(8,18-8,68)
(pop)
(push)

; Starting query at ./bloat5.fst(8,0-8,68)
(declare-fun label_3 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))
;;;;;;;;;;;;;;;;query
(assert (!
(not 
;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x0 Term))
 (implies (and (HasType @x0
Prims.int)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x0
(BoxInt 0))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x1 Term))
 (implies (and (HasType @x1
(Prims.list Prims.int))

;; def=./bloat5.fst(8,43-8,46); use=./bloat5.fst(8,43-8,46)
(= @x1
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int)))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x2 Term))
 (implies (and (HasType @x2
(Prims.list Prims.int))

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x2
@x1)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x3 Term))
 (implies (and (HasType @x3
Prims.int)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x3
(BoxInt 0))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x4 Term))
 (implies (and (HasType @x4
(Prims.list Prims.int))

;; def=./bloat5.fst(8,49-8,52); use=./bloat5.fst(8,49-8,52)
(= @x4
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int)))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x5 Term))
 (implies (and (HasType @x5
(Prims.list Prims.int))

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x5
@x4)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x6 Term))
 (implies (and (HasType @x6
Prims.int)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x6
(BoxInt 0))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x7 Term))
 (implies (and (HasType @x7
Prims.int)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x7
(BoxInt 0))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x8 Term))
 (implies (and (HasType @x8
(Prims.list Prims.int))

;; def=./bloat5.fst(8,55-8,61); use=./bloat5.fst(8,55-8,61)
(= @x8
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int)))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x9 Term))
 (implies (and (HasType @x9
(Prims.list Prims.int))

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x9
@x8)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x10 Term))
 (implies (and (HasType @x10
(Prims.list Prims.int))

;; def=./bloat5.fst(8,55-8,61); use=./bloat5.fst(8,55-8,61)
(= @x10
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int))))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x11 Term))
 (implies (and (HasType @x11
(Prims.list Prims.int))

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x11
@x10)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x12 Term))
 (implies (and (HasType @x12
(Prims.list Prims.int))

;; def=./bloat5.fst(8,49-8,61); use=./bloat5.fst(8,49-8,61)
(= @x12
(FStar.List.Tot.Base.op_At Prims.int
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int))
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int)))))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x13 Term))
 (implies (and (HasType @x13
(Prims.list Prims.int))

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x13
@x12)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x14 Term))
 (implies (and (HasType @x14
(Prims.list Prims.int))

;; def=./bloat5.fst(8,42-8,62); use=./bloat5.fst(8,42-8,62)
(= @x14
(FStar.List.Tot.Base.op_At Prims.int
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int))
(FStar.List.Tot.Base.op_At Prims.int
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int))
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int))))))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x15 Term))
 (implies (and (HasType @x15
(Prims.list Prims.int))

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x15
@x14)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x16 Term))
 (implies (and (HasType @x16
Prims.nat)

;; def=./bloat5.fst(8,34-8,63); use=./bloat5.fst(8,34-8,63)
(= @x16
(FStar.List.Tot.Base.length Prims.int
(FStar.List.Tot.Base.op_At Prims.int
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int))
(FStar.List.Tot.Base.op_At Prims.int
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int))
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Cons Prims.int
(BoxInt 0)
(Prims.Nil Prims.int)))))))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x17 Term))
 (implies (and (HasType @x17
Prims.nat)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x17
@x16)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x18 Term))
 (implies (and (HasType @x18
Prims.int)

;; def=./bloat5.fst(8,19-8,63); use=./bloat5.fst(8,19-8,63)
(= @x18
(BoxInt 4))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x19 Term))
 (implies (and (HasType @x19
Prims.int)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x19
@x18)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x20 Term))
 (implies (and (HasType @x20
Prims.int)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x20
(BoxInt 4))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x21 Term))
 (implies (and (HasType @x21
Prims.bool)

;; def=./bloat5.fst(8,18-8,68); use=./bloat5.fst(8,18-8,68)
(= @x21
(BoxBool true))
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,5-150,31); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(forall ((@x22 Term))
 (implies (and (HasType @x22
Prims.bool)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(150,19-150,23); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(175,22-175,33)
(= @x22
@x21)
)

;; def=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(170,52-170,69); use=/usr/local/Cellar/fstar/0.9.4.0_1/ulib/prims.fst(193,30-193,42)
(forall ((@x23 Term))
 (implies (HasType @x23
Tm_type)

;; def=./bloat5.fst(8,18-8,68); use=./bloat5.fst(8,11-8,17)
(or label_3

;; def=./bloat5.fst(8,18-8,68); use=./bloat5.fst(8,11-8,17)
(BoxBool_proj_0 (BoxBool true))
)
));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

));;no pats

)
:named @query))
(set-option :rlimit 2723280)
(check-sat)
(echo "label_3")
(eval label_3)
(echo "Done!")
(pop)