Bit-vector extension for SMACK

Please help me improve the code :)

Shaobo