This is very cool, especially the automatic proof generation!
That said, I wonder if it would make more sense to use an SMT prover as fallback rather than a SAT solver. The latter requires converting the 32-bit operations into boolean circuits, which might not be the most efficient way to solve the problem considering modern SMT solvers such as Z3 and CVC5 already have built-in efficient support for bit-vectors?
In fact, I believe that's what Alive2 [1] does, which is a similar tool (although with slightly different goals).
I think it might even be possible to make this work for 64-bit vectors with SMT (in most cases).
I think MiniSAT was used precisely because it is dead easy to embed into WebAssembly. I'm aware that Z3 was also ported to WebAssembly, but it will be way larger...
That said, I wonder if it would make more sense to use an SMT prover as fallback rather than a SAT solver. The latter requires converting the 32-bit operations into boolean circuits, which might not be the most efficient way to solve the problem considering modern SMT solvers such as Z3 and CVC5 already have built-in efficient support for bit-vectors?
In fact, I believe that's what Alive2 [1] does, which is a similar tool (although with slightly different goals).
I think it might even be possible to make this work for 64-bit vectors with SMT (in most cases).
[1] https://github.com/AliveToolkit/alive2