Tool Artifact for ``On Synthesizing Presence Conditions in Numerical Software Product Lines''

In this work, we describe the installation, usage, and evaluation results of the tool, denoted \texttt{SPLSynthesize}, introduced by the paper ``On Synthesizing Presence Conditions in Numerical Software Product Lines''. We provide step-by-step instructions on how to download, run, and compare the tool's outputs to outputs described in the paper. The tool is a research prototype synthesizer designed for automatically synthesizing assertion-safe \texttt{\#ifdef}-guards in numerical Software Product Lines (SPLs). It uses a combination of forward and backward lifted static analyses of SPLs based on abstract interpretation to generate constraints that are subsequently solved by using the logical abduction technique.