(272) * Warning 272 at Monitor.fst(15,0-15,36): - Top-level let-bindings must be total; this term may have effects

(361) * Warning 361 at GoodHandler1.fst(150,0-150,37): - Some #push-options have not been popped. Current depth is 1.

(272) * Warning 272 at GoodHandler1.fst(150,0-150,37): - Top-level let-bindings must be total; this term may have effects

(361) * Warning 361 at StlcHandlers.fst(121,0-124,16): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at ../../Compiler.StlcToFStar.fst(385,0-394,18): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at WebServer.fst(237,0-238,38): - Some #push-options have not been popped. Current depth is 1.

* Warning <unknown> at WebServer.fst(184,2-184,32): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also ../../Compiler.MIO.To.Interm.fst(391,8-391,43)

* Warning <unknown> at WebServer.fst(184,2-184,32): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also ../../Compiler.MIO.To.Interm.fst(390,8-390,42)

(349) * Warning 349 at Utils.fst(377,2-381,5): - The verification condition succeeded after splitting it to localize potential errors, although the original non-split verification condition failed. If you want to rely on splitting queries for verifying your program please use the '--split_queries always' option rather than relying on it implicitly.

(352) * Warning 352 at ../../MIO.fst(217,27-217,44): - Combinator Prims.PURE ~> MIO.MIOwp is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(242) * Warning 242 at case-studies/IOLogging.fst(111,0-118,59): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/IOLogging.fst(112,11-112,14)

* Warning <unknown> at case-studies/IOLogging.fst(103,3-103,33): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also Compiler.MIO.To.Interm.fst(391,8-391,43)

* Warning <unknown> at case-studies/NoState.fst(75,57-75,62): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances.

* Warning <unknown> at case-studies/Compiler.Model1.Examples.fst(202,22-202,52): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also Compiler.MIO.To.Interm.fst(390,8-390,42)

* Warning <unknown> at case-studies/Zip.fst(59,76-59,81): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances.

(242) * Warning 242 at case-studies/Compiler.Model1.Examples.fst(136,0-143,58): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/Compiler.Model1.Examples.fst(137,10-137,13)

(242) * Warning 242 at case-studies/Compiler.Model1.Examples.fst(95,0-103,58): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/Compiler.Model1.Examples.fst(96,10-96,13)

(242) * Warning 242 at case-studies/NoState.fst(48,0-56,58): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/NoState.fst(49,10-49,13)

(361) * Warning 361 at Compiler.StlcToFStar.fst(385,0-394,18): - Some #push-options have not been popped. Current depth is 1.