I created a solver for it using Z3, see https://news.ycombinator.com/item?id=19093754.