If you want to use Z3 with a .NET language, there is also this very useful file with examples of how to use the bindings: https://github.com/Z3Prover/z3/blob/m

If you want to use Z3 with a .NET language, there is also this very useful file with examples of how to use the bindings: https://github.com/Z3Prover/z3/blob/master/examples/dotnet/Program.cs https://github.com/Z3Prover/z3/blob/master/examples/dotnet/P... The examples are in C#, but easy to adapt to other languages. I found them quite useful to write a program for symbolic execution in F# that calls Z3 to simplify conditionals, here is its interface to Z3: https://github.com/constructum/asm-symbolic-execution/blob/main/SmtInterface.fs https://github.com/constructum/asm-symbolic-execution/blob/m... The bindings are perhaps a bit cumbersome, but rather easy to understand and work very well. Once you appropriately wrap what you need, you can forget about the bindings as well as avoiding SMT-LIB completely.