Produce executable error trace in bitcode

[shaobo-he]

Since SMACK makes a block-to-block correspondence from Boogie to LLVM IR, we should be able to get an executable error trace in bitcode which is call-free, branch-free, and well-defined.