z3-1.0.0run

2 x Intel Xeon E5-2620 v2 testing with a ASUS Z9PE-D8 WS (5503 BIOS) and ASPEED on CentOS Stream 9 via the Phoronix Test Suite.

HTML result view exported from: https://openbenchmarking.org/result/2410244-NE-Z3100RUN697&sor&gru.

z3-1.0.0runProcessorMotherboardChipsetMemoryDiskGraphicsAudioNetworkMonitorOSKernelDisplay ServerDisplay DriverCompilerFile-SystemScreen ResolutiondebugNewGVNO2NewGVNO2-debug2 x Intel Xeon E5-2620 v2 @ 2.60GHz (12 Cores / 24 Threads)ASUS Z9PE-D8 WS (5503 BIOS)Intel Xeon E7 v2/Xeon32GB256GB Samsung SSD 850 + 2000GB Western Digital WD20EARX-00PASPEEDRealtek ALC8982 x Intel 82574LCentOS Stream 95.14.0-467.el9.x86_64 (x86_64)X ServerNVIDIAGCC 11.4.1 20231218 + PGI Compiler 16.10-0 + LLVM 3.1 + CUDA 11.2ext41024x768ASUS VW1905.14.0-514.el9.x86_64 (x86_64)GCC 11.5.0 20240719 + PGI Compiler 16.10-0 + LLVM 3.1 + CUDA 11.2OpenBenchmarking.orgKernel Details- Transparent Huge Pages: alwaysEnvironment Details- debug: CXXFLAGS=-O2 CFLAGS=-O2- NewGVNO2: CXXFLAGS="-O2 -mllvm -enable-newgvn" CFLAGS="-O2 -mllvm -enable-newgvn"- NewGVNO2-debug: CXXFLAGS="-O2 -mllvm -enable-newgvn" CFLAGS="-O2 -mllvm -enable-newgvn"Compiler Details- Optimized build with assertions; Built Apr 11 2013 (07:43:48); Default target: i386-pc-linux-gnu; Host CPU: i686Processor Details- Scaling Governor: intel_cpufreq conservative - CPU Microcode: 0x42ePython Details- debug: Python 3.9.19- NewGVNO2: Python 3.9.20- NewGVNO2-debug: Python 3.9.20Security Details- gather_data_sampling: Not affected + itlb_multihit: KVM: Mitigation of VMX disabled + l1tf: Mitigation of PTE Inversion; VMX: conditional cache flushes SMT vulnerable + mds: Mitigation of Clear buffers; SMT vulnerable + meltdown: Mitigation of PTI + mmio_stale_data: Unknown: No mitigations + reg_file_data_sampling: Not affected + retbleed: Not affected + spec_rstack_overflow: 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: conditional; RSB filling; PBRSB-eIBRS: Not affected; BHI: Not affected + srbds: Not affected + tsx_async_abort: Not affected

z3-1.0.0runz3: 2.smt2debugNewGVNO2NewGVNO2-debugOpenBenchmarking.org

Z3 Theorem Prover

Test Install Size

OpenBenchmarking.orgBytes, Fewer Is BetterZ3 Theorem Prover 4.12.1Test Install SizeNewGVNO2NewGVNO2-debug20K40K60K80K100K100572100572

Phoronix Test Suite v10.8.5