As Nate Osgood as shown over Zulip, making the symbolic model use a HomExpr comes with the assumption that the theory has dom and codom available (this gets used in the show method for the hom generators). This assumption is not valid for ThPreorder which has lhs and rhs as its accessors, so there is an error when trying to show them.
A possible solution is to just make the symbolic model use GATExprs.