Rel: keep RHS uvars abstracted over pattern vars in quasi-pattern solutions (fixes #4587) - #4590
Merged
Merged
Annotations
10 warnings and 1 notice
|
Run CI:
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/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_Minus
|
|
Run CI:
FStar.WellFoundedRelation.fst#L148
(290) * Warning 290 at /home/runner/work/FStar/FStar/ulib/FStar.WellFoundedRelation.fst(148,21-148,46):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
wfr_a.decreaser (FStar.Pervasives.dfst xy)
(bound in
FStar.WellFoundedRelation.fst(148,21-148,46))
and
wfr_a.decreaser (FStar.Pervasives.dfst xy)
(bound in
FStar.WellFoundedRelation.fst(148,21-148,46))
are equal.
- The type of the first term is:
FStar.WellFoundedRelation.acc_classical wfr_a.relation
(FStar.Pervasives.dfst xy)
- The type of the second term is:
FStar.WellFoundedRelation.acc_classical wfr_a.relation
(FStar.Pervasives.dfst xy)
- If the proof fails, try annotating these with the same type.
|
|
Run CI:
FStarC.PIMap.fsti#L7
(239) * Warning 239 at /home/runner/work/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 /home/runner/work/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 /home/runner/work/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 /home/runner/work/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 /home/runner/work/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 /home/runner/work/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 /home/runner/work/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 /home/runner/work/FStar/FStar/src/data/FStarC.PSMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.PSMap.t
|
|
"The ubuntu-latest label will migrate to Ubuntu 26 beginning October 19, 2026. For more information, see https://github.com/actions/runner-images/issues/14748"
|
background
wait
wait-all
cancel
parallel
Loading