search

Orbis-Tertius / tinyram

A vnTinyRAM emulator.
Apache License 2.0
4 stars 1 forks source link

notFlagTestCase Coq discrepancy #97

Open derekverbrugge opened 2 years ago

derekverbrugge commented 2 years ago

Steps to reproduce: Running https://github.com/Orbis-Tertius/tinyram/pull/96 will produce an error with the notFlagTestCase

Expected behavior: Expected to answer -11. (65524)

Actual behavior: Coq results in 65535 which is wrong, and Haskell results in 65524 which is correct.