Z3_Theorem_Prover_1

AMD Ryzen 9 5950X 16-Core testing with a ASUS TUF GAMING X570-PLUS (WI-FI) (4403 BIOS) and eVGA NVIDIA GeForce GTX 1050 2GB on Gentoo 2.13 via the Phoronix Test Suite.

Compare your own system(s) to this result file with the Phoronix Test Suite by running the command: phoronix-test-suite benchmark 2305208-NE-Z3THEOREM75
Jump To Table - Results

Statistics

Remove Outliers Before Calculating Averages

Graph Settings

Prefer Vertical Bar Graphs

Multi-Way Comparison

Condense Multi-Option Tests Into Single Result Graphs

Table

Show Detailed System Result Table

Run Management

Result
Identifier
View Logs
Performance Per
Dollar
Date
Run
  Test
  Duration
Z3_Theorem_Prover_Gentoo2.13_Ryzen_5950X
May 20 2023
  5 Minutes
Only show results matching title/arguments (delimit multiple options with a comma):
Do not show results matching title/arguments (delimit multiple options with a comma):


Z3_Theorem_Prover_1OpenBenchmarking.orgPhoronix Test SuiteAMD Ryzen 9 5950X 16-Core @ 3.40GHz (16 Cores / 32 Threads)ASUS TUF GAMING X570-PLUS (WI-FI) (4403 BIOS)AMD Starship/Matisse2 x 32 GB DDR4-3600MT/s Kingston KF3600C18D41000GB Samsung SSD 990 PRO 1TB + 1000GB Western Digital WDS100T2B0B + 2000GB EZRZ-00Z5HB0 + 8002GB Elements 25A3eVGA NVIDIA GeForce GTX 1050 2GBCreative CA0110-IBGRealtek RTL8111/8168/8411 + Intel-AC 9260Gentoo 2.136.3.1-gentoo-x86_64 (x86_64)KDE Plasma 5.27.5X Server 1.21.1.8NVIDIA 525.116.034.6.0GCC 12.2.1 20230428 + Clang 15.0.7 + LLVM 15.0.7ext41024x768ProcessorMotherboardChipsetMemoryDiskGraphicsAudioNetworkOSKernelDesktopDisplay ServerDisplay DriverOpenGLCompilerFile-SystemScreen ResolutionZ3_Theorem_Prover_1 BenchmarksSystem Logs- Transparent Huge Pages: madvise- --bindir=/usr/x86_64-pc-linux-gnu/gcc-bin/12 --build=x86_64-pc-linux-gnu --datadir=/usr/share/gcc-data/x86_64-pc-linux-gnu/12 --disable-cet --disable-esp --disable-fixed-point --disable-libada --disable-libssp --disable-libstdcxx-pch --disable-libunwind-exceptions --disable-libvtv --disable-systemtap --disable-valgrind-annotations --disable-vtable-verify --disable-werror --enable-__cxa_atexit --enable-checking=release --enable-clocale=gnu --enable-default-pie --enable-default-ssp --enable-languages=c,c++,fortran --enable-libgomp --enable-libstdcxx-time --enable-lto --enable-multilib --enable-nls --enable-obsolete --enable-secureplt --enable-shared --enable-targets=all --enable-threads=posix --host=x86_64-pc-linux-gnu --includedir=/usr/lib/gcc/x86_64-pc-linux-gnu/12/include --mandir=/usr/share/gcc-data/x86_64-pc-linux-gnu/12/man --with-gcc-major-version-only --with-multilib-list=m32,m64 --with-python-dir=/share/gcc-data/x86_64-pc-linux-gnu/12/python --without-isl --without-zstd - Scaling Governor: acpi-cpufreq performance (Boost: Enabled) - CPU Microcode: 0xa201016- Python 3.11.3- itlb_multihit: Not affected + l1tf: Not affected + mds: Not affected + meltdown: Not affected + mmio_stale_data: Not affected + retbleed: Not affected + spec_store_bypass: Mitigation of SSB disabled via prctl + spectre_v1: Mitigation of usercopy/swapgs barriers and __user pointer sanitization + spectre_v2: Mitigation of Retpolines IBPB: conditional IBRS_FW STIBP: always-on RSB filling PBRSB-eIBRS: Not affected + srbds: Not affected + tsx_async_abort: Not affected

Z3 Theorem Prover

The Z3 Theorem Prover / SMT solver is developed by Microsoft Research under the MIT license. Learn more via the OpenBenchmarking.org test page.

OpenBenchmarking.orgSeconds, Fewer Is BetterZ3 Theorem Prover 4.12.1SMT File: 1.smt2Z3_Theorem_Prover_Gentoo2.13_Ryzen_5950X510152025SE +/- 0.18, N = 322.591. (CXX) g++ options: -lpthread -std=c++17 -fvisibility=hidden -mfpmath=sse -msse -msse2 -O3 -fPIC

OpenBenchmarking.orgSeconds, Fewer Is BetterZ3 Theorem Prover 4.12.1SMT File: 2.smt2Z3_Theorem_Prover_Gentoo2.13_Ryzen_5950X1428425670SE +/- 0.15, N = 360.611. (CXX) g++ options: -lpthread -std=c++17 -fvisibility=hidden -mfpmath=sse -msse -msse2 -O3 -fPIC