Testing the new NRA theory solver in Z3

This study conducts an empirical evaluation comparing Z3New (new Z3 solver version 4.14.1), an SMT solver for checking logical formulas, to Z3Old (old Z3 solver version 4.8.7), on Quantifier-Free Non-linear Real Arithmetic (QF_NRA) queries. This investigation aims to determine their relative performance, particularly the impact of the set-logic QF_NRA command, to obtain optimal solver selection for the Daisy verifier (a verification tool that utilizes such queries). A further aim is to identify potential bugs in solver through fuzz testing. Z3New was compared to Z3Old by running benchmarks from the Daisy verifier and the SMT-LIB library benchmark set. Fuzz testing with STORM, a blackbox mutational fuzzer, was also conducted to identify possible bugs and gather performance data. Performance was measured by run time for each solver. A key finding was a performance inversion that depended on the set-logic QF_NRA command. Z3New excelled on Daisy queries without this explicit command, with a median speedup of 1.62x relative to Z3Old. In contrast, Z3Old outperformed Z3New when the command was present, showing a 0.78x median speedup. This performance inversion also appeared for SMT-LIB QF_NRA benchmarks: with the set-logic QF_NRA command, Z3Old was faster, while without it, Z3New was faster. No bugs were found during fuzz testing; however, fuzz testing revealed that performance outliers shifted with different seed inputs, indicating high variability in Z3 solver performance for certain fuzz-generated inputs. In summary, the set-logic QF_NRA command critically impacts the relative performance of the Z3New and Z3Old solvers for QF_NRA queries. This evaluation suggests that Z3New can be the optimal version for Daisy. While benchmark performance showed clear trends, the variability observed during fuzz testing underscores the challenge of drawing universal performance conclusions for highly mutated inputs.