Sketch Pulse short-circuiting for stateful boolean operands#4336
Draft
eluvane wants to merge 9 commits into
Draft
Sketch Pulse short-circuiting for stateful boolean operands#4336eluvane wants to merge 9 commits into
eluvane wants to merge 9 commits into
Annotations
10 warnings
|
Run CI:
FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
Run CI:
FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
Run CI:
FStarC.PIMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PIMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.PIMap.t
|
|
Run CI:
FStarC.IMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.IMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.IMap.t
|
|
Run CI:
FStarC.Unionfind.fsti#L21
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(21,5-21,11):
- Adding an implicit 'assume new' qualifier on FStarC.Unionfind.p_uvar
|
|
Run CI:
FStarC.Unionfind.fsti#L20
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(20,5-20,8):
- Adding an implicit 'assume new' qualifier on FStarC.Unionfind.puf
|
|
Run CI:
FStarC.Hash.fsti#L4
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Hash.fsti(4,5-4,14):
- Adding an implicit 'assume new' qualifier on FStarC.Hash.hash_code
|
|
Run CI:
FStarC.Timing.fsti#L20
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Timing.fsti(20,5-20,12):
- Adding an implicit 'assume new' qualifier on FStarC.Timing.time_ns
|
|
Run CI:
FStarC.SMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.SMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.SMap.t
|
|
Run CI:
FStarC.PSMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PSMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.PSMap.t
|
background
wait
wait-all
cancel
parallel
Loading