Question: How does crosshair work?

[RabbitDong-on]

I'm just starting to learn the symbolic execution and crosshair. I'm very interested in them.
In my understanding, Crosshair call the function i want to analyze and replace original objects with object proxies implemented by Crosshair. When the cpython interpreter executes the function, the methods, e.g., add, in object proxies will be invoked and generate path constraints.
For example, Crosshair implements LongProxy for Long.
def add(Long X, Long Y)->Long:
return X+Y
If there are two Long variable X and Y, Crosshair will translate x and y into LongProxy Xp and Yp.
The cpython interpreter executes Xp+Yp by invoking add implemented in LongProxy and generates a formula Xsym+Ysym.
Is this correct? Please let me know if there is any misunderstanding, thank you.
I have some questions.
(1)If there is a string varible S and the function invoke S.substring(), how to deal with this scenario. Does Crosshair also implement a special version of substring()?
(2) For a variable X in the function i want to analyze, any operations on X at the python language level will generate formulas like above example. Is it possible X used by the cpython interpreter at the C/C++ language level? If X is used by the cpython interpreter at the C/C++ language level, does this scenario generate formulas？
For example, here is a add method in cpython interpreter.

If left and right objects are symbolic variables, the sum in if statements needs generate some path constraints. Does crosshair need to consider this scenario?
I would really appreciate any help