Artifact for "Ultimate Eliminator: a Tool for Partial Quantifier Elimination and Formula Simplification"

Artifact for the Paper: "Ultimate Eliminator: a Tool for Partial Quantifier Elimination and Formula Simplification" Designed for the TACAS 2027 VM https://zenodo.org/records/23472158 with 4 CPUs and 12 GB. Does not work with ARM! Licensed under the MIT License, all included licenses permit the evaluation of the artifact. The paper compares the quantifier elimination of UltimateEliminator with z3's tactics qe, qe2 and qe_rec on 21,387 SMT-LIB benchmarks with quantifiers (logics ABV, ALIA, ANIA, BV, LIA, LRA, NIA, NRA). After the elimination, MathSAT or z3 decides the quantifier-free result. The artifact contains: - UltimateEliminator 0.3.0-dev-305869c-m, z3 5.1.0 and MathSAT 5.6.11 (binaries with licenses) - the 21,387 benchmarks, the BenchExec benchmark definitions and the tool pipelines of all 9 configurations - the raw BenchExec results of the evaluation (192,483 runs) and scripts that recompute every number, table and figure of the paper from them - scripts for a 10-task test run and for rerunning the full evaluation - an offline installation of all dependencies (BenchExec 3.33, matplotlib) for the TACAS 2027 AE VM (Ubuntu 26.04) and Ubuntu 24.04