FStar build with configurable Z3 inputs — 2026-06-09 #9794

2026-06-09T14:34:46Z

github-actions[bot]
Bot Jun 9, 2026

Build status

✅ Z3 build completed
⚠️ FStar build failure (pipeline continued)

Inputs used

z3_ref: master
z3_cmake_args: ``
z3_runtime_args: smt.ho_matching=true
fstar_ref: _nik_higher_order_smt
fstar_opam_switch: 4.14.2
fstar_otherflags: --split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery

Produced versions

Z3: Z3 version 4.17.0 - 64 bit - build hashcode 32e50e014ee2549dad5e725b6173404bccb4f665
FStar: unknown
FStar commit: 848d63ad4a10703c2424e293c4023c0e868d2b1a

Generated SMT2 files

Artifact: https://github.com/Z3Prover/z3/actions/runs/27211368950/artifacts/7510881703

First 1000 lines per generated .smt2 file:

`failedQueries-FStar.Algebra.Monoid-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   ;; def=Prims.fst(427,77-427,89); use=Prims.fst(427,77-427,89)
   (and
    (forall ((@x0 Term) (@x1 Term))
     (! (implies
       (and (HasType @x0 Prims.nat) (HasType @x1 Prims.nat))
       ;; def=Prims.fst(642,18-642,24); use=FStar.Algebra.Monoid.fst(60,30-60,35)
       (or
        label_1
        ;; def=Prims.fst(642,18-642,24); use=FStar.Algebra.Monoid.fst(60,30-60,35)
        (>= (BoxInt_proj_0 (Prims.op_Addition @x0 @x1)) (BoxInt_proj_0 (BoxInt 0)))))
      :qid @query))
    ;; def=Prims.fst(419,66-419,102); use=Prims.fst(422,31-422,44)
    (forall ((@x0 Term))
     (! (implies
       (and
        (HasType @x0 Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba)
        ;; def=FStar.Algebra.Monoid.fst(60,6-60,35); use=FStar.Algebra.Monoid.fst(60,6-60,35)
        (=
         (WithType
          ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
          (Tm_lambda
           Prims.nat
           ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
           (lambda ((@x1 Term))
            ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
            (Tm_lambda
             Prims.nat
             ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
             (lambda ((@x2 Term)) (Prims.op_Addition @x1 @x2)))))
          Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba)
         @x0))
       ;; def=FStar.Algebra.Monoid.fst(51,14-51,109); use=FStar.Algebra.Monoid.fst(61,2-61,14)
       (and
        ;; def=FStar.Algebra.Monoid.fst(51,15-51,45); use=FStar.Algebra.Monoid.fst(61,2-61,14)
        (or
         label_2
         ;; def=FStar.Algebra.Monoid.fst(51,15-51,45); use=FStar.Algebra.Monoid.fst(61,2-61,14)
         (Valid
          ;; def=FStar.Algebra.Monoid.fst(51,15-51,45); use=FStar.Algebra.Monoid.fst(61,2-61,14)
          (FStar.Algebra.Monoid.right_unitality_lemma U_zero Prims.nat (BoxInt 0) @x0)))
        ;; def=FStar.Algebra.Monoid.fst(51,49-51,78); use=FStar.Algebra.Monoid.fst(61,2-61,14)
        (or
         label_3
         ;; def=FStar.Algebra.Monoid.fst(51,49-51,78); use=FStar.Algebra.Monoid.fst(61,2-61,14)
         (Valid
          ;; def=FStar.Algebra.Monoid.fst(51,49-51,78); use=FStar.Algebra.Monoid.fst(61,2-61,14)
          (FStar.Algebra.Monoid.left_unitality_lemma U_zero Prims.nat (BoxInt 0) @x0)))
        ;; def=FStar.Algebra.Monoid.fst(51,82-51,108); use=FStar.Algebra.Monoid.fst(61,2-61,14)
        (or
         label_4
         ;; def=FStar.Algebra.Monoid.fst(51,82-51,108); use=FStar.Algebra.Monoid.fst(61,2-61,14)
         (Valid
          ;; def=FStar.Algebra.Monoid.fst(51,82-51,108); use=FStar.Algebra.Monoid.fst(61,2-61,14)
          (FStar.Algebra.Monoid.associativity_lemma U_zero Prims.nat @x0)))))
      :qid @query.1))))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_4")
(eval label_4)
(echo "label_3")
(eval label_3)
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.DependentMap-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   (forall ((@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term) (@x4 Term))
    (! (implies
      (and
       (HasType @x0 Prims.eqtype)
       (HasType @x1 (Tm_arrow_691ba3b0ee09d4bdef69566fca8dc50b @x0 uu___115))
       (HasType @x2 (FStar.DependentMap.t uu___115 @x0 @x1))
       (HasType @x3 @x0)
       (HasType @x4 (ApplyTT @x1 @x3)))
      ;; def=Prims.fst(373,4-373,44); use=Prims.fst(398,19-398,32)
      (forall ((@x5 Term))
       (! (implies
         (and
          (HasType @x5 (Prims.pure_post U_zero Prims.unit))
          ;; def=Prims.fst(409,36-409,97); use=FStar.DependentMap.fst(39,2-39,4)
          (forall ((@x6 Term))
           (! (implies
             (and
              (or label_1 (HasType @x6 Prims.unit))
              ;; def=FStar.DependentMap.fsti(65,21-65,45); use=FStar.DependentMap.fst(39,2-39,4)
              (or
               label_2
               ;; def=FStar.DependentMap.fsti(65,21-65,45); use=FStar.DependentMap.fst(39,2-39,4)
               (=
                (FStar.DependentMap.sel
                 uu___115
                 @x0
                 @x1
                 (FStar.DependentMap.upd uu___115 @x0 @x1 @x2 @x3 @x4)
                 @x3)
                @x4)))
             ;; def=Prims.fst(409,83-409,96); use=FStar.DependentMap.fst(39,2-39,4)
             (Valid
              ;; def=Prims.fst(409,83-409,96); use=FStar.DependentMap.fst(39,2-39,4)
              (ApplyTT @x5 @x6)))
            :pattern
             (;; def=Prims.fst(409,83-409,96); use=FStar.DependentMap.fst(39,2-39,4)
              (Valid
               ;; def=Prims.fst(409,83-409,96); use=FStar.DependentMap.fst(39,2-39,4)
               (ApplyTT @x5 @x6)))
            :qid @query.2)))
         ;; def=Prims.fst(419,66-419,102); use=Prims.fst(422,31-422,44)
         (forall ((@x6 Term))
          (! (implies
            (HasType @x6 Prims.unit)
            ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
            (Valid
             ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
             (ApplyTT @x5 @x6)))
           :qid @query.3)))
        :qid @query.1)))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.GSet-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   (forall ((@x0 Term) (@x1 Term) (@x2 Term))
    (! (implies
      (and (HasType @x0 (Tm_type uu___72)) (HasType @x1 @x0) (HasType @x2 @x0))
      ;; def=Prims.fst(373,4-373,44); use=Prims.fst(398,19-398,32)
      (forall ((@x3 Term))
       (! (implies
         (and
          (HasType @x3 (Prims.pure_post U_zero Prims.unit))
          ;; def=Prims.fst(409,36-409,97); use=FStar.GSet.fst(41,32-41,34)
          (forall ((@x4 Term))
           (! (implies
             (and
              (or label_1 (HasType @x4 Prims.unit))
              ;; def=FStar.GSet.fsti(53,12-53,45); use=FStar.GSet.fst(41,32-41,34)
              (or
               label_2
               ;; def=FStar.GSet.fsti(53,12-53,45); use=FStar.GSet.fst(41,32-41,34)
               (iff
                ;; def=FStar.GSet.fsti(53,13-53,32); use=FStar.GSet.fst(41,32-41,34)
                (BoxBool_proj_0
                 (FStar.GSet.mem uu___72 @x0 @x2 (FStar.GSet.singleton uu___72 @x0 @x1)))
                ;; def=FStar.GSet.fsti(53,38-53,44); use=FStar.GSet.fst(41,32-41,34)
                (= @x1 @x2))))
             ;; def=Prims.fst(409,83-409,96); use=FStar.GSet.fst(41,32-41,34)
             (Valid
              ;; def=Prims.fst(409,83-409,96); use=FStar.GSet.fst(41,32-41,34)
              (ApplyTT @x3 @x4)))
            :pattern
             (;; def=Prims.fst(409,83-409,96); use=FStar.GSet.fst(41,32-41,34)
              (Valid
               ;; def=Prims.fst(409,83-409,96); use=FStar.GSet.fst(41,32-41,34)
               (ApplyTT @x3 @x4)))
            :qid @query.2)))
         ;; def=Prims.fst(419,66-419,102); use=Prims.fst(422,31-422,44)
         (forall ((@x4 Term))
          (! (implies
            (HasType @x4 Prims.unit)
            ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
            (Valid
             ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
             (ApplyTT @x3 @x4)))
           :qid @query.3)))
        :qid @query.1)))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.GhostSet-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   (forall ((@x0 Term) (@x1 Term) (@x2 Term))
    (! (implies
      (and (HasType @x0 (Tm_type uu___72)) (HasType @x1 @x0) (HasType @x2 @x0))
      ;; def=Prims.fst(373,4-373,44); use=Prims.fst(398,19-398,32)
      (forall ((@x3 Term))
       (! (implies
         (and
          (HasType @x3 (Prims.pure_post U_zero Prims.unit))
          ;; def=Prims.fst(409,36-409,97); use=FStar.GhostSet.fst(41,32-41,34)
          (forall ((@x4 Term))
           (! (implies
             (and
              (or label_1 (HasType @x4 Prims.unit))
              ;; def=FStar.GhostSet.fsti(53,12-53,45); use=FStar.GhostSet.fst(41,32-41,34)
              (or
               label_2
               ;; def=FStar.GhostSet.fsti(53,12-53,45); use=FStar.GhostSet.fst(41,32-41,34)
               (iff
                ;; def=FStar.GhostSet.fsti(53,13-53,32); use=FStar.GhostSet.fst(41,32-41,34)
                (BoxBool_proj_0
                 (FStar.GhostSet.mem uu___72 @x0 @x2 (FStar.GhostSet.singleton uu___72 @x0 @x1)))
                ;; def=FStar.GhostSet.fsti(53,38-53,44); use=FStar.GhostSet.fst(41,32-41,34)
                (= @x1 @x2))))
             ;; def=Prims.fst(409,83-409,96); use=FStar.GhostSet.fst(41,32-41,34)
             (Valid
              ;; def=Prims.fst(409,83-409,96); use=FStar.GhostSet.fst(41,32-41,34)
              (ApplyTT @x3 @x4)))
            :pattern
             (;; def=Prims.fst(409,83-409,96); use=FStar.GhostSet.fst(41,32-41,34)
              (Valid
               ;; def=Prims.fst(409,83-409,96); use=FStar.GhostSet.fst(41,32-41,34)
               (ApplyTT @x3 @x4)))
            :qid @query.2)))
         ;; def=Prims.fst(419,66-419,102); use=Prims.fst(422,31-422,44)
         (forall ((@x4 Term))
          (! (implies
            (HasType @x4 Prims.unit)
            ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
            (Valid
             ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
             (ApplyTT @x3 @x4)))
           :qid @query.3)))
        :qid @query.1)))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.LexicographicOrdering-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   (forall ((@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term) (@x4 Term) (@x5 Term))
    (! (implies
      (and
       (HasType @x0 (Tm_type a))
       (HasType @x1 (Tm_arrow_5b1c7f3f701f4c9bd877a4f9b4ec1dfa @x0 b a))
       (HasType @x2 (FStar.WellFounded.binrel a @x0))
       (HasType @x3 (Tm_arrow_bb074318a2006f6490fd85adc80d67dd @x0 b @x1 a))
       (HasType @x4 (FStar.WellFounded.well_founded a @x0 @x2))
       (HasType @x5 (Tm_arrow_5dbc3dfa5b57e1572d5d420104425158 @x0 b @x1 @x3 a)))
      ;; def=Prims.fst(373,4-373,44); use=Prims.fst(398,19-398,32)
      (forall ((@x6 Term))
       (! (implies
         (and
          (HasType @x6 (Prims.pure_post U_zero Prims.unit))
          ;; def=Prims.fst(409,36-409,97); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
          (forall ((@x7 Term))
           (! (implies
             (and
              (or label_1 (HasType @x7 Prims.unit))
              ;; def=FStar.LexicographicOrdering.fsti(75,10-75,43); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
              (or
               label_2
               ;; def=FStar.LexicographicOrdering.fsti(75,10-75,43); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
               (Valid
                ;; def=FStar.LexicographicOrdering.fsti(75,10-75,43); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
                (FStar.WellFounded.is_well_founded
                 (U_max a b)
                 (Prims.dtuple2
                  a
                  b
                  @x0
                  (WithType
                   ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
                   (Tm_lambda
                    @x0
                    ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
                    (lambda ((@x8 Term)) (ApplyTT @x1 @x8)))
                   (Tm_arrow_5b1c7f3f701f4c9bd877a4f9b4ec1dfa @x0 b a)))
                 (FStar.LexicographicOrdering.lex_t a b @x0 @x1 @x2 @x3)))))
             ;; def=Prims.fst(409,83-409,96); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
             (Valid
              ;; def=Prims.fst(409,83-409,96); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
              (ApplyTT @x6 @x7)))
            :pattern
             (;; def=Prims.fst(409,83-409,96); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
              (Valid
               ;; def=Prims.fst(409,83-409,96); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
               (ApplyTT @x6 @x7)))
            :qid @query.2)))
         ;; def=Prims.fst(322,2-322,58); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
         (forall ((@x7 Term))
          (! (implies
            (and
             (HasType @x7 (Tm_type (U_max a b)))
             ;; def=Prims.fst(322,26-322,41); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
             (=
              @x7
              (Prims.dtuple2
               a
               b
               @x0
               (WithType
                ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,37-76,45)
                (Tm_lambda
                 @x0
                 ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,37-76,45)
                 (lambda ((@x8 Term)) (ApplyTT @x1 @x8)))
                (Tm_arrow_5b1c7f3f701f4c9bd877a4f9b4ec1dfa @x0 b a)))))
            ;; def=Prims.fst(322,2-322,58); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
            (forall ((@x8 Term))
             (! (implies
               (and
                (HasType
                 @x8
                 (FStar.WellFounded.binrel
                  (U_max a b)
                  (Prims.dtuple2
                   a
                   b
                   @x0
                   (WithType
                    ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                    (Tm_lambda
                     @x0
                     ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                     (lambda ((@x9 Term)) (ApplyTT @x1 @x9)))
                    (Tm_arrow_5b1c7f3f701f4c9bd877a4f9b4ec1dfa @x0 b a)))))
                ;; def=Prims.fst(322,26-322,41); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
                (= @x8 (FStar.LexicographicOrdering.lex_t a b @x0 @x1 @x2 @x3)))
               ;; def=Prims.fst(322,2-322,58); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
               (forall ((@x9 Term))
                (! (implies
                  (and
                   (HasType
                    @x9
                    (FStar.WellFounded.well_founded
                     (U_max a b)
                     (Prims.dtuple2
                      a
                      b
                      @x0
                      (WithType
                       ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                       (Tm_lambda
                        @x0
                        ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                        (lambda ((@x10 Term)) (ApplyTT @x1 @x10)))
                       (Tm_arrow_5b1c7f3f701f4c9bd877a4f9b4ec1dfa @x0 b a)))
                     (FStar.LexicographicOrdering.lex_t a b @x0 @x1 @x2 @x3)))
                   ;; def=Prims.fst(322,26-322,41); use=FStar.LexicographicOrdering.fsti(76,4-76,56)
                   (= @x9 (FStar.LexicographicOrdering.lex_t_wf a b @x0 @x1 @x2 @x3 @x4 @x5)))
                  ;; def=Prims.fst(409,36-409,97); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                  (forall ((@x10 Term))
                   (! (implies
                     (and
                      (HasType @x10 Prims.unit)
                      ;; def=FStar.WellFounded.fst(113,10-113,29); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                      (Valid
                       ;; def=FStar.WellFounded.fst(113,10-113,29); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                       (FStar.WellFounded.is_well_founded
                        (U_max a b)
                        (Prims.dtuple2
                         a
                         b
                         @x0
                         (WithType
                          ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                          (Tm_lambda
                           @x0
                           ;; def=FStar.LexicographicOrdering.fsti(53,30-53,33); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                           (lambda ((@x11 Term)) (ApplyTT @x1 @x11)))
                          (Tm_arrow_5b1c7f3f701f4c9bd877a4f9b4ec1dfa @x0 b a)))
                        (FStar.LexicographicOrdering.lex_t a b @x0 @x1 @x2 @x3))))
                     ;; def=Prims.fst(409,83-409,96); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                     (Valid
                      ;; def=Prims.fst(409,83-409,96); use=FStar.LexicographicOrdering.fsti(76,4-76,35)
                      (ApplyTT @x6 @x10)))
                    :qid @query.6)))
                 :qid @query.5)))
              :qid @query.4)))
           :qid @query.3)))
        :qid @query.1)))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.List.Tot.Base-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   ;; def=FStar.List.Tot.Base.fst(570,0-574,65); use=FStar.List.Tot.Base.fst(570,0-574,65)
   (forall ((@x0 Term) (@x1 Term) (@x2 Term))
    (! (implies
      (and
       (HasType @x0 Prims.eqtype)
       (HasType @x1 (Tm_arrow_84543425b818e2d10a976186b8e8c250 @x0))
       ;; def=FStar.List.Tot.Base.fst(571,2-571,26); use=FStar.List.Tot.Base.fst(571,2-571,26)
       (HasType
        @x2
        ;; def=FStar.List.Tot.Base.fst(571,2-571,26); use=FStar.List.Tot.Base.fst(571,2-571,26)
        (Tm_refinement
         (Prims.list U_zero @x0)
         ;; def=FStar.List.Tot.Base.fst(571,2-571,26); use=FStar.List.Tot.Base.fst(571,2-571,26)
         (lambda ((@x3 Term))
          ;; def=FStar.List.Tot.Base.fst(571,13-571,24); use=FStar.List.Tot.Base.fst(571,13-571,24)
          (BoxBool_proj_0 (FStar.List.Tot.Base.for_all U_zero @x0 @x1 @x3))))))
      ;; def=FStar.List.Tot.Base.fst(570,18-574,65); use=FStar.List.Tot.Base.fst(570,18-574,65)
      (forall ((@x3 Term))
       (! (implies
         (HasType
          @x3
          (Prims.list
           U_zero
           ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(572,15-572,27)
           (Tm_refinement
            @x0
            ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(572,15-572,27)
            (lambda ((@x4 Term))
             ;; def=FStar.List.Tot.Base.fst(572,21-572,24); use=FStar.List.Tot.Base.fst(572,21-572,24)
             (BoxBool_proj_0 (ApplyTT @x1 @x4))))))
         ;; def=FStar.List.Tot.Base.fst(73,27-574,62); use=FStar.List.Tot.Base.fst(573,4-574,62)
         (and
          ;; def=Prims.fst(90,23-90,30); use=FStar.List.Tot.Base.fst(573,4-573,10)
          (or
           label_1
           ;; def=Prims.fst(90,23-90,30); use=FStar.List.Tot.Base.fst(573,4-573,10)
           (Valid
            ;; def=Prims.fst(90,23-90,30); use=FStar.List.Tot.Base.fst(573,4-573,10)
            (Prims.hasEq U_zero Prims.nat)))
          (implies
           ;; def=FStar.List.Tot.Base.fst(573,4-573,24); use=FStar.List.Tot.Base.fst(573,4-573,24)
           (=
            (FStar.List.Tot.Base.length U_zero @x0 @x2)
            (FStar.List.Tot.Base.length
             U_zero
             ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(573,22-573,24)
             (Tm_refinement
              @x0
              ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(573,22-573,24)
              (lambda ((@x4 Term))
               ;; def=FStar.List.Tot.Base.fst(572,21-572,24); use=FStar.List.Tot.Base.fst(573,22-573,24)
               (BoxBool_proj_0 (ApplyTT @x1 @x4))))
             @x3))
           ;; def=FStar.List.Tot.Base.fst(573,4-574,62); use=FStar.List.Tot.Base.fst(573,4-574,62)
           (forall ((@x4 Term))
            (! (implies
              ;; def=FStar.List.Tot.Base.fst(89,34-89,52); use=FStar.List.Tot.Base.fst(574,12-574,13)
              (HasType
               @x4
               ;; def=FStar.List.Tot.Base.fst(89,34-89,52); use=FStar.List.Tot.Base.fst(574,12-574,13)
               (Tm_refinement
                Prims.nat
                ;; def=FStar.List.Tot.Base.fst(89,34-89,52); use=FStar.List.Tot.Base.fst(574,12-574,13)
                (lambda ((@x5 Term))
                 ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,12-574,13)
                 (and
                  ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,12-574,13)
                  (< (BoxInt_proj_0 @x5) (BoxInt_proj_0 (FStar.List.Tot.Base.length U_zero @x0 @x2)))
                  ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,12-574,13)
                  (<
                   (BoxInt_proj_0 @x5)
                   (BoxInt_proj_0
                    (FStar.List.Tot.Base.length
                     U_zero
                     ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,12-574,13)
                     (Tm_refinement
                      @x0
                      ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,12-574,13)
                      (lambda ((@x6 Term))
                       ;; def=FStar.List.Tot.Base.fst(572,21-572,24); use=FStar.List.Tot.Base.fst(574,12-574,13)
                       (BoxBool_proj_0 (ApplyTT @x1 @x6))))
                     @x3)))))))
              ;; def=Prims.fst(427,77-427,89); use=FStar.List.Tot.Base.fst(574,4-574,62)
              (and
               (implies
                ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,47-574,48)
                (and
                 ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,47-574,48)
                 (< (BoxInt_proj_0 @x4) (BoxInt_proj_0 (FStar.List.Tot.Base.length U_zero @x0 @x2)))
                 ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,47-574,48)
                 (<
                  (BoxInt_proj_0 @x4)
                  (BoxInt_proj_0
                   (FStar.List.Tot.Base.length
                    U_zero
                    ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,47-574,48)
                    (Tm_refinement
                     @x0
                     ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,47-574,48)
                     (lambda ((@x5 Term))
                      ;; def=FStar.List.Tot.Base.fst(572,21-572,24); use=FStar.List.Tot.Base.fst(574,47-574,48)
                      (BoxBool_proj_0 (ApplyTT @x1 @x5))))
                    @x3))))
                ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,47-574,48)
                (or
                 label_2
                 ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,47-574,48)
                 (< (BoxInt_proj_0 @x4) (BoxInt_proj_0 (FStar.List.Tot.Base.length U_zero @x0 @x2)))))
               ;; def=Prims.fst(419,66-419,102); use=FStar.List.Tot.Base.fst(574,4-574,62)
               (forall ((@x5 Term))
                (! (implies
                  (and
                   ;; def=FStar.List.Tot.Base.fst(89,34-89,52); use=FStar.List.Tot.Base.fst(574,4-574,62)
                   (HasType
                    @x5
                    ;; def=FStar.List.Tot.Base.fst(89,34-89,52); use=FStar.List.Tot.Base.fst(574,4-574,62)
                    (Tm_refinement
                     Prims.nat
                     ;; def=FStar.List.Tot.Base.fst(89,34-89,52); use=FStar.List.Tot.Base.fst(574,4-574,62)
                     (lambda ((@x6 Term))
                      ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,4-574,62)
                      (and
                       ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,4-574,62)
                       (<
                        (BoxInt_proj_0 @x6)
                        (BoxInt_proj_0 (FStar.List.Tot.Base.length U_zero @x0 @x2)))
                       ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,4-574,62)
                       (<
                        (BoxInt_proj_0 @x6)
                        (BoxInt_proj_0
                         (FStar.List.Tot.Base.length
                          U_zero
                          ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,4-574,62)
                          (Tm_refinement
                           @x0
                           ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,4-574,62)
                           (lambda ((@x7 Term))
                            ;; def=FStar.List.Tot.Base.fst(572,21-572,24); use=FStar.List.Tot.Base.fst(574,4-574,62)
                            (BoxBool_proj_0 (ApplyTT @x1 @x7))))
                          @x3)))))))
                   ;; def=FStar.List.Tot.Base.fst(89,34-574,13); use=FStar.List.Tot.Base.fst(574,4-574,62)
                   (= @x4 @x5))
                  ;; def=Prims.fst(419,66-419,102); use=FStar.List.Tot.Base.fst(574,4-574,62)
                  (forall ((@x6 Term))
                   (! (implies
                     (and
                      (HasType @x6 @x0)
                      ;; def=FStar.List.Tot.Base.fst(574,4-574,62); use=FStar.List.Tot.Base.fst(574,4-574,62)
                      (= (FStar.List.Tot.Base.index U_zero @x0 @x2 @x4) @x6)
                      ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,60-574,61)
                      (<
                       (BoxInt_proj_0 @x4)
                       (BoxInt_proj_0 (FStar.List.Tot.Base.length U_zero @x0 @x2)))
                      ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,60-574,61)
                      (<
                       (BoxInt_proj_0 @x4)
                       (BoxInt_proj_0
                        (FStar.List.Tot.Base.length
                         U_zero
                         ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,60-574,61)
                         (Tm_refinement
                          @x0
                          ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,60-574,61)
                          (lambda ((@x7 Term))
                           ;; def=FStar.List.Tot.Base.fst(572,21-572,24); use=FStar.List.Tot.Base.fst(574,60-574,61)
                           (BoxBool_proj_0 (ApplyTT @x1 @x7))))
                         @x3))))
                     ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,60-574,61)
                     (or
                      label_3
                      ;; def=FStar.List.Tot.Base.fst(89,40-89,52); use=FStar.List.Tot.Base.fst(574,60-574,61)
                      (<
                       (BoxInt_proj_0 @x4)
                       (BoxInt_proj_0
                        (FStar.List.Tot.Base.length
                         U_zero
                         ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,60-574,61)
                         (Tm_refinement
                          @x0
                          ;; def=FStar.List.Tot.Base.fst(572,15-572,27); use=FStar.List.Tot.Base.fst(574,60-574,61)
                          (lambda ((@x7 Term))
                           ;; def=FStar.List.Tot.Base.fst(572,21-572,24); use=FStar.List.Tot.Base.fst(574,60-574,61)
                           (BoxBool_proj_0 (ApplyTT @x1 @x7))))
                         @x3)))))
                    :qid @query.4)))
                 :qid @query.3))))
             :qid @query.2)))))
        :qid @query.1)))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_3")
(eval label_3)
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.Map-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   (forall ((@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term) (@x4 Term))
    (! (implies
      (and
       (HasType @x0 Prims.eqtype)
       (HasType @x1 (Tm_type uu___92))
       (HasType @x2 (FStar.Map.t uu___92 @x0 @x1))
       (HasType @x3 @x0)
       (HasType @x4 @x1))
      ;; def=Prims.fst(373,4-373,44); use=Prims.fst(398,19-398,32)
      (forall ((@x5 Term))
       (! (implies
         (and
          (HasType @x5 (Prims.pure_post U_zero Prims.unit))
          ;; def=Prims.fst(409,36-409,97); use=FStar.Map.fst(79,45-79,47)
          (forall ((@x6 Term))
           (! (implies
             (and
              (or label_1 (HasType @x6 Prims.unit))
              ;; def=FStar.Map.fsti(96,50-96,74); use=FStar.Map.fst(79,45-79,47)
              (or
               label_2
               ;; def=FStar.Map.fsti(96,50-96,74); use=FStar.Map.fst(79,45-79,47)
               (=
                (FStar.Map.sel uu___92 @x0 @x1 (FStar.Map.upd uu___92 @x0 @x1 @x2 @x3 @x4) @x3)
                @x4)))
             ;; def=Prims.fst(409,83-409,96); use=FStar.Map.fst(79,45-79,47)
             (Valid
              ;; def=Prims.fst(409,83-409,96); use=FStar.Map.fst(79,45-79,47)
              (ApplyTT @x5 @x6)))
            :pattern
             (;; def=Prims.fst(409,83-409,96); use=FStar.Map.fst(79,45-79,47)
              (Valid
               ;; def=Prims.fst(409,83-409,96); use=FStar.Map.fst(79,45-79,47)
               (ApplyTT @x5 @x6)))
            :qid @query.2)))
         ;; def=Prims.fst(419,66-419,102); use=Prims.fst(422,31-422,44)
         (forall ((@x6 Term))
          (! (implies
            (HasType @x6 Prims.unit)
            ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
            (Valid
             ;; def=Prims.fst(419,90-419,102); use=Prims.fst(422,31-422,44)
             (ApplyTT @x5 @x6)))
           :qid @query.3)))
        :qid @query.1)))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.Math.Lemmas-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   ;; def=FStar.Math.Lemmas.fsti(228,0-230,20); use=FStar.Math.Lemmas.fsti(228,0-230,20)
   (forall ((@x0 Term) (@x1 Term) (@x2 Term))
    (! (implies
      (and (HasType @x0 Prims.pos) (HasType @x1 Prims.nat) (HasType @x2 Prims.nat))
      ;; def=Prims.fst(427,77-427,89); use=FStar.Math.Lemmas.fsti(228,27-230,20)
      (and
       (implies
        ;; def=FStar.Math.Lemmas.fsti(229,13-229,27); use=FStar.Math.Lemmas.fsti(229,13-229,27)
        (and
         ;; def=FStar.Math.Lemmas.fsti(229,13-229,18); use=FStar.Math.Lemmas.fsti(229,13-229,18)
         (< (BoxInt_proj_0 @x1) (BoxInt_proj_0 @x0))
         ;; def=FStar.Math.Lemmas.fsti(229,22-229,27); use=FStar.Math.Lemmas.fsti(229,22-229,27)
         (< (BoxInt_proj_0 @x2) (BoxInt_proj_0 @x0)))
        ;; def=Prims.fst(427,77-427,89); use=FStar.Math.Lemmas.fsti(229,12-229,45)
        (and
         (implies
          ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(229,35-229,36)
          (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0)))
          ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(229,35-229,36)
          (or
           label_1
           ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(229,35-229,36)
           (not (= @x0 (BoxInt 0)))))
         ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(229,12-229,45)
         (forall ((@x3 Term))
          (! (implies
            (and
             (HasType @x3 Prims.pos)
             ;; def=FStar.Math.Lemmas.fsti(229,12-229,45); use=FStar.Math.Lemmas.fsti(229,12-229,45)
             (= @x0 @x3))
            ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(229,12-229,45)
            (forall ((@x4 Term))
             (! (implies
               (and
                (HasType @x4 Prims.int)
                ;; def=FStar.Math.Lemmas.fsti(229,12-229,45); use=FStar.Math.Lemmas.fsti(229,12-229,45)
                (= (Prims.op_Modulus @x1 @x0) @x4)
                ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(229,43-229,44)
                (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0))))
               ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(229,43-229,44)
               (or
                label_2
                ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(229,43-229,44)
                (not (= @x0 (BoxInt 0)))))
              :qid @query.2)))
           :qid @query.1))))
       ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(228,27-230,20)
       (forall ((@x3 Term))
        (! (implies
          (and
           (HasType @x3 Prims.prop)
           ;; def=FStar.Pervasives.fsti(112,28-112,31); use=FStar.Math.Lemmas.fsti(228,27-230,20)
           (=
            (Prims.l_and
             (Prims.l_and
              (Prims.b2t (Prims.op_LessThan @x1 @x0))
              (Prims.b2t (Prims.op_LessThan @x2 @x0)))
             (Prims.b2t
              (Prims.op_Equality Prims.int (Prims.op_Modulus @x1 @x0) (Prims.op_Modulus @x2 @x0))))
            @x3))
          ;; def=FStar.Math.Lemmas.fsti(228,27-230,20); use=FStar.Math.Lemmas.fsti(228,27-230,20)
          (and
           (implies
            ;; def=FStar.Math.Lemmas.fsti(229,13-229,27); use=FStar.Math.Lemmas.fsti(230,12-230,19)
            (and
             ;; def=FStar.Math.Lemmas.fsti(229,13-229,18); use=FStar.Math.Lemmas.fsti(230,12-230,19)
             (< (BoxInt_proj_0 @x1) (BoxInt_proj_0 @x0))
             ;; def=FStar.Math.Lemmas.fsti(229,22-229,27); use=FStar.Math.Lemmas.fsti(230,12-230,19)
             (< (BoxInt_proj_0 @x2) (BoxInt_proj_0 @x0)))
            ;; def=Prims.fst(427,77-427,89); use=FStar.Math.Lemmas.fsti(230,12-230,19)
            (and
             (implies
              ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(230,12-230,19)
              (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0)))
              ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(229,35-229,36)
              (or
               label_3
               ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(230,12-230,19)
               (not (= @x0 (BoxInt 0)))))
             ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(230,12-230,19)
             (forall ((@x4 Term))
              (! (implies
                (and
                 (HasType @x4 Prims.pos)
                 ;; def=FStar.Math.Lemmas.fsti(228,52-228,57); use=FStar.Math.Lemmas.fsti(230,12-230,19)
                 (= @x0 @x4))
                ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(230,12-230,19)
                (forall ((@x5 Term))
                 (! (implies
                   (and
                    (HasType @x5 Prims.int)
                    ;; def=FStar.Math.Lemmas.fsti(228,52-228,57); use=FStar.Math.Lemmas.fsti(230,12-230,19)
                    (= (Prims.op_Modulus @x1 @x0) @x5)
                    ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(230,12-230,19)
                    (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0))))
                   ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(229,43-229,44)
                   (or
                    label_4
                    ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(230,12-230,19)
                    (not (= @x0 (BoxInt 0)))))
                  :qid @query.5)))
               :qid @query.4))))
           ;; def=FStar.Math.Lemmas.fsti(228,27-230,20); use=FStar.Math.Lemmas.fsti(228,27-230,20)
           (forall ((@x4 Term))
            (! (implies
              (and
               (HasType @x4 Prims.unit)
               ;; def=FStar.Math.Lemmas.fsti(229,13-229,18); use=FStar.Math.Lemmas.fsti(228,52-228,57)
               (< (BoxInt_proj_0 @x1) (BoxInt_proj_0 @x0))
               ;; def=FStar.Math.Lemmas.fsti(229,22-229,27); use=FStar.Math.Lemmas.fsti(228,52-228,57)
               (< (BoxInt_proj_0 @x2) (BoxInt_proj_0 @x0))
               ;; def=FStar.Math.Lemmas.fsti(229,31-229,44); use=FStar.Math.Lemmas.fsti(228,52-228,57)
               (= (Prims.op_Modulus @x1 @x0) (Prims.op_Modulus @x2 @x0)))
              ;; def=Prims.fst(90,23-90,30); use=FStar.Math.Lemmas.fsti(230,13-230,14)
              (or
               label_5
               ;; def=Prims.fst(90,23-90,30); use=FStar.Math.Lemmas.fsti(230,13-230,14)
               (Valid
                ;; def=Prims.fst(90,23-90,30); use=FStar.Math.Lemmas.fsti(230,13-230,14)
                (Prims.hasEq U_zero Prims.nat))))
             :qid @query.6))))
         :qid @query.3))))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_5")
(eval label_5)
(echo "label_4")
(eval label_4)
(echo "label_3")
(eval label_3)
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.Math.Lemmas-2.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   ;; def=FStar.Math.Lemmas.fsti(398,0-400,18); use=FStar.Math.Lemmas.fsti(398,0-400,18)
   (forall ((@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))
    (! (implies
      (and
       (HasType @x0 Prims.pos)
       (HasType @x1 Prims.int)
       (HasType @x2 Prims.nat)
       (HasType @x3 Prims.nat))
      ;; def=Prims.fst(427,77-427,89); use=FStar.Math.Lemmas.fsti(398,32-400,18)
      (and
       (implies
        ;; def=FStar.Math.Lemmas.fsti(399,12-399,26); use=FStar.Math.Lemmas.fsti(399,12-399,26)
        (and
         ;; def=FStar.Math.Lemmas.fsti(399,12-399,17); use=FStar.Math.Lemmas.fsti(399,12-399,17)
         (< (BoxInt_proj_0 @x2) (BoxInt_proj_0 @x0))
         ;; def=FStar.Math.Lemmas.fsti(399,21-399,26); use=FStar.Math.Lemmas.fsti(399,21-399,26)
         (< (BoxInt_proj_0 @x3) (BoxInt_proj_0 @x0)))
        ;; def=Prims.fst(427,77-427,89); use=FStar.Math.Lemmas.fsti(399,12-399,55)
        (and
         (implies
          ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(399,40-399,41)
          (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0)))
          ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(399,40-399,41)
          (or
           label_1
           ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(399,40-399,41)
           (not (= @x0 (BoxInt 0)))))
         ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(399,12-399,55)
         (forall ((@x4 Term))
          (! (implies
            (and
             (HasType @x4 Prims.pos)
             ;; def=FStar.Math.Lemmas.fsti(399,12-399,55); use=FStar.Math.Lemmas.fsti(399,12-399,55)
             (= @x0 @x4))
            ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(399,12-399,55)
            (forall ((@x5 Term))
             (! (implies
               (and
                (HasType @x5 Prims.int)
                ;; def=FStar.Math.Lemmas.fsti(399,12-399,55); use=FStar.Math.Lemmas.fsti(399,12-399,55)
                (= (Prims.op_Modulus (Prims.op_Addition @x1 @x2) @x0) @x5)
                ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(399,54-399,55)
                (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0))))
               ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(399,54-399,55)
               (or
                label_2
                ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(399,54-399,55)
                (not (= @x0 (BoxInt 0)))))
              :qid @query.2)))
           :qid @query.1))))
       ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(398,32-400,18)
       (forall ((@x4 Term))
        (! (implies
          (and
           (HasType @x4 Prims.prop)
           ;; def=FStar.Pervasives.fsti(112,28-112,31); use=FStar.Math.Lemmas.fsti(398,32-400,18)
           (=
            (Prims.l_and
             (Prims.l_and
              (Prims.b2t (Prims.op_LessThan @x2 @x0))
              (Prims.b2t (Prims.op_LessThan @x3 @x0)))
             (Prims.b2t
              (Prims.op_Equality
               Prims.int
               (Prims.op_Modulus (Prims.op_Addition @x1 @x2) @x0)
               (Prims.op_Modulus (Prims.op_Addition @x1 @x3) @x0))))
            @x4))
          ;; def=FStar.Math.Lemmas.fsti(398,32-400,18); use=FStar.Math.Lemmas.fsti(398,32-400,18)
          (and
           (implies
            ;; def=FStar.Math.Lemmas.fsti(399,12-399,26); use=FStar.Math.Lemmas.fsti(400,12-400,17)
            (and
             ;; def=FStar.Math.Lemmas.fsti(399,12-399,17); use=FStar.Math.Lemmas.fsti(400,12-400,17)
             (< (BoxInt_proj_0 @x2) (BoxInt_proj_0 @x0))
             ;; def=FStar.Math.Lemmas.fsti(399,21-399,26); use=FStar.Math.Lemmas.fsti(400,12-400,17)
             (< (BoxInt_proj_0 @x3) (BoxInt_proj_0 @x0)))
            ;; def=Prims.fst(427,77-427,89); use=FStar.Math.Lemmas.fsti(400,12-400,17)
            (and
             (implies
              ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(400,12-400,17)
              (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0)))
              ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(399,40-399,41)
              (or
               label_3
               ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(400,12-400,17)
               (not (= @x0 (BoxInt 0)))))
             ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(400,12-400,17)
             (forall ((@x5 Term))
              (! (implies
                (and
                 (HasType @x5 Prims.pos)
                 ;; def=FStar.Math.Lemmas.fsti(398,63-398,68); use=FStar.Math.Lemmas.fsti(400,12-400,17)
                 (= @x0 @x5))
                ;; def=Prims.fst(419,66-419,102); use=FStar.Math.Lemmas.fsti(400,12-400,17)
                (forall ((@x6 Term))
                 (! (implies
                   (and
                    (HasType @x6 Prims.int)
                    ;; def=FStar.Math.Lemmas.fsti(398,63-398,68); use=FStar.Math.Lemmas.fsti(400,12-400,17)
                    (= (Prims.op_Modulus (Prims.op_Addition @x1 @x2) @x0) @x6)
                    ;; def=Prims.fst(645,18-645,23); use=FStar.Math.Lemmas.fsti(400,12-400,17)
                    (> (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0))))
                   ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(399,54-399,55)
                   (or
                    label_4
                    ;; def=Prims.fst(648,22-648,28); use=FStar.Math.Lemmas.fsti(400,12-400,17)
                    (not (= @x0 (BoxInt 0)))))
                  :qid @query.5)))
               :qid @query.4))))
           ;; def=FStar.Math.Lemmas.fsti(398,32-400,18); use=FStar.Math.Lemmas.fsti(398,32-400,18)
           (forall ((@x5 Term))
            (! (implies
              (and
               (HasType @x5 Prims.unit)
               ;; def=FStar.Math.Lemmas.fsti(399,12-399,17); use=FStar.Math.Lemmas.fsti(398,63-398,68)
               (< (BoxInt_proj_0 @x2) (BoxInt_proj_0 @x0))
               ;; def=FStar.Math.Lemmas.fsti(399,21-399,26); use=FStar.Math.Lemmas.fsti(398,63-398,68)
               (< (BoxInt_proj_0 @x3) (BoxInt_proj_0 @x0))
               ;; def=FStar.Math.Lemmas.fsti(399,30-399,55); use=FStar.Math.Lemmas.fsti(398,63-398,68)
               (=
                (Prims.op_Modulus (Prims.op_Addition @x1 @x2) @x0)
                (Prims.op_Modulus (Prims.op_Addition @x1 @x3) @x0)))
              ;; def=Prims.fst(90,23-90,30); use=FStar.Math.Lemmas.fsti(400,12-400,13)
              (or
               label_5
               ;; def=Prims.fst(90,23-90,30); use=FStar.Math.Lemmas.fsti(400,12-400,13)
               (Valid
                ;; def=Prims.fst(90,23-90,30); use=FStar.Math.Lemmas.fsti(400,12-400,13)
                (Prims.hasEq U_zero Prims.nat))))
             :qid @query.6))))
         :qid @query.3))))
     :qid @query)))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_5")
(eval label_5)
(echo "label_4")
(eval label_4)
(echo "label_3")
(eval label_3)
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

`failedQueries-FStar.Monotonic.Pure-1.smt2`

; Z3 invocation started by F*
; F* version: 2026.05.24~dev -- commit hash: 848d63ad4a10703c2424e293c4023c0e868d2b1a
; Z3 version (according to F*): 4.17.0

(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   (forall ((@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))
    (! (implies
      (and
       (HasType @x0 (Tm_type uu___79))
       (HasType @x1 (Prims.pure_wp uu___79 @x0))
       (HasType @x2 (Tm_arrow_5de678b343d19ca92349d23b50680e9e @x1 @x0 uu___79))
       (HasType @x3 (Prims.pure_post uu___79 @x0)))
      ;; def=Prims.fst(373,4-373,44); use=Prims.fst(398,19-398,32)
      (forall ((@x4 Term))
       (! (implies
         (and
          (HasType @x4 (Prims.pure_post uu___79 @x0))
          ;; def=FStar.Monotonic.Pure.fst(63,21-63,27); use=FStar.Monotonic.Pure.fst(64,4-65,8)
          (Valid
           ;; def=FStar.Monotonic.Pure.fst(63,21-63,27); use=FStar.Monotonic.Pure.fst(64,4-65,8)
           (ApplyTT @x1 @x3))
          ;; def=Prims.fst(409,36-409,97); use=FStar.Monotonic.Pure.fst(64,4-65,8)
          (forall ((@x5 Term))
           (! (implies
             (and
              (or label_1 (HasType @x5 @x0))
              ;; def=FStar.Monotonic.Pure.fst(63,48-63,51); use=FStar.Monotonic.Pure.fst(64,4-65,8)
              (or
               label_2
               ;; def=FStar.Monotonic.Pure.fst(63,48-63,51); use=FStar.Monotonic.Pure.fst(64,4-65,8)
               (Valid
                ;; def=FStar.Monotonic.Pure.fst(63,48-63,51); use=FStar.Monotonic.Pure.fst(64,4-65,8)
                (ApplyTT @x3 @x5))))
             ;; def=Prims.fst(409,83-409,96); use=FStar.Monotonic.Pure.fst(64,4-65,8)
             (Valid
              ;; def=Prims.fst(409,83-409,96); use=FStar.Monotonic.Pure.fst(64,4-65,8)
              (ApplyTT @x4 @x5)))
            :pattern
             (;; def=Prims.fst(409,83-409,96); use=FStar.Monotonic.Pure.fst(64,4-65,8)
              (Valid
               ;; def=Prims.fst(409,83-409,96); use=FStar.Monotonic.Pure.fst(64,4-65,8)
               (ApplyTT @x4 @x5)))
            :qid @query.2)))
         ;; def=Prims.fst(409,36-409,97); use=FStar.Monotonic.Pure.fst(64,4-64,29)
         (forall ((@x5 Term))
          (! (implies
            (and
             (HasType @x5 Prims.unit)
             ;; def=FStar.Monotonic.Pure.fst(34,2-34,75); use=FStar.Monotonic.Pure.fst(64,4-65,8)
             (forall ((@x6 Term) (@x7 Term))
              (! (implies
                (and
                 (HasType @x6 (Prims.pure_post uu___79 @x0))
                 (HasType @x7 (Prims.pure_post uu___79 @x0))
                 ;; def=FStar.Monotonic.Pure.fst(34,28-34,55); use=FStar.Monotonic.Pure.fst(64,4-65,8)
                 (forall ((@x8 Term))
                  (! (implies
                    (and
                     (HasType @x8 @x0)
                     ;; def=FStar.Monotonic.Pure.fst(34,43-34,46); use=FStar.Monotonic.Pure.fst(64,4-65,8)
                     (Valid
                      ;; def=FStar.Monotonic.Pure.fst(34,43-34,46); use=FStar.Monotonic.Pure.fs

... (truncated due to discussion size limits)

### Run
- Workflow run: https://github.com/Z3Prover/z3/actions/runs/27211368950

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

FStar build with configurable Z3 inputs — 2026-06-09 #9794

Uh oh!

{{title}}

Uh oh!

Replies: 0 comments

Select a reply

Uh oh!

FStar build with configurable Z3 inputs — 2026-06-09 #9794

Uh oh!

github-actions[bot] Bot Jun 9, 2026

Build status

Inputs used

Produced versions

Generated SMT2 files

failedQueries-FStar.Algebra.Monoid-1.smt2

failedQueries-FStar.DependentMap-1.smt2

failedQueries-FStar.GSet-1.smt2

failedQueries-FStar.GhostSet-1.smt2

failedQueries-FStar.LexicographicOrdering-1.smt2

failedQueries-FStar.List.Tot.Base-1.smt2

failedQueries-FStar.Map-1.smt2

failedQueries-FStar.Math.Lemmas-1.smt2

failedQueries-FStar.Math.Lemmas-2.smt2

failedQueries-FStar.Monotonic.Pure-1.smt2

Replies: 0 comments

github-actions[bot]
Bot Jun 9, 2026

`failedQueries-FStar.Algebra.Monoid-1.smt2`

`failedQueries-FStar.DependentMap-1.smt2`

`failedQueries-FStar.GSet-1.smt2`

`failedQueries-FStar.GhostSet-1.smt2`

`failedQueries-FStar.LexicographicOrdering-1.smt2`

`failedQueries-FStar.List.Tot.Base-1.smt2`

`failedQueries-FStar.Map-1.smt2`

`failedQueries-FStar.Math.Lemmas-1.smt2`

`failedQueries-FStar.Math.Lemmas-2.smt2`

`failedQueries-FStar.Monotonic.Pure-1.smt2`