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/ https://unsat.cs.was

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/ https://unsat.cs.washington.edu/projects/serval/ IIUC Serval uses an interpreter built in Rosette (?) to build a Symbolic execution tool.