Mauro Bringolf

`args` makes sense to me, although there is some overlap with arguments that are not instructions but literals (indices, numberliterals). These are currently also stored under `args`, in `i32.const 0`...

My motivation for this was that in #306, in the type checker and conceptually it seems more natural to have locals as a property of the function node. I just...

Yes, thats what I started doing in the `nan-payloads` branch. Theyre still number literals and I have a couple of things to fix in JSON (`NaN`, `Infinity` and hex literals)....

#49 Fixes the test issue with `+-0`. I think its enough to store the extra information for `NaN`s. My idea would be to make a `maybeNumber` type that looks something...

The solution suggested by @leeb003 works perfectly for me. Thank you! I'd be very interested in an updated version of this plugin.

Any updates on this? Is there something a new contributor could help with? So far I am a happy user of `qcheck` (thanks!) and recently ran into https://github.com/c-cube/qcheck/issues/197 and would...

I just ran the example given above through a version of my fork and successfully verified it. The quantifiers in the postcondition of `main` are translated as follows (identifiers manually...

Claimed ✋

Just for reference, without further investigation: This verifies in my fork with semantic heap snapshots.

Thank you for reporting the issue. Based on a first look, I am not yet sure where exactly the non-termination is coming from. But like you, I don't think it...