Create symbolic execution library for sequential code

The native symbolic execution of sequential code is much simpler
than the one for concurrent code. So we distinguish these features
to improve the modularity and extensibility of the library.