Add test case for non-chronological symbolic execution

BacktrackDfsChecker keeps assertions separate from guards so it
doesn't matter where assertions are encountered in the program.