The algorithm is designed to provide the exact result for all inputs but to perform only few symbolic operations for the sake of efficiency. In particular, the roots of f(\alpha,y) at a critical x-coordinate \alpha are found with adaptive-precision arithmetic in all cases, using a variant of the Bitstream Descartes method~(Eigenwillig et al., 2005). The algorithm may choose a generic coordinate system for parts of the analysis but provides its result in the original system.
The algorithm is implemented as C++ library AlciX in the EXACUS project. Running time comparisons with top by Gonzalez-Vega and Necula (2002), and with cad2d by Brown demonstrate its efficiency.