Programming Constraint Services with Z3 (Nikolaj Bjørner, ISPRASOPEN-2019)