Build FStar master with Z3 master #10
NikolajBjornerfstar-master-build.yml
on: schedule
build-and-report
39m 11s
Annotations
2 errors and 10 warnings
|
build-and-report
Process completed with exit code 2.
|
|
build-and-report:
FStar.BitVector.fst#L122
(19) * Error 19 at /tmp/gh-aw/agent/FStar/ulib/FStar.BitVector.fst(123,51-127,9):
- Could not prove post-condition
- Try with --query_stats to get more details
- Env =
(n : Prims.pos) (a : FStar.BitVector.bv_t n) (s : Prims.nat)
(i : i: Prims.nat{i < n})
- VC =
(forall (_: Prims.squash Prims.l_True).
(* - Could not prove post-condition *)
(i < n ==>
i < FStar.Seq.Base.length (FStar.BitVector.rotate_left_vec a s)) /\
(forall (any_result: i: Prims.nat{i < n}).
i == any_result ==>
(forall (any_result: Prims.bool).
FStar.Seq.Base.index (FStar.BitVector.rotate_left_vec a s) i ==
any_result ==>
(n > 0 ==> n <> 0) /\
(forall (any_result: Prims.pos).
n == any_result ==>
(forall (any_result: Prims.int).
(i + s) % n == any_result ==>
(i + s) % n >= 0 /\
(i + s) % n < FStar.Seq.Base.length a))))) /\
(forall (p: Prims.pure_post Prims.unit).
(forall (pure_result: Prims.unit).
FStar.Seq.Base.index (FStar.BitVector.rotate_left_vec a s) i =
FStar.Seq.Base.index a ((i + s) % n) ==>
p pure_result) ==>
(n > 0 ==> n <> 0) /\
(forall (any_result: Prims.pos).
n == any_result ==>
(forall (any_result: Prims.int).
s % n == any_result ==>
(forall (k: Prims.pure_post Prims.unit).
(forall (x: Prims.unit). {:pattern Prims.guard_free (k x)}
p x ==> k x) ==>
(any_result = 0 == true ==>
(forall (any_result: Prims.unit). k any_result)) /\
(~(any_result = 0 = true) ==>
(forall (b: Prims.bool).
any_result = 0 == b ==>
(forall (k: Prims.pure_post Prims.unit).
(forall (x: Prims.unit).
{:pattern Prims.guard_free (k x)}
k x ==> k x) ==>
(i < n - any_result == true ==>
(forall (any_result: Prims.unit). k any_result
)) /\
(~(i < n - any_result = true) ==>
(forall (b: Prims.bool).
i < n - any_result == b ==>
(forall (any_result: Prims.unit).
k any_result))))))))))
- See also /tmp/gh-aw/agent/FStar/ulib/FStar.BitVector.fst(122,21-122,77)
|
|
build-and-report:
FStar.UInt.fsti#L435
(271) * Warning 271 at /tmp/gh-aw/agent/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
|
|
build-and-report:
FStar.UInt.fsti#L435
(271) * Warning 271 at /tmp/gh-aw/agent/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
|
|
build-and-report:
FStarC.PIMap.fsti#L7
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/data/FStarC.PIMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.PIMap.t
|
|
build-and-report:
FStarC.IMap.fsti#L7
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/data/FStarC.IMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.IMap.t
|
|
build-and-report:
FStarC.Unionfind.fsti#L21
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/basic/FStarC.Unionfind.fsti(21,5-21,11):
- Adding an implicit 'assume new' qualifier on FStarC.Unionfind.p_uvar
|
|
build-and-report:
FStarC.Unionfind.fsti#L20
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/basic/FStarC.Unionfind.fsti(20,5-20,8):
- Adding an implicit 'assume new' qualifier on FStarC.Unionfind.puf
|
|
build-and-report:
FStarC.Hash.fsti#L4
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/basic/FStarC.Hash.fsti(4,5-4,14):
- Adding an implicit 'assume new' qualifier on FStarC.Hash.hash_code
|
|
build-and-report:
FStarC.Timing.fsti#L20
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/basic/FStarC.Timing.fsti(20,5-20,12):
- Adding an implicit 'assume new' qualifier on FStarC.Timing.time_ns
|
|
build-and-report:
FStarC.SMap.fsti#L7
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/data/FStarC.SMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.SMap.t
|
|
build-and-report:
FStarC.PSMap.fsti#L7
(239) * Warning 239 at /tmp/gh-aw/agent/FStar/src/data/FStarC.PSMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.PSMap.t
|