search

dapphub / k-dss

formal verification of multicollateral dai in the K framework
GNU Affero General Public License v3.0
45 stars 25 forks source link

catch up to latest implementation #10

Closed livnev closed 6 years ago

livnev commented 6 years ago

This is up to date with current dss master branch.

ehildenb commented 6 years ago

@livnev one way to mitigate the issue of the mystery K crashes is to re-run the proof on initial failure in the Makefile. Replace:

%.test: pre-test
    klab run --headless --force --spec $*

with:

%.test: pre-test
    klab run --headless --force --spec $* \
        || klab run --headless --force --spec $*

If the first invocation fails, the second will be called. If the first succeeds, the second will not be called, if the second succeeds, it succeeds overall.

livnev commented 6 years ago

@ehildenb Nice, that should help until we figure out the cause of the issue.

livnev commented 6 years ago

Closing in favour of #13