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

4 Minutes, 15 Seconds

Average Run Time

3 Minutes, 40 Seconds

Test Dependencies

C/C++ Compiler Toolchain + Python + CMake

Accolades

10k+ Downloads

Supported Platforms

Supported Architectures

x86_64 + aarch64
Public Result Uploads *Reported Installs **Reported Test Completions **Test Profile Page ViewsOpenBenchmarking.orgEventsZ3 Theorem Prover Popularity Statisticspts/z32023.052023.062023.072023.082023.092023.102023.112023.122024.012024.022024.032024.042024.052024.062024.072024.082024.092024.102024.112024.1210002000300040005000
* 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 23 December 2024.
2.smt250.2%1.smt249.8%SMT File Option PopularityOpenBenchmarking.org

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 831 public results since 5 May 2023 with the latest data as of 19 December 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 9800X3D 8-Core
98th
7
34
AMD Ryzen 7 9700X 8-Core
97th
10
35
AMD Ryzen 9 9950X 16-Core
95th
10
36 +/- 1
AMD Ryzen 9 9900X 12-Core
94th
7
36 +/- 1
AMD Ryzen 5 9600X 6-Core
94th
14
37 +/- 1
AMD Ryzen 7 7700X 8-Core
87th
12
45 +/- 1
AMD Ryzen 9 7950X 16-Core
87th
14
46 +/- 1
AMD Ryzen 9 7900X 12-Core
84th
16
47 +/- 1
AMD Ryzen 7 7700 8-Core
84th
12
47 +/- 1
AMD Ryzen 9 7900 12-Core
84th
9
47 +/- 2
AMD Ryzen 7 7800X3D 8-Core
84th
11
47 +/- 1
AMD EPYC 4484PX 12-Core
82nd
4
47
AMD EPYC 4584PX 16-Core
79th
4
48
AMD EPYC 4344P 8-Core
78th
3
48
AMD Ryzen 5 7600 6-Core
78th
6
48 +/- 1
AMD Ryzen 9 7950X3D 16-Core
77th
17
48 +/- 4
AMD Ryzen 5 7600X 6-Core
77th
12
48 +/- 2
Intel Core Ultra 9 285K
77th
8
48 +/- 1
AMD EPYC 4364P 8-Core
77th
4
49
AMD Ryzen 9 7900X3D 12-Core
77th
13
49 +/- 4
AMD Ryzen Threadripper PRO 7995WX 96-Cores
76th
3
49 +/- 1
Mid-Tier
75th
> 49
AMD EPYC 4564P 16-Core
74th
5
49
AMD EPYC 4244P 6-Core
72nd
3
49
AMD Ryzen Threadripper 7980X 64-Cores
72nd
4
49 +/- 1
Intel Core i9-14900K
70th
11
50
AMD EPYC 4464P 12-Core
68th
3
50
Intel Core i9-13900K
66th
7
52 +/- 2
AMD Ryzen 7 8700G
66th
7
53 +/- 2
Intel Core Ultra 5 245K
64th
5
54 +/- 1
AMD Ryzen 5 8600G
62nd
9
54 +/- 2
AMD Ryzen 5 8400F 6-Core
61st
4
55
AMD EPYC 4124P 4-Core
57th
4
57
AMD Ryzen 7 5800X3D 8-Core
56th
13
58 +/- 2
Intel Core i5-14600K
56th
7
58 +/- 1
AMD Ryzen 7 5800X 8-Core
54th
8
59
AMD Ryzen 9 5950X 16-Core
54th
13
59 +/- 1
Intel Core i5-13600K
52nd
3
60
AMD Ryzen 5 5600X 6-Core
51st
5
61 +/- 1
AMD Ryzen 9 5900X 12-Core
51st
7
61 +/- 1
ARMv8 Neoverse-N1 160-Core
51st
62
61 +/- 8
AMD Ryzen 7 7840HS
51st
8
61 +/- 2
Median
50th
61
Intel Core i5-14500
48th
7
62
Intel Core Ultra 7 256V
48th
4
62
Intel Xeon E E-2488
46th
5
63 +/- 1
AMD Ryzen 7 8845HS
45th
5
64 +/- 2
Intel Core i5-12600K
44th
7
65 +/- 2
AMD Ryzen Z1 Extreme
44th
14
65 +/- 1
AMD Ryzen 7 7840U
44th
16
65 +/- 5
2 x Intel Xeon E5-2620 v2
43rd
3
66
AMD Ryzen 7 3800XT 8-Core
43rd
4
67 +/- 1
Intel Core i5-14400F
43rd
5
67
Intel Core i5-13400
41st
3
68
AMD Ryzen 7 PRO 7840U
41st
7
68
2 x AMD EPYC 9684X 96-Core
41st
6
68
2 x AMD EPYC 9554 64-Core
39th
6
69 +/- 1
Intel Core i3-14100
39th
8
69 +/- 1
2 x AMD EPYC 7373X 16-Core
37th
4
70
2 x AMD EPYC 9654 96-Core
36th
11
71 +/- 1
Intel Xeon E-2388G
34th
10
72 +/- 1
Intel Xeon Platinum 8462Y
30th
4
73 +/- 1
AMD Ryzen 9 5900HX
30th
4
73 +/- 3
Intel Xeon Gold 6444Y
27th
3
75 +/- 1
2 x Intel Xeon Gold 6442Y
27th
3
75
2 x AMD EPYC 7773X 64-Core
27th
10
75 +/- 1
AMD Ryzen 5 5500
27th
6
75 +/- 2
Low-Tier
25th
> 76
AMD Ryzen AI 9 365
25th
3
76
AMD Ryzen 9 3900XT 12-Core
25th
4
76 +/- 1
Intel Core Ultra 7 155H
25th
10
76 +/- 1
AMD Ryzen Threadripper 3970X 32-Core
25th
8
76 +/- 1
AMD Ryzen AI 9 HX 370
25th
6
76 +/- 9
Intel Xeon E-2336
23rd
5
77
AMD Ryzen 7 6800U
22nd
3
78 +/- 1
AMD Ryzen 7 PRO 5850U
20th
8
79 +/- 1
AmpereOne 192-Core
20th
5
79 +/- 7
Intel Core i7-1165G7
17th
10
81 +/- 1
AMD Ryzen 7 PRO 6850U
17th
11
81
Intel Xeon Platinum 8468
15th
6
82
AMD EPYC 7F32 8-Core
14th
3
83
2 x Intel Xeon Platinum 8468
14th
3
83 +/- 1
AMD Ryzen Threadripper 3990X 64-Core
13th
8
84 +/- 1
Intel Core i7-1185G7
11th
9
85 +/- 1
2 x Intel Xeon Platinum 8380
10th
8
86 +/- 1
2 x Intel Xeon Max 9480
10th
3
86
2 x AMD EPYC 9754 128-Core
9th
5
87
Intel Core i7-1065G7
9th
4
91
2 x AMD EPYC 7303 16-Core
8th
4
94 +/- 1
AMD Ryzen 7 4800U
7th
3
103 +/- 2
ARMv8 Neoverse-N1 128-Core
7th
4
104 +/- 2
AMD Ryzen 5 4500U
6th
3
106
AMD Ryzen 5 5500U
6th
3
109
Intel Xeon E3-1280 v5
5th
5
123 +/- 1
Intel Core i7-8565U
4th
5
131
AMD EPYC 7551 32-Core
4th
4
135 +/- 5
Intel Core i9-10980XE
4th
9
135 +/- 4
Intel Core i7-5960X
3rd
3
137
Intel Xeon Silver 4216
2nd
3
144
ARMv8 Cortex-A72 4-Core
1st
5
808 +/- 1
Detailed Performance Overview
OpenBenchmarking.orgDistribution Of Public Results - SMT File: 2.smt2827 Results Range From 32 To 809 Seconds32608811614417220022825628431234036839642445248050853656459262064867670473276078881690180270360450

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.

OpenBenchmarking.orgMinutesTime Required To Complete BenchmarkSMT File: 2.smt2Run-Time3691215Min: 2 / Avg: 3.27 / Max: 12

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

OpenBenchmarking.orgPercent, Fewer Is BetterAverage Deviation Between RunsSMT File: 2.smt2Deviation246810Min: 0 / Avg: 0.14 / Max: 2

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.

IntelAMDOpenBenchmarking.orgRelative Core Scaling To BaseZ3 Theorem Prover CPU Core ScalingSMT File: 2.smt24681012141624320.44580.89161.33741.78322.229

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)
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 Bulldozer (2011).
 
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 Cortex-A72 4-Core, ARMv8 Neoverse-N1 128-Core, ARMv8 Neoverse-N1 160-Core, AmpereOne 192-Core, HiSilicon TSV110

Recent Test Results

OpenBenchmarking.org Results Compare

1 System - 109 Benchmark Results

Intel Core Ultra 9 285K - ASUS ROG MAXIMUS Z890 HERO - 2 x 16384MB 6400MHz Micron CP16G64C38U5B.M8D1

Microsoft Windows 11 Pro Build 26100 - 10.0.26100.2605 - 32.0.101.6325

1 System - 628 Benchmark Results

ARMv8 Cortex-A72 - Raspberry Pi 400 Rev 1.0 - Broadcom BCM2711

Debian 12 - 6.6.63-v8+ - X Server 1.21.1.7

4 Systems - 3 Benchmark Results

2 x Intel Xeon E5-2620 v2 - ASUS Z9PE-D8 WS - Intel Xeon E7 v2

CentOS Stream 9 - 5.14.0-467.el9.x86_64 - X Server

1 System - 2 Benchmark Results

AMD Ryzen 7 9800X3D 8-Core - ASRock X870E Taichi - AMD Device 14d8

Ubuntu 24.04 - 6.12.0-rc7-phx-eraps - GNOME Shell 46.0

3 Systems - 3 Benchmark Results

2 x Intel Xeon E5-2620 v2 - ASUS Z9PE-D8 WS - Intel Xeon E7 v2

CentOS Stream 9 - 5.14.0-467.el9.x86_64 - X Server

2 Systems - 3 Benchmark Results

2 x Intel Xeon E5-2620 v2 - ASUS Z9PE-D8 WS - Intel Xeon E7 v2

CentOS Stream 9 - 5.14.0-514.el9.x86_64 - X Server

2 Systems - 3 Benchmark Results

2 x Intel Xeon E5-2620 v2 - ASUS Z9PE-D8 WS - Intel Xeon E7 v2

CentOS Stream 9 - 5.14.0-467.el9.x86_64 - X Server

3 Systems - 289 Benchmark Results

1 System - 64 Benchmark Results

Intel Core Ultra 7 256V - ASUS UX5406SA - 8 x 2048MB 8533MHz Samsung

Microsoft Windows 11 Home Build 26100 - 10.0.26100.1742 - 32.0.101.5730

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

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

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

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

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

Most Popular Test Results

OpenBenchmarking.org Results Compare

1 System - 64 Benchmark Results

Intel Core Ultra 7 256V - ASUS UX5406SA - 8 x 2048MB 8533MHz Samsung

Microsoft Windows 11 Home Build 26100 - 10.0.26100.1742 - 32.0.101.5730

12 Systems - 69 Benchmark Results

2 x AMD EPYC 9654 96-Core - AMD Titanite_4G - AMD Device 14a4

Ubuntu 23.04 - 6.2.0-23-generic - GNOME Shell 44.0

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

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

18 Systems - 442 Benchmark Results

AMD Ryzen 5 7600 6-Core - ASUS ROG STRIX X670E-E GAMING WIFI - AMD Device 14d8

Ubuntu 24.04 - 6.10.0-061000rc2-generic - GNOME Shell 46.0

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

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

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

8 Systems - 271 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

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

7 Systems - 223 Benchmark Results

AMD Ryzen 7 7840U - Framework FRANMDCP07 - AMD Device 14e8

Ubuntu 23.10 - 6.5.0-5-generic - GNOME Shell 45.0

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

3 Systems - 369 Benchmark Results

Intel Xeon E-2388G - ASRockRack E3C252D4U - Intel Tiger Lake-H

Ubuntu 22.04 - 6.2.0-26-generic - GNOME Shell 42.9
Find More Test Results