[BUG] Z3_dec_ref is None at program exit point

[ganler]

The function object Z3_dec_ref becomes None at the program exit point thus producing many annoying messages.

System environment:
OS: Linux ise-manjaro 5.10.70-1-MANJARO #1 SMP PREEMPT Thu Sep 30 15:29:01 UTC 2021 x86_64 GNU/Linux
Python version: 3.8

Relevant issues: #989

[NikolajBjorner]

If you are unloading the z3 library, as you seem to do, then you would also need to ensure there are no live objects before the library is retired.

[ganler]

@NikolajBjorner Thanks for the reply.

I did not manually unload any libraries including z3. Just wrote a program with many constraints and such kinds of warnings occur. The more constraints I have the more warnings I got.

For example the following constraints would lead to the warnings:

[i0 > 0,
 i1 > 0,
 i2 > 0,
 i3 > 0,
 i3 > 0,
 i1 > 0,
 i2 > 0,
 i0 > 0,
 i3 > 0,
 i1 > 0,
 i2 > 0,
 i0 > 0,
 i3 > 0,
 i1 > 0,
 i2 > 0,
 i0 > 0,
 i3 > 0,
 i1 > 0,
 i2 > 0,
 i0 > 0]
Exception ignored in: <function Solver.__del__ at 0x7fc2deb60ee0>
Traceback (most recent call last):
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/z3/z3.py", line 6866, in __del__
TypeError: 'NoneType' object is not callable
Exception ignored in: <function AstRef.__del__ at 0x7fc2deb46ca0>
Traceback (most recent call last):
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/z3/z3.py", line 354, in __del__
TypeError: 'NoneType' object is not callable
Exception ignored in: <function AstRef.__del__ at 0x7fc2deb46ca0>
Traceback (most recent call last):
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/z3/z3.py", line 354, in __del__
TypeError: 'NoneType' object is not callable
Exception ignored in: <function AstRef.__del__ at 0x7fc2deb46ca0>
Traceback (most recent call last):
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/z3/z3.py", line 354, in __del__
TypeError: 'NoneType' object is not callable
Exception ignored in: <function AstRef.__del__ at 0x7fc2deb46ca0>
Traceback (most recent call last):
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/z3/z3.py", line 354, in __del__
TypeError: 'NoneType' object is not callable
Exception ignored in: <function Context.__del__ at 0x7fc2deb46550>
Traceback (most recent call last):
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/z3/z3.py", line 219, in __del__
TypeError: 'NoneType' object is not callable
Exception ignored in: <function AGraph.__del__ at 0x7fc2dd4b9430>
Traceback (most recent call last):
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/pygraphviz/agraph.py", line 283, in __del__
  File "/home/ganler/anaconda3/lib/python3.8/site-packages/pygraphviz/agraph.py", line 1000, in _close_handle
TypeError: 'NoneType' object is not callable

[NikolajBjorner]

it's impossible to say without a repro. The stack you show suggests that there is a call to deleting a Context object.
The _close_handle call might perform some unloading.

[ganler]

@NikolajBjorner Thanks for the patience. I just found a minimal sample to repro. It seems to be a compatibility issue with PyTorch.

import torch
import z3

if __name__ == '__main__':
    p, q, r = z3.Ints('p q r')

    s = z3.Solver()
    s.add(p > 0)
    s.add(p > 0)
    s.add(r > 0)
    s.add(p > 0)
    s.add(p > 0)
    s.add(p > 0)
    s.add(p > 0)
    s.add(r > 0)
    s.add(p > 0)
    s.add(r > 0)
    s.add(r > 0)
    s.add(q > 0)
    s.add(p > 0)
    s.add(p > 0)
    s.add(p > 0)

    print(s)

    s.check()
    s.check()
    s.check()
    s.check()

[ganler]

@NikolajBjorner Found a workaround. It works fine if I import z3 first. I am not sure why this happens. Thanks for your patience.

[NikolajBjorner]

I tried to repro on my Windows 11:

C:\z3\build\python>python t.py
[p > 0,
p > 0,
r > 0,
p > 0,
p > 0,
p > 0,
p > 0,
r > 0,
p > 0,
r > 0,
r > 0,
q > 0,
p > 0,
p > 0,
p > 0]

It exits cleanly.

It could also relate to version of torch being used. I installed a fresh version right now.

[ganler]

My environment is Linux (Manjaro) and I am using PyTorch 1.10 with CUDA 11.3 support.

• pip3 install torch==1.10.0+cu113 torchvision==0.11.1+cu113 torchaudio==0.10.0+cu113 -f https://download.pytorch.org/whl/cu113/torch_stable.html

In addition to PyTorch, graphviz is also not compatible with z3 as you see in my second reply. My current workaround is to only generate a graph descriptor and use external executable binary (i.e., dot) to convert it into a PNG file.

[ganler]

This bug seems to only occur on my PC. I tried it on Colab and it works fine.

[NikolajBjorner]

I tried with both torch and graphviz on my end (and it has been tested in many other settings before).

[sergei-mironov]

Sorry to say this, but I have the very same problem.
Linux (NixOS 21.05), Python 3.8, z3 4.8.12

[r4dr3fr4d]

I have this issue as well - happens whenever there's some error in my code or if I call exit().