MrChico
MrChico
You would have to look into which opcode this error is thrown on to get a clue about what specifically is not supported here, I agree that it looks like...
Whatever opcode it crashes on if you step carefully would be the culprit
Related to this issue from the 18th century #38
lgtm
getting annoying, mysterious errors in the communication with the solver and sbv ``` *** Data.SBV: Unexpected response from the solver, context: push: *** *** Sent : (push 1) *** Expected...
probably easiest to simply let `--json-file` be a list and merge it inside hevm
This is a known issue, unfortunately, that I once thought I solved with #582, but it has reappeared lately. Its only present with cvc4 in some particular circumstances. As a...
Long term we should investigate further if the situation can be improved in sbv, but also make z3 the default solver again
Exciting! I think this is a good approach to ameliorate the biggest pain point with a small change. Will investigate the consequences