Finished replacing the old constraint solver with Z3, noticed a substantial slowdown.
Revised the SMT interface, added yices and successfully compiled, but some assertions fail during runtime.