Essentially we implement [Podelski/Rybalchenko](https://www.cs.cmu.edu/~hzarnani/fm-rg/cmuonly/podelski04complete.pdf)