Table of Contents

Introduction and basic concepts.
Decision procedures for propositional logic.
Equality logic and uninterpreted functions.
Decision procedures for equality logic and uninterpreted functions.
Linear arithmetic.
Bit vectors.
Arrays.
Pointer logic.
Quantified formulas.
Deciding a combination of theories.
Propositional encodings.