A randomized satisfiability procedure for arithmetic and uninterpreted function symbols
scientific article; zbMATH DE number 2193212