This seems to be an instance of concolic execution which has seen some success in the fuzzing and testing research community. The key ideas originate from these papers:
The technique works well when parts of the program space (including paths through the program) can be easily represented in SMT solvers (like booleans, bit vectors, and arithmetic), and the remainder program space can be explored using random testing. I am excited to see this work being brought to Crosshair in Python via Hypothesis!
[1] https://web.eecs.umich.edu/~weimerw/590/reading/p213-godefro...
[2] https://mir.cs.illinois.edu/marinov/publications/SenETAL05CU...
The Wikipedia page gives a good overview of the area and some successful applications: https://en.wikipedia.org/wiki/Concolic_testing
The technique works well when parts of the program space (including paths through the program) can be easily represented in SMT solvers (like booleans, bit vectors, and arithmetic), and the remainder program space can be explored using random testing. I am excited to see this work being brought to Crosshair in Python via Hypothesis!