I think you remember wrong. Rust is moving towards using a datalog engine, but for lifetime resolution (the project is called Polonius), not for type checking. Datalog engines have some similarities with SMT solvers so this might be what you're thinking of.