search

runtimeverification / plutus-core-semantics

BSD 3-Clause "New" or "Revised" License
27 stars 5 forks source link

The trivial-policies proof broke #347

Closed gtrepta closed 1 year ago

gtrepta commented 2 years ago

Somewhere along the way, the trivial-policies.md proof silently broke, outputting #Top still (so it passes on CI) but also a lot of kore from kore-exec because it failed to simplify a term.

gtrepta commented 2 years ago

Some more info on the kore-exec output, they are all of the form:

kore-exec: [12327082] Warning (WarnUnsimplifiedPredicate)

If they are just warnings, then does that mean they can safely be ignored? It would still be nice to suppress this output though (there's around 95MB of it).

gtrepta commented 1 year ago

fixed by https://github.com/runtimeverification/plutus-core-semantics/pull/361