NOTE: we are providing the source code under the MIT license (at github.com/SRI-CSL/ICS) It hasn't been built in several years; please let us know if you have any updates, so others can benefit.
ICS (Integrated Canonizer and Solver) is an efficient decision procedure for a fragment of first-order logic. Terms are built from uninterpreted function symbols and operators from a rich combination of datatypes including arithmetic, functional arrays, tuples, cotuples, and fixed-sized bitvectors. It incorporates a state-of-the-art SAT solver.
ICS can be used as a standalone application that reads formulas interactively, and may also be included as a library in any application that requires embedded deduction.
ICS is one of the SRI FormalWare tools.