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

Last Updated

16 July 2024

Test Maintainer

Lucian Popescu

Test Type

Processor

Average Install Time

3 Minutes, 46 Seconds

Average Run Time

4 Minutes, 27 Seconds

Test Dependencies

C/C++ Compiler Toolchain + Python + CMake

Accolades

10k+ Downloads

Supported Platforms

Supported Architectures

x86_64 + aarch64

* 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 17 September 2024.

Revision History

pts/z3-1.0.1 [View Source] Tue, 16 Jul 2024 12:59:39 GMT
Enable AArch64 support, change broken download URLs. Closes: https://github.com/phoronix-test-suite/test-profiles/issues/295

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: 2.smt2

OpenBenchmarking.org metrics for this test profile configuration based on 774 public results since 5 May 2023 with the latest data as of 18 September 2024.

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)

AMD Ryzen 7 9700X 8-Core

97th

AMD Ryzen 9 9950X 16-Core

95th

36 ^{+/- 1}

AMD Ryzen 9 9900X 12-Core

95th

36 ^{+/- 1}

AMD Ryzen 5 9600X 6-Core

95th

37 ^{+/- 1}

AMD Ryzen 7 7700X 8-Core

88th

45 ^{+/- 1}

AMD Ryzen 9 7950X 16-Core

88th

46 ^{+/- 1}

AMD Ryzen 9 7900X 12-Core

85th

47 ^{+/- 1}

AMD Ryzen 7 7700 8-Core

85th

47 ^{+/- 1}

AMD Ryzen 9 7900 12-Core

85th

47 ^{+/- 2}

AMD Ryzen 7 7800X3D 8-Core

85th

47 ^{+/- 1}

AMD EPYC 4484PX 12-Core

82nd

AMD EPYC 4584PX 16-Core

79th

AMD EPYC 4344P 8-Core

78th

AMD Ryzen 5 7600 6-Core

78th

48 ^{+/- 1}

AMD Ryzen 9 7950X3D 16-Core

77th

48 ^{+/- 4}

AMD Ryzen 5 7600X 6-Core

77th

48 ^{+/- 2}

AMD EPYC 4364P 8-Core

77th

AMD Ryzen 9 7900X3D 12-Core

77th

49 ^{+/- 4}

AMD Ryzen Threadripper PRO 7995WX 96-Cores

76th

49 ^{+/- 1}

Mid-Tier

75th

> 49

AMD EPYC 4564P 16-Core

75th

AMD EPYC 4244P 6-Core

73rd

AMD Ryzen Threadripper 7980X 64-Cores

72nd

49 ^{+/- 1}

Intel Core i9-14900K

70th

AMD EPYC 4464P 12-Core

69th

Intel Core i9-13900K

67th

52 ^{+/- 2}

AMD Ryzen 7 8700G

66th

53 ^{+/- 2}

AMD Ryzen 5 8600G

62nd

54 ^{+/- 2}

AMD Ryzen 5 8400F 6-Core

61st

AMD EPYC 4124P 4-Core

58th

AMD Ryzen 7 5800X3D 8-Core

57th

58 ^{+/- 2}

Intel Core i5-14600K

56th

58 ^{+/- 1}

AMD Ryzen 7 5800X 8-Core

54th

AMD Ryzen 9 5950X 16-Core

54th

59 ^{+/- 1}

Intel Core i5-13600K

52nd

Median

50th

AMD Ryzen 5 5600X 6-Core

50th

61 ^{+/- 1}

ARMv8 Neoverse-N1 160-Core

50th

61 ^{+/- 8}

AMD Ryzen 9 5900X 12-Core

50th

61 ^{+/- 1}

AMD Ryzen 7 7840HS

50th

61 ^{+/- 2}

Intel Core i5-14500

48th

AMD Ryzen 7 7840U

48th

62 ^{+/- 1}

Intel Xeon E E-2488

46th

63 ^{+/- 1}

Intel Core i5-12600K

46th

AMD Ryzen 7 8845HS

45th

64 ^{+/- 2}

AMD Ryzen Z1 Extreme

44th

65 ^{+/- 1}

2 x Intel Xeon E5-2620 v2

43rd

AMD Ryzen 7 3800XT 8-Core

43rd

67 ^{+/- 1}

Intel Core i5-14400F

43rd

AMD Ryzen 7 PRO 7840U

41st

Intel Core i5-13400

41st

2 x AMD EPYC 9684X 96-Core

41st

2 x AMD EPYC 9554 64-Core

39th

69 ^{+/- 1}

Intel Core i3-14100

39th

69 ^{+/- 1}

2 x AMD EPYC 7373X 16-Core

37th

2 x AMD EPYC 9654 96-Core

35th

71 ^{+/- 1}

Intel Xeon E-2388G

33rd

72 ^{+/- 1}

Intel Xeon Platinum 8462Y

30th

73 ^{+/- 1}

AMD Ryzen 9 5900HX

30th

73 ^{+/- 3}

2 x AMD EPYC 7773X 64-Core

28th

75 ^{+/- 1}

2 x Intel Xeon Gold 6442Y

28th

AMD Ryzen 5 5500

28th

75 ^{+/- 2}

Intel Xeon Gold 6444Y

28th

75 ^{+/- 1}

Low-Tier

25th

> 76

Intel Core Ultra 7 155H

25th

76 ^{+/- 1}

AMD Ryzen 9 3900XT 12-Core

25th

76 ^{+/- 1}

AMD Ryzen Threadripper 3970X 32-Core

25th

76 ^{+/- 1}

Intel Xeon E-2336

23rd

AMD Ryzen 7 6800U

22nd

78 ^{+/- 1}

AMD Ryzen 7 PRO 5850U

21st

79 ^{+/- 1}

AmpereOne 192-Core

21st

79 ^{+/- 7}

Intel Core i7-1165G7

17th

81 ^{+/- 1}

AMD Ryzen 7 PRO 6850U

17th

Intel Xeon Platinum 8468

15th

AMD Ryzen AI 9 HX 370

15th

82 ^{+/- 11}

2 x Intel Xeon Platinum 8468

14th

83 ^{+/- 1}

AMD EPYC 7F32 8-Core

14th

AMD Ryzen Threadripper 3990X 64-Core

12th

84 ^{+/- 1}

Intel Core i7-1185G7

11th

86 ^{+/- 1}

2 x Intel Xeon Max 9480

11th

2 x Intel Xeon Platinum 8380

11th

86 ^{+/- 1}

2 x AMD EPYC 9754 128-Core

9th

Intel Core i7-1065G7

9th

2 x AMD EPYC 7303 16-Core

8th

94 ^{+/- 1}

AMD Ryzen 7 4800U

7th

103 ^{+/- 2}

ARMv8 Neoverse-N1 128-Core

6th

104 ^{+/- 2}

AMD Ryzen 5 4500U

6th

106

AMD Ryzen 5 5500U

5th

109

Intel Xeon E3-1280 v5

5th

123 ^{+/- 1}

Intel Core i7-8565U

4th

131

AMD EPYC 7551 32-Core

3rd

135 ^{+/- 5}

Intel Core i9-10980XE

3rd

135 ^{+/- 4}

Intel Core i7-5960X

3rd

137

Intel Xeon Silver 4216

1st

144

Based on OpenBenchmarking.org data, the selected test / test configuration (Z3 Theorem Prover 4.12.1 - SMT File: 2.smt2) has an average run-time of 4 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.1%.

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: 23 August 2024

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

x86_64

(Many Processors)

ARMv8 64-bit

aarch64

ARMv8 Neoverse-N1 128-Core, ARMv8 Neoverse-N1 160-Core, AmpereOne 192-Core, HiSilicon TSV110

9600X 2 Systems - 137 Benchmark Results	AMD Ryzen 5 9600X 6-Core - ASUS ROG STRIX X670E-E GAMING WIFI - AMD Device 14d8 Ubuntu 24.04 - 6.10.0-phx - GNOME Shell 46.0
7773X 2P 3 Systems - 120 Benchmark Results	2 x AMD EPYC 7773X 64-Core - AMD DAYTONA_X - AMD Starship Ubuntu 24.04 - 6.8.0-41-generic - GNOME Shell 46.0
new sep 4 Systems - 116 Benchmark Results	2 x AMD EPYC 7303 16-Core - AMD DAYTONA_X - AMD Starship Ubuntu 24.04 - 6.8.0-31-generic - GNOME Shell 46.0
z3-1.0.0-all 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-fdrop-ub-builtins 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3 0905 1 System - 2 Benchmark Results	HiSilicon TSV110 - Huawei TaiShan 200 - Huawei HiSilicon Ubuntu 22.04 - 5.15.0-119-generic - 1.3.255
z3 0905 1 System - 2 Benchmark Results	2 x Intel Xeon Gold 6248 - Dell PowerEdge R740xd 0WXD1Y - Intel Sky Lake-E DMI3 Registers Ubuntu 24.04 - 6.8.0-41-generic - GCC 13.2.0
z3-1.0.0-Xclang-no-enable-noundef-analysis 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-fdrop-deref-attr 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-fdrop-align-attr 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-fdrop-noalias-restrict-attr 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-fcheck-div-rem-overflow 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-mllvm-disable-object-based-analysis 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-mllvm-zero-uninit-loads 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255
z3-1.0.0-fdrop-inbounds-from-gep-mllvm-disable-oob-analysis 1 System - 2 Benchmark Results	ARMv8 Neoverse-N1 - Oracle TLA MB TRAY A1-2c - 1008GB Ubuntu 22.04 - 6.5.0-1026-oracle - 1.3.255

AMD EPYC 9684X 2P Genoa-X Benchmarks 12 Systems - 69 Benchmark Results	2 x AMD EPYC 9684X 96-Core - AMD Titanite_4G - AMD Device 14a4 Ubuntu 23.04 - 6.2.0-23-generic - GNOME Shell 44.0
Linux - Intel Meteor Lake vs. AMD Zen 4 Laptop Benchmarks 3 Systems - 413 Benchmark Results	AMD Ryzen 7 7840U - Framework Laptop 13 - AMD Device 14e8 Ubuntu 24.04 - 6.10.0-061000rc4daily20240621-generic - GNOME Shell 46.0
Intel Core Ultra 7 155H vs. AMD Ryzen 7 7840U Linux Benchmarks 2 Systems - 831 Benchmark Results	Intel Core Ultra 7 155H - MTL Coral_MTH - Intel Device 7e7f Ubuntu 23.10 - 6.7.0-060700rc5-generic - GNOME Shell 45.1
AMD Ryzen 7 7840U Linux Laptops 3 Systems - 273 Benchmark Results	AMD Ryzen 7 PRO 6850U - LENOVO 21CM0001US - AMD 17h-19h PCIe Root Complex Ubuntu 23.04 - 6.2.0-23-generic - GNOME Shell 44.0
7950x3d may 2 Systems - 35 Benchmark Results	AMD Ryzen 9 7950X3D 16-Core - ASRock X670E PG Lightning - AMD Device 14d8 Ubuntu 22.10 - 5.19.0-23-generic - GNOME Shell 43.0
AMD Ryzen 5000 Series Linux Performance Featured Processor Comparison	AMD Ryzen 7 5800X3D 8-Core - ASUS ROG CROSSHAIR VIII HERO - AMD Starship Ubuntu 22.04 - 5.19.0-46-generic - GNOME Shell 42.5
dddas 2 Systems - 234 Benchmark Results	AMD Ryzen Threadripper 3970X 32-Core - ASUS ROG ZENITH II EXTREME - AMD Starship Ubuntu 22.04 - 5.19.0-051900rc7-generic - GNOME Shell 42.2
AMD Ryzen 5000 Series Linux Performance 8 Systems - 271 Benchmark Results	AMD Ryzen 5 5600X 6-Core - ASUS ROG CROSSHAIR VIII HERO - AMD Starship Ubuntu 22.04 - 5.19.0-46-generic - GNOME Shell 42.5
dddxxx Featured Compiler Comparison	Intel Core i7-8565U - Dell 0KTW76 - Intel Cannon Point-LP Ubuntu 22.04 - 5.19.0-rc6-phx-retbleed - GNOME Shell 42.2
ssa 3 Systems - 22 Benchmark Results	AMD Ryzen 5 5500U - NB01 NL5xNU - AMD Renoir Tuxedo 22.04 - 6.0.0-1010-oem - KDE Plasma 5.26.5
new new 2 Systems - 191 Benchmark Results	AMD Ryzen Z1 Extreme - ASUS RC71L v1.0 - AMD Device 14e8 Ubuntu 23.04 - 6.4.0-060400rc6-generic - GNOME Shell 44.2
AMD Ryzen 5000 Series Linux Performance 10 Systems - 272 Benchmark Results	AMD Ryzen 9 5950X 16-Core - ASUS ROG CROSSHAIR VIII HERO - AMD Starship Ubuntu 22.04 - 5.19.0-46-generic - GNOME Shell 42.5
sdmay 3 Systems - 49 Benchmark Results	AMD Ryzen 5 4500U - LENOVO LNVNB161216 - AMD Renoir Pop 22.04 - 5.17.5-76051705-generic - GNOME Shell 42.1
new may 3 Systems - 16 Benchmark Results	Intel Core i7-1185G7 - Dell 0DXP1F - Intel Tiger Lake-LP Ubuntu 22.04 - 5.19.0-40-generic - GNOME Shell 42.2
sssa 2 Systems - 191 Benchmark Results	AMD Ryzen 7 PRO 5850U - HP 8A78 - AMD Renoir Pop 22.04 - 6.2.6-76060206-generic - GNOME Shell 42.5

Z3 Theorem Prover

Project Site

Source Repository

Test Created

Last Updated

Test Maintainer

Test Type

Average Install Time

Average Run Time

Test Dependencies

Accolades

Supported Platforms

Supported Architectures

Revision History

Performance Metrics

Z3 Theorem Prover 4.12.1

SMT File: 2.smt2

Does It Scale Well With Increasing Cores?

Notable Instruction Set Usage

Tested CPU Architectures

Recent Test Results

Most Popular Test Results