Use of setjmp() and longjmp(): In C/C++, setjmp() saves the contents of the registers at a particular state in the program and longjmp() will restore that state later. In this way, longjmp() “returns” to the state of the program when setjmp() was called.
In general these functions are problematic for C++ because they do not support C++ object semantics. In particular, they do not ensure the proper destructor calls and so objects may not be cleaned up properly, leaving the system in a bad state.
Using these functions may also degrade performance by preventing optimization on local variables. For C++ exception handling, try/catch constructs are recommended instead.
For model checking in particular, non-hierarchical long jumps are difficult to model with modeling languages like Java. These functions need to do register restoration which requires modeling of registers and their related operations, adding considerable overhead to model-checking effort.