[plagiarist]

I'd trust the SMT solver also! But if I read correctly you were only doing one insert at a time thus far? If you give it a try with multiple I hope you post again! This was a really neat project to read.