Swire42

There seem to be some minor issue with the naming of variables in the generated SMT constraints. I'll work on that and let you know once it works on `five`

I have fixed the issues. To verify `five`, you will need #135, as DontCare values are used. On my machine, the verification time goes from 2 minutes with the old...

It turns out that I was not catching some errors from z3's stderr, and that z3 was spitting meaningless sat/unsat result in stdout as a consequence... I'll push an updated...

So... it seems that it wasn't that I wasn't catching the error, but rather that z3 was just not producing any errors, just incorrect results... I had several datatypes sharing...

z3 issue: https://github.com/Z3Prover/z3/issues/7212

On the topic of performance, I am currently pondering on the idea of not using datatypes. It would seem that getting rid of datatypes would allow running z3 in parallel...

I come with good and bad news: - I have managed to inductively verify 3/4 of the correctness properties of Five, using a new verification procedure, after some more proof-testing,...

Let me know if you fix the the forward progress properties so that they have a chance of getting verified inductively. Indeed, with LogRegs=1, even "Operands Correct" gets verified.

I have also since then managed to verify with LogRegs=2, but that took 5h. An interesting fact is that the required induction depth for "Operands Correct" is 7 with this...

I think a good solution to handle this would be to split registers in two (or more) parts, such that the resulting registers are either fully initialized or fully uninitialized.