Testsuite fails on s390x with 4.10.2

[nmeum]

Hi, I maintain an Alpine Linux package for z3. While upgrading the Alpine package from 4.10.1 to 4.10.2, I noticed that the test suite fails on the s390x architecture with 4.10.2 while it passed fine on 4.10.1. The testsuite also passes on all other architectures supported by Alpine (x86, x86_64, armhf, armv7, ppc64le, riscv64 and aarch64). Of these architectures, s390x is the only big-endian architecture.

The test failure looks as follows:

test dl_table :time 0.11 :before-memory 33.08 :after-memory 33.08)
PASS
(test dl_context :time 0.00 :before-memory 33.08 :after-memory 33.08)
PASS
(test dl_context :time 0.00 :before-memory 33.08 :after-memory 33.08)
PASS
(test dl_util :time 0.00 :before-memory 33.08 :after-memory 33.08)
PASS
(test dl_util :time 0.00 :before-memory 33.08 :after-memory 33.08)
ASSERTION VIOLATION
File: /home/buildozer/aports/community/z3/src/z3-z3-4.10.2/src/test/dl_product_relation.cpp
Line: 68
Failed to verify: t0->get_size_estimate_rows()==2

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

The complete build log: z3-4.10.2-s390x.txt

We build z3 as follows:

cmake -B build -G Ninja \
	-DZ3_BUILD_PYTHON_BINDINGS=True \
	-DZ3_INSTALL_PYTHON_BINDINGS=True \
	-DPYTHON_EXECUTABLE=/usr/bin/python3 \
	-DCMAKE_INSTALL_PREFIX=/usr \
	-DCMAKE_INSTALL_LIBDIR=lib \
	-DBUILD_SHARED_LIBS=True \
	-DCMAKE_BUILD_TYPE=MinSizeRel
cmake --build build

# Binary for running the unit tests
cmake --build build --target test-z3

# Run the tests
./build/test-z3 -a

Let me know if you need more information.

[NikolajBjorner]

can you bisect and point out what commit caused the regression?
I don't have alpine s390x set up.

[NikolajBjorner]

What is the number of z3 users from s390x on Alpine Linux?

[nmeum]

can you bisect and point out what commit caused the regression?

7823757 (so looks like the code itself was broken prior to 4.10.2).

What is the number of z3 users from s390x on Alpine Linux?

I don't know, we don't collect any statistics.

[waywardmonkeys]

@nmeum Looks like your comment about this being the only big endian platform that is tested might be important.

Any chance you could narrow things down a bit further as to where we might have a dependence on little vs big endian?

(And then open a new bug...)

[nmeum]

@nmeum Looks like your comment about this being the only big endian platform that is tested might be important.

Yes, looks like it.

Any chance you could narrow things down a bit further as to where we might have a dependence on little vs big endian?

Unfortunately, my time is currently very limited. I also don't use z3 on s390x, I just maintain the Alpine package and use it myself on x86_64. However, I would like to point out that qemu also has s390x support, which might be an option to narrow this down further in case someone else has time/interest to do so.

[matoro]

Hi, I would like to report that this also occurs on sparc, so that's further evidence this is an endian issue. I have hardware I can make available for testing - would anyone be willing to investigate if I can provide a shell? I'd rather the underlying issue get fixed rather than re-disabling the tests!