t3 test3t t3test: Processor: 2 x Intel Xeon E5-2697 v2 @ 3.50GHz (24 Cores / 48 Threads), Motherboard: Dell 0C4Y3R (2.9.0 BIOS), Chipset: Intel Xeon E7 v2/Xeon, Memory: 144GB, Disk: 1024GB JAJM600M1TB + 2 x 4000GB PERC H710P + 12001GB PERC H710P + 1000GB PERC H710P + 2000GB + 62GB Ultra + 4001GB Expansion Desk, Graphics: llvmpipe (324/405MHz), Audio: C-Media CMI8738/CMI8768, Monitor: C27F390, Network: 4 x Intel I350 + Mellanox MT27500 OS: openSUSE 20230828, Kernel: 6.5.0-6.gde97d09-default (x86_64), Desktop: KDE Plasma 5.27.7, Display Server: X Server 1.21.1.8, Display Driver: NVIDIA 535.104.05, OpenGL: 4.5 Mesa 23.1.6 (LLVM 16.0.6 256 bits), OpenCL: OpenCL 3.0 LINUX + OpenCL 1.2 Intel FPGA SDK for OpenCL 20.3 + OpenCL 3.0 CUDA 12.2.138, Compiler: PGI Compiler + Clang 16.0.6 + LLVM 16.0.6 + ICC 2021.10.0 20230609 + CUDA 12.2, File-System: xfs, Screen Resolution: 1680x1050 Z3 Theorem Prover 4.12.1 SMT File: 1.smt2 Seconds < Lower Is Better t3test . 40.33 |=============================================================== Z3 Theorem Prover 4.12.1 SMT File: 2.smt2 Seconds < Lower Is Better t3test . 151.62 |==============================================================