Z3 crash on Python exit after creating Lambda expression

[daniel-larraz]

$ python
Python 3.12.3 (main, Apr 26 2024, 09:58:40) [GCC 9.4.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> x = Int('x')
>>> f = Lambda(x, x + 1)
>>> exit()
ASSERTION VIOLATION
File: /tmp/build-via-sdist-tued87mr/z3_solver-4.14.1.0/core/src/ast/ast.cpp
Line: 406
UNEXPECTED CODE WAS REACHED.
4.14.1.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
terminate called after throwing an instance of 'default_exception'
  what():  unreachable
Aborted (core dumped)

[NikolajBjorner]

check your include paths. This doesn't repro for me. Tends to be issue with a header file left over from a previous version of z3.

[daniel-larraz]

I can reproduce the issue using this Dockerfile on Ubuntu 20.04:

FROM python:3.12-slim

ENV DEBIAN_FRONTEND=noninteractive

# Install the problematic Z3 version
RUN pip install z3-solver==4.14.1.0

# Set working directory
WORKDIR /app

# Start an interactive shell
CMD ["python"]

Then run:

$ docker build -t z3-shell-crash .
$ docker run -it --rm z3-shell-crash

Inside the interactive Python shell:

Python 3.12.10 (main, Apr 28 2025, 22:12:29) [GCC 12.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> x = Int('x')
>>> f = Lambda(x, x + 1)
>>> exit()

This results in:

ASSERTION VIOLATION
File: /tmp/build-via-sdist-tued87mr/z3_solver-4.14.1.0/core/src/ast/ast.cpp
Line: 406
UNEXPECTED CODE WAS REACHED.
4.14.1.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
terminate called after throwing an instance of 'default_exception'
  what():  unreachable

Note: This crash only occurs when entering the commands manually in the interactive shell. If the same code is run from a script, the issue does not occur.

[NikolajBjorner]

C:\z3\build\python>python
Python 3.12.10 (tags/v3.12.10:0cc8128, Apr  8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> x = Int('x')
>>> f = Lambda(x, x + 1)
>>> print(f)
Lambda(x, x + 1)

this is for the latest build, so not conclusive for the release.

[NikolajBjorner]

C:\tmp\x>python
Python 3.12.10 (tags/v3.12.10:0cc8128, Apr  8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> get_version()
(4, 14, 1, 0)
>>> x = Int('x')
>>> f = Lambda(x, x + 1)
>>> print(f)
Lambda(x, x + 1)
>>> exit()
ASSERTION VIOLATION
File: ..\..\src\ast\ast.cpp
Line: 406
UNEXPECTED CODE WAS REACHED.
Z3 4.14.1.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new