This paper presents the raSAT SMT solver for polynomial constraints, which aims to handle them over both reals and integers with simple unified methodologies: (1) raSAT loop for inequalities, which extends the interval constraint propagation with testing to accelerate SAT detection, and (2) a non-constructive reasoning for equations over reals, based on the generalized intermediate value theorem.
展开▼
