Accessing Symbolic State or Path Conditions in CrossHair for Research Use

[Stefania-P11]

I’m working on extending DIG (https://github.com/dynaroars/dig), a tool that uses CIVL to generate invariants for C programs, to support Python analysis. I’m exploring how CrossHair might fit into this pipeline.

I have two main questions:

1. Does CrossHair internally generate symbolic states over inputs during execution? If so, is there a way to extract or inspect those symbolic states?

2. Is there a way to obtain path conditions at a specific program point — e.g., by inserting an assert and retrieving the input constraints that reach that point?

Any pointers on how CrossHair handles symbolic state under the hood or where to hook in would be greatly appreciated.