Implement API to set exit action to exception

[smoy]

Disclosure: I don't develop C/C++. I really just put this together by studying existing code.

Testing: In order to generate those unreachable code, i test the patch against 4.13.0 in macos.

>>> from z3 import *
>>> solver = Solver()
>>> A = SetSort(IntSort())
>>> B = SetSort(IntSort())
>>> solver.add(IsSubset(A, B) != (Union(A, B) == A))
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 388
UNEXPECTED CODE WAS REACHED.
Z3 4.13.0.1
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/smoy/github/z3-fork/build-dist/python/z3/z3.py", line 5074, in IsSubset
    return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/smoy/github/z3-fork/build-dist/python/z3/z3core.py", line 2351, in Z3_mk_set_subset
    _elems.Check(a0)
  File "/Users/smoy/github/z3-fork/build-dist/python/z3/z3core.py", line 1554, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'unreachable'