Just do some math

`1000 + 15 & -16`

Find out whether two expression are equivalent

`let x = a + b in (x < a) == (x < max(a, b))`

*Prove* that two expressions are equivalent

`a ^ ((a ^ b) & mask) == (a & ~mask) | (b & mask)`

Find when two expressions are equal and when they are not

`x == -x`

== binds less strongly than bitwise operators.

Finding proofs can be slow and often nothing is found at all.

The BDD structural matcher has not been fully ported yet.

~~Division, remainder and multiplication will not work if both operands are variable, and even in some cases where one operand is a constant. That's not a bug but an inherent limitation of the techniques used. This situation may be improved (with reduced functionality) someday if I get around to coding up the SAT fallback.~~

SAT fallback now exists, using MiniSat compiled with Emscripten. This is brand new so expect bugs (not due to MiniSat, but for example I don't entirely trust my circuit builder and circuit-to-SAT converter). It takes a while before haroldbot gives up on BDDs and switches to SAT, even if it could have known from the start that BDDs were never going to work. I'll probably improve that.

In general, there *are* many bugs.

Since everything happens client-side now, I don't get automatic bug reports. Please open an issue or contact me (if you know how).