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.

HTML result view exported from: https://openbenchmarking.org/result/2305208-NE-Z3THEOREM75.

Z3_Theorem_Prover_1ProcessorMotherboardChipsetMemoryDiskGraphicsAudioNetworkOSKernelDesktopDisplay ServerDisplay DriverOpenGLCompilerFile-SystemScreen ResolutionZ3_Theorem_Prover_Gentoo2.13_Ryzen_5950XAMD 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.7ext41024x768OpenBenchmarking.org- 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_1z3: 1.smt2z3: 2.smt2Z3_Theorem_Prover_Gentoo2.13_Ryzen_5950X22.59060.611OpenBenchmarking.org

Z3 Theorem Prover

SMT File: 1.smt2

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

Z3 Theorem Prover

SMT File: 2.smt2

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

Phoronix Test Suite v10.8.4