I asked Zac why in his class do we use this formal methods stuff for symbolic evaluation where we track both branches to figure out the constraint.
Why can't we just do term replacement???
So I [built up an example using egglog to do it]https://colab.research.google.com/drive/1xsBLbMq1nya_ZwqestEMH8XkiMKoZCnA#scrollTo=dc2682fd)
When I asked him about it he said this is what he thought symbolic evaluation was too until he had to teach this class. He isn't sure why people don't do it the other way. Maybe just before they didn't have e-graphs so it was harder without that foundaton? He thought maybe redoing the seminal paper might be an OK way to see how it works
https://madhu.cs.illinois.edu/cs598-fall10/king76symbolicexecution.pdf