Steel CI #357
Annotations
2 errors and 10 warnings
|
Steel CI
Process completed with exit code 2.
|
|
Steel CI:
dummy#L0
(276) * Error 276 at Steel.Heap.fst(844,0-931,18):
- Unexpected output from Z3:
"ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1066
Failed to verify: m_columns_with_changed_bounds.empty()
Z3 4.13.3.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new"
|
|
Steel CI:
Steel.ST.Effect.AtomicAndGhost.fsti#L185
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti(185,16-185,20):
- Combinator (Steel.ST.Effect.AtomicAndGhost.STAGCommon ,
Steel.ST.Effect.AtomicAndGhost.STAGCommon) |>
Steel.ST.Effect.AtomicAndGhost.STAGCommon is not a substitutive indexed
effect combinator, it is better to make it one if possible for better
performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L169
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36):
- Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect
combinator, it is better to make it one if possible for better performance
and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L168
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26):
- Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a
substitutive indexed effect combinator, it is better to make it one if
possible for better performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L167
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20):
- Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |>
Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it
is better to make it one if possible for better performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L169
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36):
- Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect
combinator, it is better to make it one if possible for better performance
and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L168
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26):
- Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a
substitutive indexed effect combinator, it is better to make it one if
possible for better performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L167
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20):
- Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |>
Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it
is better to make it one if possible for better performance and ease of use
|
|
Steel CI:
Steel.Effect.Common.fsti#L415
(340) * Warning 340 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(461,24-461,37):
- Unfolding name which is marked as a plugin: frame_vc_norm
- See also /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(415,4-415,17)
|
|
Steel CI:
Steel.Effect.Common.fsti#L2066
(337) * Warning 337 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(2066,65-2066,66):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
Steel CI:
ExtractSteel.Krml.fst#L33
(337) * Warning 337 at /__w/steel/steel/steel/src/extraction/ExtractSteel.Krml.fst(33,41-33,42):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
Loading