Alt-Ergo is an automatic theorem prover dedicated to program
verification. Alt-Ergo is based on CC(X) a congruence closure algorithm
parameterized by an equational theory X. Currently, CC(X) can be instantiated
by the empty equational theory and by the linear arithmetics. Alt-Ergo
contains also a home made SAT-solver and an instantiation mechanism. Its
architecture is summarized by the the following picture.