Some spec fixes - Githubissues

makerdao / k-dss

formal verification of multicollateral dai in the K framework

GNU Affero General Public License v3.0

14 stars 11 forks source link

Closed ehildenb closed 4 years ago

ehildenb commented 4 years ago

Removes a formatting error which prevented the Jug rpow loop invariant from being generated.
Switches hardcoded storage locations for DSValue to macro ones.