FStar build with configurable Z3 inputs — 2026-09-04

[github-actions[bot]]

Build status

• ✅ Z3 build completed
• ✅ FStar build completed
• ⚠️ FStar test suite (make test) failure (pipeline continued)

Inputs used

• z3_ref: master
• z3_cmake_args: ``
• z3_runtime_args: smt.ho_matching=false
• fstar_ref: master
• fstar_opam_switch: 4.14.2
• fstar_otherflags: --log_failing_queries --proof_recovery
• fstar_run_tests: true
• effective OTHERFLAGS: --z3version 5.1.0 --log_failing_queries --proof_recovery

Produced versions

• Z3: Z3 version 5.1.0 - 64 bit - build hashcode 0d4a2dbb188dd2034f0a820272dc945f64af50dc
• FStar: F* 2026.08.30~dev
• FStar commit: 52f17ab8fdea379708a659a1b02c8f8b47f877fa

Failing tests

Mismatched expected outputs: 104
  pulse/test/_output/LoopInvariants.fst.output
  pulse/test/_output/MatchBasic.fst.output
  pulse/test/_output/Test.Recursion.fst.output
  pulse/test/bug-reports/_output/Bug100.fst.output
  pulse/test/bug-reports/_output/Bug206.fst.output
  pulse/test/bug-reports/_output/Bug266.fst.output
  pulse/test/bug-reports/_output/Bug267.fst.output
  pulse/test/bug-reports/_output/Bug59.fst.output
  pulse/test/bug-reports/_output/Bug94.fst.output
  pulse/test/error_messages/_output/AssertExtraContext.fst.output
  pulse/test/error_messages/_output/ClosureError.fst.output
  pulse/test/error_messages/_output/ExistsIntro.fst.output
  pulse/test/error_messages/_output/FoldError.fst.output
  pulse/test/error_messages/_output/IfBranchMismatch.fst.output
  pulse/test/error_messages/_output/IllTypedInvariant.fst.output
  pulse/test/error_messages/_output/IntroExistsFail.fst.output
  pulse/test/error_messages/_output/InvariantPayload.fst.output
  pulse/test/error_messages/_output/MatchBranchMismatch.fst.output
  pulse/test/error_messages/_output/MultiError.fst.output
  pulse/test/error_messages/_output/NestedBlock.fst.output
  pulse/test/error_messages/_output/NestedCall.fst.output
  pulse/test/error_messages/_output/PrePostMismatch.fst.output
  pulse/test/error_messages/_output/ReturnImplicit.fst.output
  pulse/test/error_messages/_output/RewriteFail.fst.output
  pulse/test/error_messages/_output/SequenceError.fst.output
  pulse/test/error_messages/_output/SubtypingFailure.fst.output
  pulse/test/error_messages/_output/TerminalActionPostConditionMismatch.fst.output
  pulse/test/error_messages/_output/WhileInvPreservation.fst.output
  pulse/test/nolib/_output/Bug416.fst.output
  pulse/test/nolib/_output/MatchRange.fst.output
  tests/bug-reports/closed/_output/Bug3980.fst.output
  tests/error-messages/_output/ArrowRanges.fst.json_output
  tests/error-messages/_output/ArrowRanges.fst.output
  tests/error-messages/_output/AssertNorm.fst.json_output
  tests/error-messages/_output/AssertNorm.fst.output
  tests/error-messages/_output/Asserts.fst.json_output
  tests/error-messages/_output/Asserts.fst.output
  tests/error-messages/_output/Basic.fst.json_output
  tests/error-messages/_output/Basic.fst.output
  tests/error-messages/_output/Bug1997.fst.json_output
  tests/error-messages/_output/Bug1997.fst.output
  tests/error-messages/_output/Bug446.fst.json_output
  tests/error-messages/_output/Bug446.fst.output
  tests/error-messages/_output/Calc.fst.json_output
  tests/error-messages/_output/Calc.fst.output
  tests/error-messages/_output/Coercions.fst.json_output
  tests/error-messages/_output/Coercions.fst.output
  tests/error-messages/_output/ExpectFailure.fst.json_output
  tests/error-messages/_output/ExpectFailure.fst.output
  tests/error-messages/_output/NegativeTests.BST.fst.json_output
  tests/error-messages/_output/NegativeTests.BST.fst.output
  tests/error-messages/_output/NegativeTests.Bug260.fst.json_output
  tests/error-messages/_output/NegativeTests.Bug260.fst.output
  tests/error-messages/_output/NegativeTests.False.fst.json_output
  tests/error-messages/_output/NegativeTests.False.fst.output
  tests/error-messages/_output/NegativeTests.Neg.fst.json_output
  tests/error-messages/_output/NegativeTests.Neg.fst.output
  tests/error-messages/_output/NegativeTests.Set.fst.json_output
  tests/error-messages/_output/NegativeTests.Set.fst.output
  tests/error-messages/_output/NegativeTests.ShortCircuiting.fst.json_output
  tests/error-messages/_output/NegativeTests.ShortCircuiting.fst.output
  tests/error-messages/_output/NegativeTests.Termination.fst.json_output
  tests/error-messages/_output/NegativeTests.Termination.fst.output
  tests/error-messages/_output/NegativeTests.ZZImplicitFalse.fst.json_output
  tests/error-messages/_output/NegativeTests.ZZImplicitFalse.fst.output
  tests/error-messages/_output/Nonempty.fst.json_output
  tests/error-messages/_output/Nonempty.fst.output
  tests/error-messages/_output/OptionStack.fst.json_output
  tests/error-messages/_output/OptionStack.fst.output
  tests/error-messages/_output/PatAnnot.fst.json_output
  tests/error-messages/_output/PatAnnot.fst.output
  tests/error-messages/_output/PatternMatch.fst.json_output
  tests/error-messages/_output/PatternMatch.fst.output
  tests/error-messages/_output/PostconditionLocalization.fst.json_output
  tests/error-messages/_output/PostconditionLocalization.fst.output
  tests/error-messages/_output/QuickTest.fst.json_output
  tests/error-messages/_output/QuickTest.fst.output
  tests/error-messages/_output/QuickTestNBE.fst.json_output
  tests/error-messages/_output/QuickTestNBE.fst.output
  tests/error-messages/_output/StrictUnfolding.fst.json_output
  tests/error-messages/_output/StrictUnfolding.fst.output
  tests/error-messages/_output/StringNormalization.fst.json_output
  tests/error-messages/_output/StringNormalization.fst.output
  tests/error-messages/_output/Test.FunctionalExtensionality.fst.json_output
  tests/error-messages/_output/Test.FunctionalExtensionality.fst.output
  tests/error-messages/_output/TestErrorLocations.fst.json_output
  tests/error-messages/_output/TestErrorLocations.fst.output
  tests/error-messages/_output/TestHasEq.fst.json_output
  tests/error-messages/_output/TestHasEq.fst.output
  tests/error-messages/_output/Unit2.fst.json_output
  tests/error-messages/_output/Unit2.fst.output
  tests/error-messages/_output/WPExtensionality.fst.json_output
  tests/error-messages/_output/WPExtensionality.fst.output
  tests/ide/emacs/_output/Backtracking.refinements.ideout
  tests/ide/emacs/_output/Harness.selfref.ideout
  tests/ide/emacs/_output/Integration.push-pop.ideout
  tests/ide/emacs/_output/Number.interface-violation-and-fix.ideout
  tests/ide/emacs/_output/Number.interface-violation.ideout
  tests/interfaces/_output/IfaceNoPragmaLeak.fst.json_output
  tests/interfaces/_output/IfaceNoPragmaLeak.fst.output
  tests/interfaces/_output/IfaceNoSmtLeak.fst.json_output
  tests/int
... (truncated, see artifact logs/failing-tests.txt)

Generated SMT2 files

• Artifact (logs, failing .smt2 queries, and mismatched test outputs with diffs): https://github.com/Z3Prover/z3/actions/runs/33836732499/artifacts/9924545887

First 1000 lines per generated .smt2 file:

doc/book/code/failedQueries-Divergence-1.smt2

; Z3 invocation started by F*
; F* version: 2026.08.30~dev -- commit hash: 52f17ab8fdea379708a659a1b02c8f8b47f877fa
; Z3 version (according to F*): 5.1.0

(set-option :global-decls false)
(set-option :smt.mbqi false)
(set-option :auto_config false)
(set-option :model true)
(set-option :smt.case_split 3)
(set-option :smt.relevancy 2)
(set-option :rewriter.enable_der false)
(set-option :rewriter.sort_disjunctions false)
(set-option :pi.decompose_patterns false)
(set-option :smt.arith.solver 6)
(set-option :smt.random-seed 0)


(declare-sort FString)
(declare-fun FString_constr_id (FString) Int)

(declare-sort Term)
(declare-sort Universe)
(declare-fun U_zero () Universe)
(declare-fun U_succ (Universe) Universe)
(declare-fun ulevel ((Universe)) Int)
(declare-fun Univ (Int) Universe)
(assert (= (ulevel U_zero) 0))
(assert (forall ((u Universe)) (! (= (ulevel (U_succ u)) (+ 1 (ulevel u))) :pattern ((ulevel (U_succ u))))))
(assert (forall ((u Universe)) (! (>= (ulevel u) 0) :pattern ((ulevel u)))))
(assert (forall ((u Universe)) (! (= (Univ (ulevel u)) u) :pattern ((ulevel u)))))
(assert (forall ((i Int)) (! (implies (>= i 0) (= (ulevel (Univ i)) i)) :pattern ((Univ i)))))
(declare-fun U_max (Universe Universe) Universe)
(assert (forall ((u1 Universe) (u2 Universe))
(! (= (U_max u1 u2)
(ite (<= (ulevel u1) (ulevel u2)) u2 u1))
:pattern ((U_max u1 u2)))))
(declare-fun U_unif (Int) Universe)
(declare-fun U_unknown () Universe)
(declare-fun Term_constr_id (Term) Int)
(declare-sort Dummy_sort)
(declare-fun Dummy_value () Dummy_sort)
(declare-datatypes () ((Fuel 
(ZFuel) 
(SFuel (prec Fuel)))))
(declare-fun MaxIFuel () Fuel)
(declare-fun MaxFuel () Fuel)
(declare-fun PreType (Term) Term)
(declare-fun Valid (Term) Bool)
(declare-fun HasTypeFuel (Fuel Term Term) Bool)
(define-fun HasTypeZ ((x Term) (t Term)) Bool
(HasTypeFuel ZFuel x t))
(define-fun HasType ((x Term) (t Term)) Bool
(HasTypeFuel MaxIFuel x t))
(declare-fun IsTotFun (Term) Bool)

                ;;fuel irrelevance
(assert (forall ((f Fuel) (x Term) (t Term))
(! (= (HasTypeFuel (SFuel f) x t)
(HasTypeZ x t))
:pattern ((HasTypeFuel (SFuel f) x t)))))
(declare-fun NoHoist (Term Bool) Bool)
;;no-hoist
(assert (forall ((dummy Term) (b Bool))
(! (= (NoHoist dummy b) b)
:pattern ((NoHoist dummy b)))))
(define-fun  IsTyped ((x Term)) Bool
(exists ((t Term)) (HasTypeZ x t)))
(declare-fun ApplyTF (Term Fuel) Term)
(declare-fun ApplyTT (Term Term) Term)
(declare-fun Prec (Term Term) Bool)
(assert (forall ((x Term) (y Term) (z Term))
(! (implies (and (Prec x y) (Prec y z)) (Prec x z))
:pattern ((Prec x z) (Prec x y)))))
(assert (forall ((x Term) (y Term))
(implies (Prec x y)
(not (Prec y x)))))
(declare-fun Closure (Term) Term)
(declare-fun ConsTerm (Term Term) Term)
(declare-fun ConsFuel (Fuel Term) Term)
(declare-fun Tm_uvar (Int) Term)
(define-fun Reify ((x Term)) Term x)
(declare-fun Prims.precedes (Universe Universe Term Term Term Term) Term)
(declare-fun Range_const (Int) Term)
(declare-fun _mul (Int Int) Int)
(declare-fun _div (Int Int) Int)
(declare-fun _mod (Int Int) Int)
(declare-fun __uu__PartialApp () Term)
(assert (forall ((x Int) (y Int)) (! (= (_mul x y) (* x y)) :pattern ((_mul x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_div x y) (div x y)) :pattern ((_div x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_mod x y) (mod x y)) :pattern ((_mod x y)))))
(declare-fun _rmul (Real Real) Real)
(declare-fun _rdiv (Real Real) Real)
(assert (forall ((x Real) (y Real)) (! (= (_rmul x y) (* x y)) :pattern ((_rmul x y)))))
(assert (forall ((x Real) (y Real)) (! (= (_rdiv x y) (/ x y)) :pattern ((_rdiv x y)))))
(define-fun Unreachable () Bool false); <start constructor FString_const>
; Constructor
(declare-fun FString_const (Int) FString)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 0 (FString_constr_id (FString_const @u0)))
    :pattern ((FString_const @u0))
    :qid constructor_distinct_FString_const))
  :named constructor_distinct_FString_const))
; Projector
(declare-fun FString_const_proj_0 (FString) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (FString_const_proj_0 (FString_const @u0)) @u0)
    :pattern ((FString_const @u0))
    :qid projection_inverse_FString_const_proj_0))
  :named projection_inverse_FString_const_proj_0))
; Discriminator definition
(define-fun is-FString_const ((__@u0 FString)) Bool
 (and (= (FString_constr_id __@u0) 0) (= __@u0 (FString_const (FString_const_proj_0 __@u0)))))
; </end constructor FString_const>
; <start constructor Tm_type>
; Constructor
(declare-fun Tm_type (Universe) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= 2 (Term_constr_id (Tm_type @u0)))
    :pattern ((Tm_type @u0))
    :qid constructor_distinct_Tm_type))
  :named constructor_distinct_Tm_type))
; Projector
(declare-fun Tm_type_0 (Term) Universe)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= (Tm_type_0 (Tm_type @u0)) @u0) :pattern ((Tm_type @u0)) :qid projection_inverse_Tm_type_0))
  :named projection_inverse_Tm_type_0))
; Discriminator definition
(define-fun is-Tm_type ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 2) (= __@x0 (Tm_type (Tm_type_0 __@x0)))))
; </end constructor Tm_type>
; <start constructor Tm_arrow>
; Constructor
(declare-fun Tm_arrow (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 3 (Term_constr_id (Tm_arrow @u0)))
    :pattern ((Tm_arrow @u0))
    :qid constructor_distinct_Tm_arrow))
  :named constructor_distinct_Tm_arrow))
; Projector
(declare-fun Tm_arrow_id (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (Tm_arrow_id (Tm_arrow @u0)) @u0)
    :pattern ((Tm_arrow @u0))
    :qid projection_inverse_Tm_arrow_id))
  :named projection_inverse_Tm_arrow_id))
; Discriminator definition
(define-fun is-Tm_arrow ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 3) (= __@x0 (Tm_arrow (Tm_arrow_id __@x0)))))
; </end constructor Tm_arrow>
; <start constructor Tm_unit>
; Constructor
(declare-fun Tm_unit () Term)
; Constructor distinct
;;; Fact-ids: 
(assert (! (= 6 (Term_constr_id Tm_unit)) :named constructor_distinct_Tm_unit))
; Discriminator definition
(define-fun is-Tm_unit ((__@x0 Term)) Bool (and (= (Term_constr_id __@x0) 6) (= __@x0 Tm_unit)))
; </end constructor Tm_unit>
; <start constructor BoxInt>
; Constructor
(declare-fun BoxInt (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 7 (Term_constr_id (BoxInt @u0))) :pattern ((BoxInt @u0)) :qid constructor_distinct_BoxInt))
  :named constructor_distinct_BoxInt))
; Projector
(declare-fun BoxInt_proj_0 (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (BoxInt_proj_0 (BoxInt @u0)) @u0)
    :pattern ((BoxInt @u0))
    :qid projection_inverse_BoxInt_proj_0))
  :named projection_inverse_BoxInt_proj_0))
; Discriminator definition
(define-fun is-BoxInt ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 7) (= __@x0 (BoxInt (BoxInt_proj_0 __@x0)))))
; </end constructor BoxInt>
; <start constructor BoxBool>
; Constructor
(declare-fun BoxBool (Bool) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= 8 (Term_constr_id (BoxBool @u0)))
    :pattern ((BoxBool @u0))
    :qid constructor_distinct_BoxBool))
  :named constructor_distinct_BoxBool))
; Projector
(declare-fun BoxBool_proj_0 (Term) Bool)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= (BoxBool_proj_0 (BoxBool @u0)) @u0)
    :pattern ((BoxBool @u0))
    :qid projection_inverse_BoxBool_proj_0))
  :named projection_inverse_BoxBool_proj_0))
; Discriminator definition
(define-fun is-BoxBool ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 8) (= __@x0 (BoxBool (BoxBool_proj_0 __@x0)))))
; </end constructor BoxBool>
; <start constructor BoxString>
; Constructor
(declare-fun BoxString (FString) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= 9 (Term_constr_id (BoxString @u0)))
    :pattern ((BoxString @u0))
    :qid constructor_distinct_BoxString))
  :named constructor_distinct_BoxString))
; Projector
(declare-fun BoxString_proj_0 (Term) FString)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= (BoxString_proj_0 (BoxString @u0)) @u0)
    :pattern ((BoxString @u0))
    :qid projection_inverse_BoxString_proj_0))
  :named projection_inverse_BoxString_proj_0))
; Discriminator definition
(define-fun is-BoxString ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 9) (= __@x0 (BoxString (BoxString_proj_0 __@x0)))))
; </end constructor BoxString>
; <start constructor BoxReal>
; Constructor
(declare-fun BoxReal (Real) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= 10 (Term_constr_id (BoxReal @u0)))
    :pattern ((BoxReal @u0))
    :qid constructor_distinct_BoxReal))
  :named constructor_distinct_BoxReal))
; Projector
(declare-fun BoxReal_proj_0 (Term) Real)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= (BoxReal_proj_0 (BoxReal @u0)) @u0)
    :pattern ((BoxReal @u0))
    :qid projection_inverse_BoxReal_proj_0))
  :named projection_inverse_BoxReal_proj_0))
; Discriminator definition
(define-fun is-BoxReal ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 10) (= __@x0 (BoxReal (BoxReal_proj_0 __@x0)))))
; </end constructor BoxReal>
; <start constructor LexCons>
; Constructor
(declare-fun LexCons (Term Term Term) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= 11 (Term_constr_id (LexCons @x0 @x1 @x2)))
    :pattern ((LexCons @x0 @x1 @x2))
    :qid constructor_distinct_LexCons))
  :named constructor_distinct_LexCons))
; Projector
(declare-fun LexCons_0 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_0 (LexCons @x0 @x1 @x2)) @x0)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_0))
  :named projection_inverse_LexCons_0))
; Projector
(declare-fun LexCons_1 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_1 (LexCons @x0 @x1 @x2)) @x1)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_1))
  :named projection_inverse_LexCons_1))
; Projector
(declare-fun LexCons_2 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_2 (LexCons @x0 @x1 @x2)) @x2)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_2))
  :named projection_inverse_LexCons_2))
; Discriminator definition
(define-fun is-LexCons ((__@x0 Term)) Bool
 (and
  (= (Term_constr_id __@x0) 11)
  (= __@x0 (LexCons (LexCons_0 __@x0) (LexCons_1 __@x0) (LexCons_2 __@x0)))))
; </end constructor LexCons>
; <start constructor BoxProp>
; Constructor
(declare-fun BoxProp (Bool) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= 12 (Term_constr_id (BoxProp @u0)))
    :pattern ((BoxProp @u0))
    :qid constructor_distinct_BoxProp))
  :named constructor_distinct_BoxProp))
; Projector
(declare-fun BoxProp_proj_0 (Term) Bool)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= (BoxProp_proj_0 (BoxProp @u0)) @u0)
    :pattern ((BoxProp @u0))
    :qid projection_inverse_BoxProp_proj_0))
  :named projection_inverse_BoxProp_proj_0))
; Discriminator definition
(define-fun is-BoxProp ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 12) (= __@x0 (BoxProp (BoxProp_proj_0 __@x0)))))
; </end constructor BoxProp>
(declare-fun Prims.precedes@tok (Universe Universe) Term)
(assert
(forall ((u0 Universe) (u1 Universe) (@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))
(! (= (ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)
(Prims.precedes u0 u1 @x0 @x1 @x2 @x3))
:pattern ((ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)))))

(define-fun is-Prims.LexCons ((t Term)) Bool 
(is-LexCons t))
(declare-fun Prims.lex_t () Term)
(declare-fun LexTop () Term)
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (x1 Term) (x2 Term) (y1 Term) (y2 Term))
(iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t (LexCons t1 x1 x2) (LexCons t2 y1 y2)))
(or (Valid (Prims.precedes u0 u1 t1 t2 x1 y1))
(and (= x1 y1)
(Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t x2 y2)))))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (e1 Term) (e2 Term))
(! (iff (Valid (Prims.precedes u0 u1 t1 t2 e1 e2))
(Valid (Prims.precedes U_zero U_zero Prims.lex_t Prims.lex_t e1 e2)))
:pattern (Prims.precedes u0 u1 t1 t2 e1 e2))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term))
(! (iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)) 
(Prec t1 t2))
:pattern ((Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)))))
(assert (forall ((u Universe) (t Term))
(! (iff (HasType (Tm_type u) t)
(= t (Tm_type (U_succ u))))
:pattern ((HasType (Tm_type u) t)))))

(push) ;; push{1
(declare-fun Prims.bool () Term)
(declare-fun Prims.eqtype () Term)
(declare-fun Prims.hasEq (Universe Term) Term)
(declare-fun Prims.int () Term)
(declare-fun Prims.op_Equals (Term Term Term) Term)
(declare-fun Prims.prop () Term)
(declare-fun Tm_refine_9d6af3f3535473623f7aec2f0501897f () Term)
; bool inversion
;;; Fact-ids: Name Prims.bool; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (implies (HasTypeFuel @u0 @x1 Prims.bool) (is-BoxBool @x1))
    :pattern ((HasTypeFuel @u0 @x1 Prims.bool))
    :qid bool_inversion))
  :named bool_inversion))
; bool typing
;;; Fact-ids: Name Prims.bool; Namespace Prims
(assert
 (! (forall ((@u0 Bool))
   (! (HasType (BoxBool @u0) Prims.bool) :pattern ((BoxBool @u0)) :qid bool_typing))
  :named bool_typing))
; Constructor distinct
;;; Fact-ids: Name Prims.bool; Namespace Prims
(assert
 (! (= 106 (Term_constr_id Prims.bool)) :named constructor_distinct_Prims.bool))
; Constructor distinct
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (= 259 (Term_constr_id Prims.int)) :named constructor_distinct_Prims.int))
; Equation for Prims.eqtype
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (= Prims.eqtype Tm_refine_9d6af3f3535473623f7aec2f0501897f) :named equation_Prims.eqtype))
; function token typing
;;; Fact-ids: Name Prims.bool; Namespace Prims
(assert
 (! (HasType Prims.bool Prims.eqtype) :named function_token_typing_Prims.bool))
; function token typing
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Prims.eqtype (Tm_type (U_succ U_zero))) :named function_token_typing_Prims.eqtype))
; function token typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (HasType Prims.int Prims.eqtype) :named function_token_typing_Prims.int))
; function token typing
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (HasType Prims.prop (Tm_type U_zero)) :named function_token_typing_Prims.prop))
; haseq for Tm_refine_9d6af3f3535473623f7aec2f0501897f
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (iff
   (Valid (Prims.hasEq (U_succ U_zero) Tm_refine_9d6af3f3535473623f7aec2f0501897f))
   (Valid (Prims.hasEq (U_succ U_zero) (Tm_type U_zero))))
  :named haseqTm_refine_9d6af3f3535473623f7aec2f0501897f))
; int inversion
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (implies (HasTypeFuel @u0 @x1 Prims.int) (is-BoxInt @x1))
    :pattern ((HasTypeFuel @u0 @x1 Prims.int))
    :qid int_inversion))
  :named int_inversion))
; int typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (forall ((@u0 Int)) (! (HasType (BoxInt @u0) Prims.int) :pattern ((BoxInt @u0)) :qid int_typing))
  :named int_typing))
;;; Fact-ids: Name Prims.op_Equals; Namespace Prims
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (Prims.op_Equals @x0 @x1 @x2) (BoxBool (= @x1 @x2)))
    :pattern ((Prims.op_Equals @x0 @x1 @x2))
    :qid primitive_Prims.op_Equals))
  :named primitive_Prims.op_Equals))
; prop inversion
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (implies (HasTypeFuel @u0 @x1 Prims.prop) (is-BoxProp @x1))
    :pattern ((HasTypeFuel @u0 @x1 Prims.prop))
    :qid prop_inversion))
  :named prop_inversion))
; prop typing
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (forall ((@u0 Bool))
   (! (HasType (BoxProp @u0) Prims.prop) :pattern ((BoxProp @u0)) :qid prop_typing))
  :named prop_typing))
; prop validity
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (forall ((@u0 Bool))
   (! (iff (Valid (BoxProp @u0)) @u0) :pattern ((Valid (BoxProp @u0))) :qid prop_validity))
  :named prop_validity))
; refinement_interpretation
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (iff
     (HasTypeFuel @u0 @x1 Tm_refine_9d6af3f3535473623f7aec2f0501897f)
     (and (HasTypeFuel @u0 @x1 (Tm_type U_zero)) (Valid (Prims.hasEq U_zero @x1))))
    :pattern ((HasTypeFuel @u0 @x1 Tm_refine_9d6af3f3535473623f7aec2f0501897f))
    :qid refinement_interpretation_Tm_refine_9d6af3f3535473623f7aec2f0501897f))
  :named refinement_interpretation_Tm_refine_9d6af3f3535473623f7aec2f0501897f))
; refinement kinding
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Tm_refine_9d6af3f3535473623f7aec2f0501897f (Tm_type (U_succ U_zero)))
  :named refinement_kinding_Tm_refine_9d6af3f3535473623f7aec2f0501897f))
; free var typing
;;; Fact-ids: Name Prims.bool; Namespace Prims
(assert
 (! (HasType Prims.bool Prims.eqtype) :named typing_Prims.bool))
; free var typing
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Prims.eqtype (Tm_type (U_succ U_zero))) :named typing_Prims.eqtype))
; free var typing
;;; Fact-ids: Name Prims.hasEq; Namespace Prims
(assert
 (! (forall ((@u0 Universe) (@x1 Term))
   (! (implies (HasType @x1 (Tm_type @u0)) (HasType (Prims.hasEq @u0 @x1) Prims.prop))
    :pattern ((Prims.hasEq @u0 @x1))
    :qid typing_Prims.hasEq))
  :named typing_Prims.hasEq))
; free var typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (HasType Prims.int Prims.eqtype) :named typing_Prims.int))
; free var typing
;;; Fact-ids: Name Prims.op_Equals; Namespace Prims
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (implies
     (and (HasType @x0 Prims.eqtype) (HasType @x1 @x0) (HasType @x2 @x0))
     (HasType (Prims.op_Equals @x0 @x1 @x2) Prims.bool))
    :pattern ((Prims.op_Equals @x0 @x1 @x2))
    :qid typing_Prims.op_Equals))
  :named typing_Prims.op_Equals))
; free var typing
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (HasType Prims.prop (Tm_type U_zero)) :named typing_Prims.prop))
(push) ;; push{2
; Starting query at Divergence.fst(47,32-47,66)
; Uninterpreted function symbol for impure function
(declare-fun Divergence.decr (Term) Term)
; Uninterpreted name for impure function
(declare-fun Divergence.decr@tok () Term)
; Encoding query formula : forall (x: Prims.int).
;   (* - Could not prove post-condition *) x = 0 = true ==> x = 0 == true ==> Prims.l_False
; Context: While encoding a query
; While typechecking the top-level declaration ‘let rec decr’
; While typechecking the top-level declaration ‘[@@expect_failure] let rec decr’
(push) ;; push{0
(push) ;; push{0
(declare-fun @sk_1 () Term)
;;; Fact-ids: 
(assert (! (HasType @sk_1 Prims.int) :named @hypothesis_4))
(push) ;; push{0
;;; Fact-ids: 
(assert
 (! (= (Prims.op_Equals Prims.int @sk_1 (BoxInt 0)) (BoxBool true)) :named @hypothesis_3))
(push) ;; push{0
;;; Fact-ids: 
(assert
 (! (= (Prims.op_Equals Prims.int @sk_1 (BoxInt 0)) (BoxBool true)) :named @hypothesis_2))
(push) ;; push{0
; <goal 1 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 (! true :named @query))
(set-option :rlimit 2500000)
(echo "<goal>")
(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 "</goal>")
(pop) ;; 0}pop
(pop) ;; 0}pop
(pop) ;; 0}pop
(pop) ;; 0}pop
(pop) ;; 0}pop
(echo "Done!")

doc/book/code/failedQueries-Part1.Assertions-1.smt2

; Z3 invocation started by F*
; F* version: 2026.08.30~dev -- commit hash: 52f17ab8fdea379708a659a1b02c8f8b47f877fa
; Z3 version (according to F*): 5.1.0

(set-option :global-decls false)
(set-option :smt.mbqi false)
(set-option :auto_config false)
(set-option :model true)
(set-option :smt.case_split 3)
(set-option :smt.relevancy 2)
(set-option :rewriter.enable_der false)
(set-option :rewriter.sort_disjunctions false)
(set-option :pi.decompose_patterns false)
(set-option :smt.arith.solver 6)
(set-option :smt.random-seed 0)


(declare-sort FString)
(declare-fun FString_constr_id (FString) Int)

(declare-sort Term)
(declare-sort Universe)
(declare-fun U_zero () Universe)
(declare-fun U_succ (Universe) Universe)
(declare-fun ulevel ((Universe)) Int)
(declare-fun Univ (Int) Universe)
(assert (= (ulevel U_zero) 0))
(assert (forall ((u Universe)) (! (= (ulevel (U_succ u)) (+ 1 (ulevel u))) :pattern ((ulevel (U_succ u))))))
(assert (forall ((u Universe)) (! (>= (ulevel u) 0) :pattern ((ulevel u)))))
(assert (forall ((u Universe)) (! (= (Univ (ulevel u)) u) :pattern ((ulevel u)))))
(assert (forall ((i Int)) (! (implies (>= i 0) (= (ulevel (Univ i)) i)) :pattern ((Univ i)))))
(declare-fun U_max (Universe Universe) Universe)
(assert (forall ((u1 Universe) (u2 Universe))
(! (= (U_max u1 u2)
(ite (<= (ulevel u1) (ulevel u2)) u2 u1))
:pattern ((U_max u1 u2)))))
(declare-fun U_unif (Int) Universe)
(declare-fun U_unknown () Universe)
(declare-fun Term_constr_id (Term) Int)
(declare-sort Dummy_sort)
(declare-fun Dummy_value () Dummy_sort)
(declare-datatypes () ((Fuel 
(ZFuel) 
(SFuel (prec Fuel)))))
(declare-fun MaxIFuel () Fuel)
(declare-fun MaxFuel () Fuel)
(declare-fun PreType (Term) Term)
(declare-fun Valid (Term) Bool)
(declare-fun HasTypeFuel (Fuel Term Term) Bool)
(define-fun HasTypeZ ((x Term) (t Term)) Bool
(HasTypeFuel ZFuel x t))
(define-fun HasType ((x Term) (t Term)) Bool
(HasTypeFuel MaxIFuel x t))
(declare-fun IsTotFun (Term) Bool)

                ;;fuel irrelevance
(assert (forall ((f Fuel) (x Term) (t Term))
(! (= (HasTypeFuel (SFuel f) x t)
(HasTypeZ x t))
:pattern ((HasTypeFuel (SFuel f) x t)))))
(declare-fun NoHoist (Term Bool) Bool)
;;no-hoist
(assert (forall ((dummy Term) (b Bool))
(! (= (NoHoist dummy b) b)
:pattern ((NoHoist dummy b)))))
(define-fun  IsTyped ((x Term)) Bool
(exists ((t Term)) (HasTypeZ x t)))
(declare-fun ApplyTF (Term Fuel) Term)
(declare-fun ApplyTT (Term Term) Term)
(declare-fun Prec (Term Term) Bool)
(assert (forall ((x Term) (y Term) (z Term))
(! (implies (and (Prec x y) (Prec y z)) (Prec x z))
:pattern ((Prec x z) (Prec x y)))))
(assert (forall ((x Term) (y Term))
(implies (Prec x y)
(not (Prec y x)))))
(declare-fun Closure (Term) Term)
(declare-fun ConsTerm (Term Term) Term)
(declare-fun ConsFuel (Fuel Term) Term)
(declare-fun Tm_uvar (Int) Term)
(define-fun Reify ((x Term)) Term x)
(declare-fun Prims.precedes (Universe Universe Term Term Term Term) Term)
(declare-fun Range_const (Int) Term)
(declare-fun _mul (Int Int) Int)
(declare-fun _div (Int Int) Int)
(declare-fun _mod (Int Int) Int)
(declare-fun __uu__PartialApp () Term)
(assert (forall ((x Int) (y Int)) (! (= (_mul x y) (* x y)) :pattern ((_mul x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_div x y) (div x y)) :pattern ((_div x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_mod x y) (mod x y)) :pattern ((_mod x y)))))
(declare-fun _rmul (Real Real) Real)
(declare-fun _rdiv (Real Real) Real)
(assert (forall ((x Real) (y Real)) (! (= (_rmul x y) (* x y)) :pattern ((_rmul x y)))))
(assert (forall ((x Real) (y Real)) (! (= (_rdiv x y) (/ x y)) :pattern ((_rdiv x y)))))
(define-fun Unreachable () Bool false); <start constructor FString_const>
; Constructor
(declare-fun FString_const (Int) FString)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 0 (FString_constr_id (FString_const @u0)))
    :pattern ((FString_const @u0))
    :qid constructor_distinct_FString_const))
  :named constructor_distinct_FString_const))
; Projector
(declare-fun FString_const_proj_0 (FString) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (FString_const_proj_0 (FString_const @u0)) @u0)
    :pattern ((FString_const @u0))
    :qid projection_inverse_FString_const_proj_0))
  :named projection_inverse_FString_const_proj_0))
; Discriminator definition
(define-fun is-FString_const ((__@u0 FString)) Bool
 (and (= (FString_constr_id __@u0) 0) (= __@u0 (FString_const (FString_const_proj_0 __@u0)))))
; </end constructor FString_const>
; <start constructor Tm_type>
; Constructor
(declare-fun Tm_type (Universe) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= 2 (Term_constr_id (Tm_type @u0)))
    :pattern ((Tm_type @u0))
    :qid constructor_distinct_Tm_type))
  :named constructor_distinct_Tm_type))
; Projector
(declare-fun Tm_type_0 (Term) Universe)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= (Tm_type_0 (Tm_type @u0)) @u0) :pattern ((Tm_type @u0)) :qid projection_inverse_Tm_type_0))
  :named projection_inverse_Tm_type_0))
; Discriminator definition
(define-fun is-Tm_type ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 2) (= __@x0 (Tm_type (Tm_type_0 __@x0)))))
; </end constructor Tm_type>
; <start constructor Tm_arrow>
; Constructor
(declare-fun Tm_arrow (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 3 (Term_constr_id (Tm_arrow @u0)))
    :pattern ((Tm_arrow @u0))
    :qid constructor_distinct_Tm_arrow))
  :named constructor_distinct_Tm_arrow))
; Projector
(declare-fun Tm_arrow_id (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (Tm_arrow_id (Tm_arrow @u0)) @u0)
    :pattern ((Tm_arrow @u0))
    :qid projection_inverse_Tm_arrow_id))
  :named projection_inverse_Tm_arrow_id))
; Discriminator definition
(define-fun is-Tm_arrow ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 3) (= __@x0 (Tm_arrow (Tm_arrow_id __@x0)))))
; </end constructor Tm_arrow>
; <start constructor Tm_unit>
; Constructor
(declare-fun Tm_unit () Term)
; Constructor distinct
;;; Fact-ids: 
(assert (! (= 6 (Term_constr_id Tm_unit)) :named constructor_distinct_Tm_unit))
; Discriminator definition
(define-fun is-Tm_unit ((__@x0 Term)) Bool (and (= (Term_constr_id __@x0) 6) (= __@x0 Tm_unit)))
; </end constructor Tm_unit>
; <start constructor BoxInt>
; Constructor
(declare-fun BoxInt (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 7 (Term_constr_id (BoxInt @u0))) :pattern ((BoxInt @u0)) :qid constructor_distinct_BoxInt))
  :named constructor_distinct_BoxInt))
; Projector
(declare-fun BoxInt_proj_0 (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (BoxInt_proj_0 (BoxInt @u0)) @u0)
    :pattern ((BoxInt @u0))
    :qid projection_inverse_BoxInt_proj_0))
  :named projection_inverse_BoxInt_proj_0))
; Discriminator definition
(define-fun is-BoxInt ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 7) (= __@x0 (BoxInt (BoxInt_proj_0 __@x0)))))
; </end constructor BoxInt>
; <start constructor BoxBool>
; Constructor
(declare-fun BoxBool (Bool) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= 8 (Term_constr_id (BoxBool @u0)))
    :pattern ((BoxBool @u0))
    :qid constructor_distinct_BoxBool))
  :named constructor_distinct_BoxBool))
; Projector
(declare-fun BoxBool_proj_0 (Term) Bool)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= (BoxBool_proj_0 (BoxBool @u0)) @u0)
    :pattern ((BoxBool @u0))
    :qid projection_inverse_BoxBool_proj_0))
  :named projection_inverse_BoxBool_proj_0))
; Discriminator definition
(define-fun is-BoxBool ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 8) (= __@x0 (BoxBool (BoxBool_proj_0 __@x0)))))
; </end constructor BoxBool>
; <start constructor BoxString>
; Constructor
(declare-fun BoxString (FString) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= 9 (Term_constr_id (BoxString @u0)))
    :pattern ((BoxString @u0))
    :qid constructor_distinct_BoxString))
  :named constructor_distinct_BoxString))
; Projector
(declare-fun BoxString_proj_0 (Term) FString)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= (BoxString_proj_0 (BoxString @u0)) @u0)
    :pattern ((BoxString @u0))
    :qid projection_inverse_BoxString_proj_0))
  :named projection_inverse_BoxString_proj_0))
; Discriminator definition
(define-fun is-BoxString ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 9) (= __@x0 (BoxString (BoxString_proj_0 __@x0)))))
; </end constructor BoxString>
; <start constructor BoxReal>
; Constructor
(declare-fun BoxReal (Real) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= 10 (Term_constr_id (BoxReal @u0)))
    :pattern ((BoxReal @u0))
    :qid constructor_distinct_BoxReal))
  :named constructor_distinct_BoxReal))
; Projector
(declare-fun BoxReal_proj_0 (Term) Real)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= (BoxReal_proj_0 (BoxReal @u0)) @u0)
    :pattern ((BoxReal @u0))
    :qid projection_inverse_BoxReal_proj_0))
  :named projection_inverse_BoxReal_proj_0))
; Discriminator definition
(define-fun is-BoxReal ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 10) (= __@x0 (BoxReal (BoxReal_proj_0 __@x0)))))
; </end constructor BoxReal>
; <start constructor LexCons>
; Constructor
(declare-fun LexCons (Term Term Term) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= 11 (Term_constr_id (LexCons @x0 @x1 @x2)))
    :pattern ((LexCons @x0 @x1 @x2))
    :qid constructor_distinct_LexCons))
  :named constructor_distinct_LexCons))
; Projector
(declare-fun LexCons_0 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_0 (LexCons @x0 @x1 @x2)) @x0)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_0))
  :named projection_inverse_LexCons_0))
; Projector
(declare-fun LexCons_1 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_1 (LexCons @x0 @x1 @x2)) @x1)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_1))
  :named projection_inverse_LexCons_1))
; Projector
(declare-fun LexCons_2 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_2 (LexCons @x0 @x1 @x2)) @x2)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_2))
  :named projection_inverse_LexCons_2))
; Discriminator definition
(define-fun is-LexCons ((__@x0 Term)) Bool
 (and
  (= (Term_constr_id __@x0) 11)
  (= __@x0 (LexCons (LexCons_0 __@x0) (LexCons_1 __@x0) (LexCons_2 __@x0)))))
; </end constructor LexCons>
; <start constructor BoxProp>
; Constructor
(declare-fun BoxProp (Bool) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= 12 (Term_constr_id (BoxProp @u0)))
    :pattern ((BoxProp @u0))
    :qid constructor_distinct_BoxProp))
  :named constructor_distinct_BoxProp))
; Projector
(declare-fun BoxProp_proj_0 (Term) Bool)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= (BoxProp_proj_0 (BoxProp @u0)) @u0)
    :pattern ((BoxProp @u0))
    :qid projection_inverse_BoxProp_proj_0))
  :named projection_inverse_BoxProp_proj_0))
; Discriminator definition
(define-fun is-BoxProp ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 12) (= __@x0 (BoxProp (BoxProp_proj_0 __@x0)))))
; </end constructor BoxProp>
(declare-fun Prims.precedes@tok (Universe Universe) Term)
(assert
(forall ((u0 Universe) (u1 Universe) (@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))
(! (= (ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)
(Prims.precedes u0 u1 @x0 @x1 @x2 @x3))
:pattern ((ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)))))

(define-fun is-Prims.LexCons ((t Term)) Bool 
(is-LexCons t))
(declare-fun Prims.lex_t () Term)
(declare-fun LexTop () Term)
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (x1 Term) (x2 Term) (y1 Term) (y2 Term))
(iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t (LexCons t1 x1 x2) (LexCons t2 y1 y2)))
(or (Valid (Prims.precedes u0 u1 t1 t2 x1 y1))
(and (= x1 y1)
(Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t x2 y2)))))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (e1 Term) (e2 Term))
(! (iff (Valid (Prims.precedes u0 u1 t1 t2 e1 e2))
(Valid (Prims.precedes U_zero U_zero Prims.lex_t Prims.lex_t e1 e2)))
:pattern (Prims.precedes u0 u1 t1 t2 e1 e2))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term))
(! (iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)) 
(Prec t1 t2))
:pattern ((Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)))))
(assert (forall ((u Universe) (t Term))
(! (iff (HasType (Tm_type u) t)
(= t (Tm_type (U_succ u))))
:pattern ((HasType (Tm_type u) t)))))

(push) ;; push{1
(declare-fun Prims.eqtype () Term)
(declare-fun Prims.hasEq (Universe Term) Term)
(declare-fun Prims.int () Term)
(declare-fun Prims.op_Star (Term Term) Term)
(declare-fun Prims.prop () Term)
(declare-fun Tm_refine_9d6af3f3535473623f7aec2f0501897f () Term)
; Constructor distinct
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (= 259 (Term_constr_id Prims.int)) :named constructor_distinct_Prims.int))
; Equation for Prims.eqtype
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (= Prims.eqtype Tm_refine_9d6af3f3535473623f7aec2f0501897f) :named equation_Prims.eqtype))
; function token typing
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Prims.eqtype (Tm_type (U_succ U_zero))) :named function_token_typing_Prims.eqtype))
; function token typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (HasType Prims.int Prims.eqtype) :named function_token_typing_Prims.int))
; function token typing
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (HasType Prims.prop (Tm_type U_zero)) :named function_token_typing_Prims.prop))
; haseq for Tm_refine_9d6af3f3535473623f7aec2f0501897f
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (iff
   (Valid (Prims.hasEq (U_succ U_zero) Tm_refine_9d6af3f3535473623f7aec2f0501897f))
   (Valid (Prims.hasEq (U_succ U_zero) (Tm_type U_zero))))
  :named haseqTm_refine_9d6af3f3535473623f7aec2f0501897f))
; int inversion
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (implies (HasTypeFuel @u0 @x1 Prims.int) (is-BoxInt @x1))
    :pattern ((HasTypeFuel @u0 @x1 Prims.int))
    :qid int_inversion))
  :named int_inversion))
; int typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (forall ((@u0 Int)) (! (HasType (BoxInt @u0) Prims.int) :pattern ((BoxInt @u0)) :qid int_typing))
  :named int_typing))
;;; Fact-ids: Name Prims.op_Star; Namespace Prims
(assert
 (! (forall ((@x0 Term) (@x1 Term))
   (! (= (Prims.op_Star @x0 @x1) (BoxInt (* (BoxInt_proj_0 @x0) (BoxInt_proj_0 @x1))))
    :pattern ((Prims.op_Star @x0 @x1))
    :qid primitive_Prims.op_Star))
  :named primitive_Prims.op_Star))
; prop inversion
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (implies (HasTypeFuel @u0 @x1 Prims.prop) (is-BoxProp @x1))
    :pattern ((HasTypeFuel @u0 @x1 Prims.prop))
    :qid prop_inversion))
  :named prop_inversion))
; prop typing
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (forall ((@u0 Bool))
   (! (HasType (BoxProp @u0) Prims.prop) :pattern ((BoxProp @u0)) :qid prop_typing))
  :named prop_typing))
; prop validity
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (forall ((@u0 Bool))
   (! (iff (Valid (BoxProp @u0)) @u0) :pattern ((Valid (BoxProp @u0))) :qid prop_validity))
  :named prop_validity))
; refinement_interpretation
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (iff
     (HasTypeFuel @u0 @x1 Tm_refine_9d6af3f3535473623f7aec2f0501897f)
     (and (HasTypeFuel @u0 @x1 (Tm_type U_zero)) (Valid (Prims.hasEq U_zero @x1))))
    :pattern ((HasTypeFuel @u0 @x1 Tm_refine_9d6af3f3535473623f7aec2f0501897f))
    :qid refinement_interpretation_Tm_refine_9d6af3f3535473623f7aec2f0501897f))
  :named refinement_interpretation_Tm_refine_9d6af3f3535473623f7aec2f0501897f))
; refinement kinding
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Tm_refine_9d6af3f3535473623f7aec2f0501897f (Tm_type (U_succ U_zero)))
  :named refinement_kinding_Tm_refine_9d6af3f3535473623f7aec2f0501897f))
; free var typing
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Prims.eqtype (Tm_type (U_succ U_zero))) :named typing_Prims.eqtype))
; free var typing
;;; Fact-ids: Name Prims.hasEq; Namespace Prims
(assert
 (! (forall ((@u0 Universe) (@x1 Term))
   (! (implies (HasType @x1 (Tm_type @u0)) (HasType (Prims.hasEq @u0 @x1) Prims.prop))
    :pattern ((Prims.hasEq @u0 @x1))
    :qid typing_Prims.hasEq))
  :named typing_Prims.hasEq))
; free var typing
;;; Fact-ids:

... (truncated due to discussion size limits)

### FStar test suite (last 200 log lines)

... (truncated)
OCAMLOPT ExtUInt128
findlib: [WARNING] Interface ratio.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface big_int.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface num.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface nat.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface arith_status.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
OCAMLOPT ExtUIntDivRem
findlib: [WARNING] Interface ratio.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface big_int.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface num.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface nat.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface arith_status.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
OCAMLOPT ExtUIntRotate
findlib: [WARNING] Interface ratio.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface big_int.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface num.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface nat.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface arith_status.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
XFAIL ocaml ExtIntNe
XFAIL ocaml ExtUInt8Lognot
RUN rust ExtUInt8Lognot
RUN ocaml ExtBoolHigherOrder
RUN ocaml ExtBoolShortCircuit
RUN ocaml ExtDatatypesEnum
RUN ocaml ExtDatatypesMutual
RUN ocaml ExtDatatypesRec
RUN ocaml ExtDatatypesRecord
RUN ocaml ExtDatatypesVariant
RUN ocaml ExtInt128
RUN ocaml ExtIntCast
RUN ocaml ExtIntDivRem
RUN ocaml ExtIntShiftArith
RUN ocaml ExtIntSigned
RUN ocaml ExtPrimsInt
RUN ocaml ExtPrimsIntBignum
RUN ocaml ExtPrimsIntDiv
RUN ocaml ExtPrimsIntMul
RUN ocaml ExtProjectorOfCtor
RUN ocaml ExtSmoke
RUN ocaml ExtUInt128
RUN ocaml ExtUIntDivRem
RUN ocaml ExtUIntRotate
EXTRACT ExtUIntUnsigned
EXTRACT ExtUIntUnsigned
OCAMLOPT ExtUIntUnsigned
findlib: [WARNING] Interface ratio.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface big_int.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface num.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface nat.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface arith_status.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
KRML C ExtUIntUnsigned
KRML RUST ExtUIntUnsigned
RUSTC ExtUIntUnsigned
warning: failed to connect to jobserver from environment variable MAKEFLAGS="krs -j4 --jobserver-auth=3,4 -- FSTAR_EXE=/tmp/gh-aw/agent/FStar/stage3/out/bin/fstar.exe KRML_EXE=/tmp/gh-aw/agent/FStar/karamel/out/bin/krml": cannot open file descriptor 3 from the jobserver environment variable value: Bad file descriptor (os error 9)
|
= note: the build environment is likely misconfigured

RUN ocaml ExtUIntUnsigned
CC ExtUIntUnsigned
RUN c ExtUIntUnsigned
RUN rust ExtUIntUnsigned
EXTRACT ExtUIntMask
EXTRACT ExtUIntMask
KRML C ExtUIntMask
XFAIL rust ExtUIntMask
OCAMLOPT ExtUIntMask
findlib: [WARNING] Interface ratio.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface big_int.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface num.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface nat.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
findlib: [WARNING] Interface arith_status.cmi occurs in several directories: /home/runner/.opam/4.14.2/lib/num, /home/runner/.opam/4.14.2/lib/ocaml
Warning 2: in the arguments to FStar.UInt32.eq_mask, in top-level declaration ExtUIntMask.eq_mask_32, in file ExtUIntMask: Reference to FStar.UInt32.eq_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt8.eq_mask, in top-level declaration ExtUIntMask.eq_mask_8, in file ExtUIntMask: Reference to FStar.UInt8.eq_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt16.eq_mask, in top-level declaration ExtUIntMask.eq_mask_16, in file ExtUIntMask: Reference to FStar.UInt16.eq_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt64.eq_mask, in top-level declaration ExtUIntMask.eq_mask_64, in file ExtUIntMask: Reference to FStar.UInt64.eq_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt32.gte_mask, in top-level declaration ExtUIntMask.gte_mask_32, in file ExtUIntMask: Reference to FStar.UInt32.gte_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt64.gte_mask, in top-level declaration ExtUIntMask.gte_mask_64, in file ExtUIntMask: Reference to FStar.UInt64.gte_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt8.gte_mask, in top-level declaration ExtUIntMask.gte_mask_8_16, in file ExtUIntMask: Reference to FStar.UInt8.gte_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt16.gte_mask, in top-level declaration ExtUIntMask.gte_mask_8_16, in file ExtUIntMask: Reference to FStar.UInt16.gte_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt32.eq_mask, in top-level declaration ExtUIntMask.mask_use_tests, in file ExtUIntMask: Reference to FStar.UInt32.eq_mask has no corresponding implementation; please provide a C implementation
Warning 2: in the arguments to FStar.UInt32.gte_mask, in top-level declaration ExtUIntMask.mask_use_tests, in file ExtUIntMask: Reference to FStar.UInt32.gte_mask has no corresponding implementation; please provide a C implementation
CC ExtUIntMask
RUN c ExtUIntMask
RUN ocaml ExtUIntMask
make[2]: Target 'all' not remade because of errors.
make[1]: *** [Makefile:574: _unit-tests] Error 2
make[1]: Target '_test' not remade because of errors.
make: *** [Makefile:525: test-3] Error 2
make: Target 'test' not remade because of errors.

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