Z3 Theorem Prover

The Z3 Theorem Prover / SMT solver is developed by Microsoft Research under the MIT license.

To run this test with the Phoronix Test Suite, the basic command is: phoronix-test-suite benchmark z3.

Project Site

github.com

Source Repository

github.com

Test Created

5 May 2023

Test Maintainer

Lucian Popescu

Test Type

Processor

Average Install Time

3 Minutes, 48 Seconds

Average Run Time

3 Minutes, 24 Seconds

Test Dependencies

C/C++ Compiler Toolchain + Python + CMake

Accolades

5k+ Downloads

Supported Platforms

Supported Architectures

x86_64

* Uploading of benchmark result data to OpenBenchmarking.org is always optional (opt-in) via the Phoronix Test Suite for users wishing to share their results publicly.
** Data based on those opting to upload their test results to OpenBenchmarking.org and users enabling the opt-in anonymous statistics reporting while running benchmarks from an Internet-connected platform.
Data updated weekly as of 3 December 2023.

Revision History

pts/z3-1.0.0 [View Source] Fri, 05 May 2023 12:58:31 GMT
Upload Z3 theorem prover test profile from https://github.com/phoronix-test-suite/test-profiles/pull/273 with various cleanups/improvements. Closes: https://github.com/phoronix-test-suite/test-profiles/pull/273

Performance Metrics

Analyze Test Configuration:

Z3 Theorem Prover 4.12.1

SMT File: 1.smt2

OpenBenchmarking.org metrics for this test profile configuration based on 345 public results since 5 May 2023 with the latest data as of 7 December 2023.

Below is an overview of the generalized performance for components where there is sufficient statistically significant data based upon user-uploaded results. It is important to keep in mind particularly in the Linux/open-source space there can be vastly different OS configurations, with this overview intended to offer just general guidance as to the performance expectations.

Component

Percentile Rank

# Compatible Public Results

Seconds (Average)

Intel Core i9-13900K

99th

14.0 ^{+/- 0.1}

AMD Ryzen 7 7800X3D 8-Core

96th

14.5 ^{+/- 0.2}

AMD Ryzen 7 5800X3D 8-Core

93rd

17.8 ^{+/- 0.8}

AMD Ryzen 9 7950X 16-Core

92nd

18.4 ^{+/- 1.3}

AMD Ryzen 7 7700X 8-Core

89th

19.1 ^{+/- 0.3}

Intel Core i5-12600K

88th

19.1

Intel Xeon Platinum 8462Y

87th

19.3 ^{+/- 0.4}

AMD Ryzen 9 7900X 12-Core

86th

19.3 ^{+/- 0.5}

AMD Ryzen 7 7700 8-Core

85th

19.4 ^{+/- 0.1}

2 x Intel Xeon Gold 6442Y

79th

20.0

AMD Ryzen 9 7900 12-Core

78th

20.1 ^{+/- 0.2}

AMD Ryzen 5 7600X 6-Core

76th

20.4 ^{+/- 0.1}

Mid-Tier

75th

> 20.5

Intel Xeon Platinum 8468

74th

20.5 ^{+/- 0.3}

2 x Intel Xeon Platinum 8468

72nd

20.7 ^{+/- 0.3}

Intel Xeon Gold 6444Y

70th

21.0 ^{+/- 0.3}

AMD Ryzen 9 7900X3D 12-Core

70th

21.2 ^{+/- 0.2}

2 x AMD EPYC 7373X 16-Core

66th

21.5 ^{+/- 0.3}

2 x AMD EPYC 9684X 96-Core

63rd

21.8 ^{+/- 0.1}

Intel Core i5-10500

61st

22.9 ^{+/- 0.3}

2 x AMD EPYC 7773X 64-Core

59th

23.1 ^{+/- 0.1}

AMD Ryzen 9 5950X 16-Core

56th

23.4 ^{+/- 0.5}

AMD Ryzen 7 5800X 8-Core

55th

23.5 ^{+/- 0.2}

2 x Intel Xeon Platinum 8380

52nd

24.9 ^{+/- 0.7}

Intel Xeon E-2388G

52nd

24.9 ^{+/- 0.1}

Median

50th

25.0

2 x AMD EPYC 9554 64-Core

46th

26.5 ^{+/- 0.3}

2 x AMD EPYC 9654 96-Core

46th

26.5 ^{+/- 0.3}

Intel Xeon E-2336

42nd

27.2 ^{+/- 0.1}

2 x Intel Xeon Max 9480

41st

27.4 ^{+/- 0.4}

Intel Core i7-1165G7

40th

29.1 ^{+/- 0.7}

AMD Ryzen 9 3900XT 12-Core

39th

29.4 ^{+/- 0.1}

Intel Core i7-1065G7

38th

29.7 ^{+/- 0.3}

AMD Ryzen Threadripper 3970X 32-Core

37th

29.9

AMD Ryzen 7 7840U

36th

30.0 ^{+/- 1.3}

Intel Core i7-1185G7

32nd

31.0 ^{+/- 0.1}

AMD Ryzen 9 5900HX

31st

31.3 ^{+/- 0.1}

AMD Ryzen Z1 Extreme

30th

31.5 ^{+/- 0.8}

AMD Ryzen 7 PRO 7840U

26th

33.5 ^{+/- 0.2}

AMD Ryzen Threadripper 3990X 64-Core

26th

33.6 ^{+/- 0.1}

Low-Tier

25th

> 33.6

2 x AMD EPYC 9754 128-Core

22nd

34.9 ^{+/- 0.2}

Intel Core i7-5960X

22nd

34.9

AMD Ryzen 7 PRO 5850U

21st

35.6 ^{+/- 0.7}

AMD EPYC 7F32 8-Core

21st

35.6

AMD Ryzen 7 6800U

18th

36.6 ^{+/- 0.3}

Intel Core i9-10980XE

16th

37.8 ^{+/- 0.3}

Intel Xeon Silver 4216

14th

38.6

AMD Ryzen 7 PRO 6850U

13th

38.8 ^{+/- 0.7}

AMD Ryzen 5 4500U

9th

43.4 ^{+/- 0.1}

Intel Core i7-8565U

8th

43.7 ^{+/- 0.3}

AMD Ryzen 7 4800U

7th

44.6 ^{+/- 1.4}

AMD Ryzen 5 5500U

6th

44.9 ^{+/- 0.7}

AMD EPYC 7551 32-Core

5th

45.9 ^{+/- 0.8}

Based on OpenBenchmarking.org data, the selected test / test configuration (Z3 Theorem Prover 4.12.1 - SMT File: 1.smt2) has an average run-time of 2 minutes. By default this test profile is set to run at least 3 times but may increase if the standard deviation exceeds pre-defined defaults or other calculations deem additional runs necessary for greater statistical accuracy of the result.

Based on public OpenBenchmarking.org results, the selected test / test configuration has an average standard deviation of 0.3%.

Does It Scale Well With Increasing Cores?

No, based on the automated analysis of the collected public benchmark data, this test / test settings does not generally scale well with increasing CPU core counts. Data based on publicly available results for this test / test settings, separated by vendor, result divided by the reference CPU clock speed, grouped by matching physical CPU core count, and normalized against the smallest core count tested from each vendor for each CPU having a sufficient number of test samples and statistically significant data.

Notable Instruction Set Usage

Notable instruction set extensions supported by this test, based on an automatic analysis by the Phoronix Test Suite / OpenBenchmarking.org analytics engine.

Instruction Set

Support

Instructions Detected

SSE2 (SSE2)

Used by default on supported hardware.

MOVDQA MOVDQU CVTSI2SD DIVSD PUNPCKLQDQ MOVD SUBSD UNPCKLPD MOVAPD COMISD XORPD ADDSD SHUFPD MULSD CVTTSD2SI CVTSD2SS UCOMISD PSHUFD CVTSS2SD PSRLDQ MAXSD CVTDQ2PD CMPLTPD ANDPD ADDPD MOVUPD DIVPD SQRTSD MINSD PADDQ PUNPCKHQDQ MULPD CVTDQ2PS ANDNPD CMPNLESD ORPD PMULUDQ UNPCKHPD CMPLTSD MOVHPD MOVLPD CMPLESD SUBPD SQRTPD

SSE 4.2 (SSE4_2)

Requires passing a supported compiler/build flag (verified with targets: sandybridge, skylake, tigerlake, cascadelake, sapphirerapids, alderlake, znver2, znver3).
Found on Intel processors since at least 2010.
Found on AMD processors since Bulldozer (2011).

POPCNT

Advanced Vector Extensions (AVX)

Requires passing a supported compiler/build flag (verified with targets: sandybridge, skylake, tigerlake, cascadelake, sapphirerapids, alderlake, znver2, znver3).
Found on Intel processors since Sandy Bridge (2011).
Found on AMD processors since Bulldozer (2011).

VZEROUPPER VEXTRACTF128 VINSERTF128 VBROADCASTSD VBROADCASTSS VPERM2F128 VPERMILPD

Advanced Vector Extensions 2 (AVX2)

Requires passing a supported compiler/build flag (verified with targets: skylake, tigerlake, cascadelake, sapphirerapids, alderlake, znver2, znver3).
Found on Intel processors since Haswell (2013).
Found on AMD processors since Excavator (2016).

VINSERTI128 VEXTRACTI128 VPBROADCASTQ VPBROADCASTD VPERM2I128 VPSLLVD VPSRLVD VPGATHERQD VPGATHERQQ VPERMQ VPMASKMOVQ VPERMPD VPERMD VPMASKMOVD VPBROADCASTB VPBROADCASTW

FMA (FMA)

VFMADD231SD VFMADD132SD VFMADD213SD VFNMADD231SD VFMSUB132SD VFNMADD132SD VFNMADD213SD VFMSUB231SD

Advanced Vector Extensions 512 (AVX512)

Requires passing a supported compiler/build flag (verified with targets: cascadelake, sapphirerapids).

(ZMM REGISTER USE)

The test / benchmark does honor compiler flag changes.

Last automated analysis: 25 June 2023

This test profile binary relies on the shared libraries libm.so.6, libc.so.6.

Tested CPU Architectures

This benchmark has been successfully tested on the below mentioned architectures. The CPU architectures listed is where successful OpenBenchmarking.org result uploads occurred, namely for helping to determine if a given test is compatible with various alternative CPU architectures.

CPU Architecture

Kernel Identifier

Verified On

Intel / AMD x86 64-bit