runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

Investigate flaky tests #286

Closed hjorthjort closed 3 years ago

hjorthjort commented 3 years ago

PR #283 separates flaky Dexter proofs from non-flaky ones.

One of the Dexter proofs passes locally on our development machines, but sometimes fails in CI (~50% of times).

One suggested solution is in https://github.com/kframework/kore/issues/2407 That would remove timing-related failures of Z3, which we suspect is what is causing issues (Z3 timing out).

Another suggested solution is to split the proof into several ones with side conditions that are easier to resolve.