How to convert neural network for solvers like Microsoft Z3 or any SAT solvers?

I have seen many papers where they verify neural networks. Either they try to check adversarial robustness or finds an input that the model predicts incorrectly. They try to convert a layer to a mathematical equation for eg a boolean expression. And then solves it by available solvers (Microsoft Z3, Gurobi). But I could not find any tutorial or starting code.

Can you help me start the process? For example, share a code to convert one fully connected layer with ReLu activation for MNIST data. Then I can build on top of that for a more complex layer.