Factorial w/o type annotation

Bloat7.smt2

; Starting query at ./simplefactorial.fst(1,22-4,61)
;;;;;;;;;;;;;;;;Uninterpreted function symbol for impure function
(declare-fun Simplefactorial.factorial (Term) Term)
;;;;;;;;;;;;;;;;Uninterpreted name for impure function
(declare-fun Simplefactorial.factorial@tok () Term)
(declare-fun label_34 () Bool)
(declare-fun label_33 () Bool)
(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
Prims.int)
(forall ((@x1 Term))
 (implies (HasType @x1
FStar.Heap.heap)
(forall ((@x2 Term))
 (implies (and (= @x2
@x0)
(HasType @x2
Prims.int))
(forall ((@x3 Term))
 (implies (and (= @x3
(BoxInt 0))
(HasType @x3
Prims.int))
(forall ((@x4 Term))
 (implies (and (HasType @x4
Prims.bool)
(= @x4
(Prims.op_Equality Prims.int
@x0
(BoxInt 0))))
(forall ((@x5 Term))
 (implies (and (= @x5
@x4)
(HasType @x5
Prims.bool)
(BoxBool_proj_0 (Prims.is_V Prims.bool
(Prims.V Prims.bool
@x5))))
(forall ((@x6 Term))
 (implies (and (forall ((@x7 Term) (@x8 Term))
 (! (iff (Valid (ApplyTT (ApplyTT @x6
@x7)
@x8))
true)
 :weight 0
 
:pattern ((ApplyTT (ApplyTT @x6
@x7)
@x8))))
(HasType @x6
(Prims.all_post_h FStar.Heap.heap
Prims.int)))
(and (implies (not (= (Prims.V.v Prims.bool
(Prims.V Prims.bool
@x5))
(BoxBool true)))
(forall ((@x7 Term))
 (implies (and (= (Prims.V.v Prims.bool
(Prims.V Prims.bool
@x5))
@x7)
(HasType @x7
Prims.bool))
(forall ((@x8 Term))
 (implies (and (= @x8
@x0)
(HasType @x8
Prims.int)
(BoxBool_proj_0 (Prims.is_V Prims.int
(Prims.V Prims.int
@x8))))
(forall ((@x9 Term))
 (implies (and (= @x9
@x0)
(HasType @x9
Prims.int))
(forall ((@x10 Term))
 (implies (and (HasType @x10
Prims.int)
(= @x10
(Prims.op_Subtraction @x0
(BoxInt 1))))
(forall ((@x11 Term))
 (implies (and (= @x11
@x10)
(HasType @x11
Prims.int)
(BoxBool_proj_0 (Prims.is_V Prims.int
(Prims.V Prims.int
@x11))))
(forall ((@x12 Term) (@x13 Term))
 (implies (and (HasType @x13
FStar.Heap.heap)
(HasType @x12
(Prims.result Prims.int))
(BoxBool_proj_0 (Prims.is_V Prims.int
@x12)))
(forall ((@x14 Term))
 (implies (and (HasType @x14
Prims.int)
(= @x14
(Prims.op_Multiply @x0
(Prims.V.v Prims.int
@x12))))
(forall ((@x15 Term))
 (implies (and (= @x15
@x14)
(HasType @x15
Prims.int))
(or label_33
(Valid (ApplyTT (ApplyTT @x6
(Prims.V Prims.int
@x15))
@x13)))));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
)
(implies (= (Prims.V.v Prims.bool
(Prims.V Prims.bool
@x5))
(BoxBool true))
(forall ((@x7 Term))
 (implies (and (= @x7
(BoxInt 1))
(HasType @x7
Prims.int))
(or label_32
(Valid (ApplyTT (ApplyTT @x6
(Prims.V Prims.int
@x7))
@x1)))));;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_34")
(eval label_34)
(echo "label_33")
(eval label_33)
(echo "label_32")
(eval label_32)
(echo "Done!")
(pop)
(pop)

; Ending query at ./simplefactorial.fst(1,22-4,61)
(push)

; Starting query at ./simplefactorial.fst(4,4-4,9)
;;;;;;;;;;;;;;;;Uninterpreted function symbol for impure function
(declare-fun Simplefactorial.factorial (Term) Term)
;;;;;;;;;;;;;;;;Uninterpreted name for impure function
(declare-fun Simplefactorial.factorial@tok () Term)
(declare-fun label_36 () Bool)
(declare-fun label_35 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))
;;;;;;;;;;;;;;;;query
(assert (!
(not (forall ((@x0 Term))
 (implies (HasType @x0
Prims.int)
(and (or label_36
(Valid (Prims.hasEq Prims.int)))
(forall ((@x1 Term))
 (implies (and (Valid (Prims.hasEq @x1))
(HasType @x1
Tm_type))
(or label_35
(Valid (Prims.hasEq @x1)))));;no pats
)));;no pats
)
:named @query))
(set-option :timeout 5000)
(check-sat)
(echo "label_36")
(eval label_36)
(echo "label_35")
(eval label_35)
(echo "Done!")
(pop)