search

Orbis-Tertius / tinyram

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

cmpaNegTestCase Coq discrepancy #69

Open derekverbrugge opened 2 years ago

derekverbrugge commented 2 years ago

Steps to reproduce: Running https://github.com/Orbis-Tertius/tinyram/tree/cmpaNegTestCaseBugwill produce an error with the cmpgeLessTestCase

Expected behavior: Expected to answer 0.

Actual behavior: Coq produces the wrong answer, 65534, in conflict with TinyRam which results in 0.