Assertion violation in PbEq with integer parameter

[dan-simon]

I'm using the Python z3 library and got the following error:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 414
UNEXPECTED CODE WAS REACHED.
Z3 4.8.14.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

via code which I managed to simplify to:

from z3 import Int, PbEq

x = Int('x')

PbEq([(x == 0, 1), (x == 1, 1), (x == 0, 1), (x, 1)], 0)

It seems like the issue with this code is x, which is an integer, being used as a boolean, and many small changes to this code (e.g. removing one of the first three terms, or doing PbEq([(x == 0, 1), (x == 0, 1), (x == 1, 1), (x, 1)], 0) instead) will instead give the error "invalid non-Boolean sort applied to 'at-most'". It appears, from a few tests, that "UNEXPECTED CODE WAS REACHED." only occurs when there are at least three items in the list passed to PbEq (in addition to the item (x, 1)), and, if there are exactly three other items, when no two consecutive items are the same.

I tried to look at the source but the issue seemed deep enough to be hard to find.

Z3 version: Z3 version 4.8.14 - 64 bit
Python version: Python 3.8.3
Operating system: macOS Big Sur (11.3)