Applying SMT in Symbolic Execution of Microcode