Optimize correctly using own translator

Passes the test that broke MiniSat+!  Fixed correctness bug in my inequality-to-SAT translator and wrote some unit tests for it.