Discard buggy test case added in previous commit and add new test cases

This patch has an intesresting test case for 16 bit multiplication
operation. For 32-bit, the stp solver was found to hang but Z3 worked.