Don't care in SMT—Building flexible yet efficient abstraction/refinement solvers - Bauer, A; Leucker, M; Schallhart, C; Tautschnig, M (Poitiers‚ France, 2007)