Bloat9.smt2

; Starting query at ./bloat9.fst(7,31-9,24)
(declare-fun label_32 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))
;;;;;;;;;;;;;;;;query
(assert (!
(not (forall ((@x0 Term))
 (implies (HasType @x0
(FStar.ST.ref Prims.int))
(forall ((@x1 Term) (@x2 Term))
 (implies (and (forall ((@x3 Term) (@x4 Term))
 (implies (and (HasType @x3
Prims.unit)
(HasType @x4
FStar.Heap.heap))
(Valid (ApplyTT (ApplyTT @x1
@x3)
@x4))));;no pats

(HasType @x2
FStar.Heap.heap)
(HasType @x1
(Prims.st_post_h FStar.Heap.heap
Prims.unit)))
(forall ((@x3 Term))
 (implies (and (= @x3
@x0)
(HasType @x3
(FStar.ST.ref Prims.int)))
(forall ((@x4 Term))
 (implies (and (HasType @x4
Prims.int)
(= @x4
(Prims.op_Addition (FStar.Heap.sel Prims.int
@x2
@x0)
(BoxInt 1))))
(forall ((@x5 Term))
 (implies (and (= @x5
@x4)
(HasType @x5
Prims.int))
(forall ((@x6 Term))
 (implies (and (= @x6
@x0)
(HasType @x6
(FStar.ST.ref Prims.int)))
(forall ((@x7 Term))
 (implies (and (= @x7
@x5)
(HasType @x7
Prims.int))
(forall ((@x8 Term) (@x9 Term))
 (implies (and (= @x9
(FStar.Heap.upd Prims.int
@x2
@x0
@x5))
(HasType @x9
FStar.Heap.heap)
(HasType @x8
Prims.unit))
(or label_32
(Valid (ApplyTT (ApplyTT @x1
@x8)
@x9)))));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
)
:named @query))
(set-option :timeout 5000)
(check-sat)
(echo "label_32")
(eval label_32)
(echo "Done!")
(pop)