It took a bit of time to orient myself not knowing much about the Z3 Python API, but that’s a very neat trick. Thanks for sharing!