Using Fixedpoint from Python API can trigger an uncaught crash/exception in C code

[phlummox]

Hi,

I came across the following issue while experimenting with the Python API for the z3 solver.

Software versions used

• z3 version: 4.8.15.0
• Python version: 3.9.12
  (also occurs using earlier versions; tested with Python 3.6.9 and Python 3.8.2)
• Operating system: Ubuntu 18.04, running Linux kernel 5.4.0-107-generic
  (also tested on Ubuntu 20.04)

z3 installation method

Using pip.

Can be replicated by running:

$ docker -D run --rm -it python:3.9.12 bash
# pip install --user "z3-solver==4.8.15.0"
# export PATH=~/.local/bin:$PATH

Steps to reproduce

Install the Python z3 library, save the following code as "crash_example.py", and run with python3 crash_example.py:

Click to expand code

from z3 import *

fp = Fixedpoint()
fp.set(engine='datalog')

Thing, (start, a, b, c, d, end) = EnumSort('Thing', ('start', 'a', 'b', 'c', 'd', 'end'))

connected  = Function('connected',  Thing, Thing, BoolSort())
fp.register_relation( connected)

fp.fact( connected(start, a)   )
fp.fact( connected(a, start)   )
fp.fact( connected(start, b)   )
fp.fact( connected(b, start)   )
fp.fact( connected(a, c)       )
fp.fact( connected(c, a)       )
fp.fact( connected(b, d)       )
fp.fact( connected(d, b)       )
fp.fact( connected(a, end)     )
fp.fact( connected(end, a)     )
fp.fact( connected(b, end)     )
fp.fact( connected(end, b)     )

res = fp.query( connected(start, d) )

Expected behaviour

fp.query should give a "sat" or "unsat" result depending on whether start is connected to d.

Actual behaviour

The program crashes with the following output:

ASSERTION VIOLATION
File: ../src/muz/rel/dl_relation_manager.cpp
Line: 380
Failed to verify: get_context().get_decl_util().is_numeral_ext(from, to)

Z3 4.8.15.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

Other notes

I may well be mis-using the Python API in some way; nevertheless, it seems like a bug if my Python code can trigger an assertion failure in the underlying C/C++ code.

The example code given is as small as I can get it, and seems to reliably cause crashes on a variety of Linux machines. Removing any of the "facts" asserted changes the behaviour and doesn't cause a C/C++ crash.