Shaked Flur

Seahorn verifies `assert!(false)`

5

The following minimal example is verified by Seahorn, even though it should obviously fail: ```rust #[test] fn t00() { for _ in 0..1 { verifier::VerifierNonDet::verifier_nondet(i32::default()); } if prop_is_replay() { //...

I need to know that BitVec's are bounded by 2^n.

2

I need the following information about the representation of BitVec. ```coq Axiom denote_bv_max : forall (n : N) (m : denote_type (BitVec (N.to_nat n))), m < 2 ^ n. ```...

Cava1 semantics was a Moore machine, but Cava2 is Mealy?

11

[Here](https://github.com/project-oak/silveroak/blob/59688de9126ffda3d23c55fabac7364ce260043e/firmware/IncrementWait/Test.v) are two circuits, test1 written in cava1, and test2 written in cava2, which I thought should behave the same, but simulate gives different traces (included in the file).