[touisteur]

By the way I kept going down this rabbit-hole and found an example of what you described : https://unsat.cs.washington.edu/projects/serval/

IIUC Serval uses an interpreter built in Rosette (?) to build a Symbolic execution tool.