open Microsoft.Z3