search

Orbis-Tertius / tinyram

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

cmpaNegTestCaseL Coq discrepancy bug. #78

Open derekverbrugge opened 2 years ago

derekverbrugge commented 2 years ago

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

Expected behavior: Expected to answer 0.

Actual behavior: Coq results in 2 which is wrong, and Haskell results in 0.