@all Thanks a lot for your awesome comments and feedback.
Besides compiler, emulator, and hypervisor, there is a symbolic execution engine in selfie that we are working on and would love to get feedback from you. The goal is to teach, eventually, a more formal approach when reasoning about correctness already in undergraduate classes. But the engine is also a research vehicle, especially the bounded model checking part.
We chose not to include support of Boolean operators and instead ask the students to implement that as part of an assignment. We use a self-grader for that. There is an assignment for bitwise Boolean operators. The assignment for logical Boolean operators with lazy evaluation is work in progress.