Bloat2.smt

; Starting query at ./Bloat2.fst(3,0-5,12)
(declare-fun label_2 () Bool)
(declare-fun label_1 () Bool)
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3285))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3286))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3287))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3288))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3289))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3290))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3291))
;;;;;;;;;;;;;;;;Uvar typing
(assert (! (HasType (Tm_uvar 26534)
Tm_type)
:named uvar_typing_26534__3292))
(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.list (Tm_uvar 26534)))

;; def=FStar/bin/../ulib/prims.fst(160,5-162,10); use=FStar/bin/../ulib/prims.fst(178,22-178,33)
(forall ((@x1 Term))
 (! (implies (and (HasType @x1
(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 ((@x2 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 @x1
@x2)
)


;; 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 @x1
@x2))
:qid @query.2))
)

;; def=FStar/bin/../ulib/prims.fst(109,47-109,70); use=FStar/bin/../ulib/prims.fst(177,22-177,39)
(and (implies 
;; def=FStar/bin/../ulib/prims.fst(109,47-109,56); use=FStar/bin/../ulib/prims.fst(177,22-177,39)
(and 
;; def=./Bloat2.fst(0,0-3,10); use=./Bloat2.fst(0,0-3,10)
(= (Prims.uu___is_Nil (Tm_uvar 26534)
@x0)
(BoxBool true))


;; def=./Bloat2.fst(3,9-4,4); use=./Bloat2.fst(3,9-4,4)
(= @x0
(Prims.Nil (Tm_uvar 26534)))
)


;; 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(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 @x1
@x2)
)
)
 
;;no pats
:qid @query.3))
)
(implies 
;; def=FStar/bin/../ulib/prims.fst(109,61-109,63); use=FStar/bin/../ulib/prims.fst(177,22-177,39)
(not 
;; def=./Bloat2.fst(0,0-3,10); use=./Bloat2.fst(0,0-3,10)
(= (Prims.uu___is_Nil (Tm_uvar 26534)
@x0)
(BoxBool true))
)


;; def=FStar/bin/../ulib/prims.fst(109,47-109,70); use=FStar/bin/../ulib/prims.fst(177,22-177,39)
(and (implies 
;; def=./Bloat2.fst(0,0-3,10); use=./Bloat2.fst(0,0-3,10)
(= (Prims.uu___is_Cons (Tm_uvar 26534)
@x0)
(BoxBool true))


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

;; def=./Bloat2.fst(3,9-5,7); use=./Bloat2.fst(3,9-5,7)
(= @x0
(Prims.Cons (Tm_uvar 26534)
@x2
@x3))
)

;; 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
Prims.int)

;; def=FStar/bin/../ulib/prims.fst(150,19-150,23); use=FStar/bin/../ulib/prims.fst(175,22-175,33)
(= @x4
(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 @x1
@x4)
)
)
 
;;no pats
:qid @query.5))
)
 
;;no pats
:qid @query.4))
)
(implies 
;; def=FStar/bin/../ulib/prims.fst(109,61-109,63); use=FStar/bin/../ulib/prims.fst(177,22-177,39)
(not 
;; def=./Bloat2.fst(0,0-3,10); use=./Bloat2.fst(0,0-3,10)
(= (Prims.uu___is_Cons (Tm_uvar 26534)
@x0)
(BoxBool true))
)

label_2))
))
)
 
;;no pats
:qid @query.1))
)
 
;;no pats
:qid @query)))
:named @query))
(set-option :rlimit 2723280)
(check-sat)
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "Done!")
(pop)