GNU/Linux ◆ xterm-256color ◆ zsh 428 views

This illustrates how invoking the satisfiability check in the scope of a function (here gen_goal) results in different behaviour to an invocation out of the function’s scope. Seems to be a Python garbage collection issue. Check Z3 issue #2784 for more details.