Bloat1.smt

; Starting query at ./Bloat1.fst(3,0-3,32)
(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 
;; def=FStar/bin/../ulib/prims.fst(170,52-170,69); use=FStar/bin/../ulib/prims.fst(193,30-193,42)
(forall ((@x0 Term))
 (! (implies (and (HasType @x0
Prims.int)

;; def=./Bloat1.fst(3,19-3,26); use=./Bloat1.fst(3,19-3,26)
(= @x0
(Prims.op_Subtraction (BoxInt 1)
(BoxInt 1)))
)

;; 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(150,5-150,31); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(forall ((@x2 Term))
 (! (implies (and (HasType @x2
Prims.int)

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

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

;; def=./Bloat1.fst(3,18-3,32); use=./Bloat1.fst(3,18-3,32)
(= @x3
(Prims.eq2 Prims.int
(Prims.op_Subtraction (BoxInt 1)
(BoxInt 1))
(BoxInt 0)))
)

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

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

;; def=./Bloat1.fst(3,18-3,32); use=FStar/bin/../ulib/prims.fst(231,4-231,11)
(or label_1

;; def=./Bloat1.fst(3,18-3,32); use=FStar/bin/../ulib/prims.fst(231,4-231,11)
(= (Prims.op_Subtraction (BoxInt 1)
(BoxInt 1))
(BoxInt 0))
)
)
 
;;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)