[baq]

What’s missing here is ‘prepare a Z3 script in a <z3-verification> tag with your thinking encoded and wait for the tool run and its output before continuing’