Z3 Theorem Prover Benchmark - OpenBenchmarking.org

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.

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

Z3 Theorem Prover 4.12.1

SMT File: 2.smt2

OpenBenchmarking.org metrics for this test profile configuration based on 69 public results since 5 May 2023 with the latest data as of 20 May 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)

AMD Ryzen 9 7950X 16-Core

96th

AMD Ryzen 9 7950X3D 16-Core

90th

Intel Core i9-13900K

86th

Mid-Tier

75th

> 70

2 x AMD EPYC 7373X 16-Core

74th

Intel Core i7-1280P

69th

71 ^{+/- 3}

2 x AMD EPYC 9654 96-Core

63rd

AMD Ryzen 9 5900HX

63rd

2 x AMD EPYC 7773X 64-Core

51st

Median

50th

AMD Ryzen 7 6800U

45th

78 ^{+/- 1}

Intel Core i7-1165G7

41st

AMD Ryzen 7 PRO 6850U

37th

81 ^{+/- 1}

AMD Ryzen Threadripper 3990X 64-Core

34th

Intel Core i7-1185G7

27th

86 ^{+/- 1}

Low-Tier

25th

> 87

Intel Core i7-1065G7

25th

AMD Ryzen 7 4800U

18th

103 ^{+/- 2}

AMD Ryzen 5 4500U

11th

106

AMD Ryzen 5 5500U

9th

109

AMD EPYC 7551 32-Core

3rd

135 ^{+/- 5}

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.

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.

Z3_Theorem_Prover_1 1 System - 2 Benchmark Results	AMD Ryzen 9 5950X 16-Core - ASUS TUF GAMING X570-PLUS - AMD Starship Gentoo 2.13 - 6.3.1-gentoo-x86_64 - KDE Plasma 5.27.5
test 1 System - 2 Benchmark Results	AMD Ryzen 5 4500 6-Core - MSI MAG B550 TOMAHAWK - AMD Renoir Root Complex Linuxmint 20.3 - 5.15.0-71-generic - Cinnamon 5.2.7
new tests cfl new microcode 1 System - 27 Benchmark Results	Intel Core i7-8700K - ASUS TUF Z370-PLUS GAMING - Intel 8th Gen Core Ubuntu 22.04 - 6.2.0-060200rc5daily20230123-generic - GNOME Shell 42.5
may 3 Systems - 29 Benchmark Results	Intel Core i7-1165G7 - Dell 0GG9PT - Intel Tiger Lake-LP Ubuntu 23.04 - 6.2.0-20-generic - GNOME Shell 44.0
z3 milan x 5 Systems - 2 Benchmark Results	2 x AMD EPYC 7773X 64-Core - AMD DAYTONA_X - AMD Starship Ubuntu 22.04 - 5.15.0-47-generic - GNOME Shell 42.4
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
icy may 3 Systems - 37 Benchmark Results	Intel Core i7-1065G7 - Dell 06CDVY - Intel Ice Lake-LP DRAM Ubuntu 22.04 - 5.19.0-38-generic - GNOME Shell 42.2
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
6850u z3 3 Systems - 3 Benchmark Results	AMD Ryzen 7 PRO 6850U - LENOVO 21CM0001US - AMD Device 14b5 Pop 22.04 - 6.2.6-76060206-generic - GNOME Shell 42.5
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
may 3 Systems - 24 Benchmark Results	AMD Ryzen 7 4800U - ASRock 4X4-4000 - AMD Renoir 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
may 2 Systems - 17 Benchmark Results	AMD EPYC 7551 32-Core - GIGABYTE MZ31-AR0-00 v01010101 - AMD 17h Debian 11 - 5.10.0-9-amd64 - GCC 10.2.1 20210110
zz 4 Systems - 3 Benchmark Results	Intel Core i7-1280P - MSI MS-14C6 - Intel Alder Lake PCH Pop 22.04 - 6.2.6-76060206-generic - GNOME Shell 42.5
zz 3 Systems - 2 Benchmark Results	AMD Ryzen 7 6800U - System76 Pangolin - AMD Device 14b5 Pop 22.04 - 6.2.6-76060206-generic - GNOME Shell 42.5

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
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
icy may 3 Systems - 37 Benchmark Results	Intel Core i7-1065G7 - Dell 06CDVY - Intel Ice Lake-LP DRAM Ubuntu 22.04 - 5.19.0-38-generic - GNOME Shell 42.2
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
may 2 Systems - 17 Benchmark Results	AMD EPYC 7551 32-Core - GIGABYTE MZ31-AR0-00 v01010101 - AMD 17h Debian 11 - 5.10.0-9-amd64 - GCC 10.2.1 20210110
zz 3 Systems - 2 Benchmark Results	AMD Ryzen 7 6800U - System76 Pangolin - AMD Device 14b5 Pop 22.04 - 6.2.6-76060206-generic - GNOME Shell 42.5
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
may 3 Systems - 24 Benchmark Results	AMD Ryzen 7 4800U - ASRock 4X4-4000 - AMD Renoir Ubuntu 22.04 - 5.19.0-rc6-phx-retbleed - GNOME Shell 42.2
5900hx z3 Featured Graphics Comparison	AMD Ryzen 9 5900HX - ASUS G513QY v1.0 - AMD Renoir Ubuntu 22.10 - 5.19.0-41-generic - GNOME Shell 43.0
may 3 Systems - 29 Benchmark Results	Intel Core i7-1165G7 - Dell 0GG9PT - Intel Tiger Lake-LP Ubuntu 23.04 - 6.2.0-20-generic - GNOME Shell 44.0
z3 first run 4 Systems - 2 Benchmark Results	AMD Ryzen Threadripper 3990X 64-Core - Gigabyte TRX40 AORUS PRO WIFI - AMD Starship Ubuntu 23.04 - 6.2.0-20-generic - GNOME Shell 44.0
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
6850u z3 3 Systems - 3 Benchmark Results	AMD Ryzen 7 PRO 6850U - LENOVO 21CM0001US - AMD Device 14b5 Pop 22.04 - 6.2.6-76060206-generic - GNOME Shell 42.5
z3 zen 4 5 Systems - 2 Benchmark Results	AMD Ryzen 9 7950X 16-Core - ASUS ROG CROSSHAIR X670E HERO - AMD Device 14d8 Ubuntu 22.04 - 6.3.0-060300rc7daily20230417-generic - GNOME Shell 42.5
z3 raptor lake 4 Systems - 2 Benchmark Results	Intel Core i9-13900K - ASUS PRIME Z790-P WIFI - Intel Device 7a27 Fedora Linux 38 - 6.2.13-300.fc38.x86_64 - GNOME Shell 44.1

Z3 Theorem Prover

Project Site

Source Repository

Test Created

Test Maintainer

Test Type

Average Install Time

Average Run Time

Test Dependencies

Supported Platforms

Supported Architectures

Revision History

Performance Metrics

Z3 Theorem Prover 4.12.1

SMT File: 2.smt2

Tested CPU Architectures

Recent Test Results

Most Popular Test Results