Bloat4.smt

; Starting query at ./Bloat4.fst(3,0-3,38)
(declare-fun label_1 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (! (= MaxFuel
(SFuel (SFuel ZFuel)))
:named @MaxFuel_assumption))
(assert (! (= MaxIFuel
(SFuel ZFuel))
:named @MaxIFuel_assumption))
;;;;;;;;;;;;;;;;query
(assert (! (not (forall ((@x0 Term))
 (! (implies (HasType @x0
Prims.int)

;; def=FStar/bin/../ulib/prims.fst(150,5-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(forall ((@x1 Term))
 (! (implies (and (HasType @x1
Prims.int)

;; def=FStar/bin/../ulib/prims.fst(150,19-150,23); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(= @x1
@x0)
)

;; def=FStar/bin/../ulib/prims.fst(170,52-170,69); use=FStar/bin/../ulib/prims.fst(193,30-193,42)
(forall ((@x2 Term))
 (! (implies (and (HasType @x2
Prims.bool)

;; def=./Bloat4.fst(3,16-3,23); use=./Bloat4.fst(3,16-3,23)
(= @x2
(Prims.op_GreaterThan @x0
(BoxInt 0)))
)

;; def=FStar/bin/../ulib/prims.fst(150,5-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(forall ((@x3 Term))
 (! (implies (and (HasType @x3
Prims.bool)

;; def=FStar/bin/../ulib/prims.fst(150,19-150,23); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(= @x3
@x2)
)

;; def=FStar/bin/../ulib/prims.fst(160,5-162,10); use=FStar/bin/../ulib/prims.fst(178,22-178,33)
(forall ((@x4 Term))
 (! (implies (and (HasType @x4
(Prims.pure_post Prims.int))

;; def=FStar/bin/../ulib/prims.fst(160,5-162,10); use=FStar/bin/../ulib/prims.fst(178,22-178,33)
(forall ((@x5 Term))
 (! (iff 
;; def=FStar/bin/../ulib/prims.fst(161,46-161,49); use=FStar/bin/../ulib/prims.fst(178,22-178,33)
(Valid 
;; def=FStar/bin/../ulib/prims.fst(161,46-161,49); use=FStar/bin/../ulib/prims.fst(178,22-178,33)
(ApplyTT @x4
@x5)
)


;; def=FStar/bin/../ulib/prims.fst(171,68-171,72); use=FStar/bin/../ulib/prims.fst(184,22-184,34)
true
)
 :weight 0


:pattern ((ApplyTT @x4
@x5))
:qid @query.5))
)

;; def=FStar/bin/../ulib/prims.fst(109,47-109,70); use=FStar/bin/../ulib/prims.fst(177,22-177,39)
(and (implies 
;; def=./Bloat4.fst(3,16-3,30); use=./Bloat4.fst(3,16-3,30)
(= @x3
(BoxBool true))


;; def=FStar/bin/../ulib/prims.fst(150,5-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(forall ((@x5 Term))
 (! (implies (and (HasType @x5
Prims.int)

;; def=FStar/bin/../ulib/prims.fst(150,19-150,23); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(= @x5
(BoxInt 1))
)

;; def=FStar/bin/../ulib/prims.fst(150,28-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(Valid 
;; def=FStar/bin/../ulib/prims.fst(150,28-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(ApplyTT @x4
@x5)
)
)
 
;;no pats
:qid @query.6))
)
(implies 
;; def=FStar/bin/../ulib/prims.fst(109,61-109,63); use=FStar/bin/../ulib/prims.fst(177,22-177,39)
(not 
;; def=./Bloat4.fst(3,16-3,30); use=./Bloat4.fst(3,16-3,30)
(= @x3
(BoxBool true))
)


;; def=FStar/bin/../ulib/prims.fst(167,90-167,110); use=FStar/bin/../ulib/prims.fst(180,22-180,35)
(forall ((@x5 Term))
 (! (implies (and (HasType @x5
Prims.bool)

;; def=./Bloat4.fst(3,16-3,38); use=./Bloat4.fst(3,16-3,38)
(= @x3
@x5)
)

;; def=FStar/bin/../ulib/prims.fst(170,52-170,69); use=FStar/bin/../ulib/prims.fst(193,30-193,42)
(forall ((@x6 Term))
 (! (implies (and (HasType @x6
Prims.int)

;; def=./Bloat4.fst(3,36-3,38); use=./Bloat4.fst(3,36-3,38)
(= @x6
(Prims.op_Minus (BoxInt 1)))
)

;; def=FStar/bin/../ulib/prims.fst(150,5-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(forall ((@x7 Term))
 (! (implies (and (HasType @x7
Prims.int)

;; def=FStar/bin/../ulib/prims.fst(150,19-150,23); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(= @x7
@x6)
)

;; def=FStar/bin/../ulib/prims.fst(150,28-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(Valid 
;; def=FStar/bin/../ulib/prims.fst(150,28-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(ApplyTT @x4
@x7)
)
)
 
;;no pats
:qid @query.9))
)
 
;;no pats
:qid @query.8))
)
 
;;no pats
:qid @query.7))
))
)
 
;;no pats
:qid @query.4))
)
 
;;no pats
:qid @query.3))
)
 
;;no pats
:qid @query.2))
)
 
;;no pats
:qid @query.1))
)
 
;;no pats
:qid @query)))
:named @query))
(set-option :rlimit 2723280)
(check-sat)
(echo "label_1")
(eval label_1)
(echo "Done!")
(pop)