fix bug in soundness check
revert parallel enumeration for guard-splitting
don't create/destroy maybe in par_next and bfs_next
remove unnecessary code
Correctly use Abort when spec is unsound
add doc for --no-soundness-check
check correct use of --no-soundness-check
use enum for guard-splitting mode