This paper presents a method for combining decision procedures for multiple theories into a single decision procedure for their combination. The method is based on a technique called equality propagation. The authors describe a simplifier that uses this method to find a normal form for expressions involving various functions and predicates, including arithmetic, arrays, lists, and uninterpreted functions. The simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier. The paper discusses two examples of theorems that arise in program manipulation. The first example involves proving that two consecutive loop executions "commute," while the second example involves verifying that a random integer generated from a random real number falls within a specified range. These theorems are not mathematically interesting but are used to verify routine facts or catch errors in program manipulation. The paper describes four quantifier-free theories: the theory of real numbers under + and ≤, the theory of arrays under store and select, the theory of list structure with car, cdr, cons, and atom, and the theory of equality with uninterpreted function symbols. The authors present a general method for combining decision procedures for two quantifier-free theories into a single decision procedure for their combination. This method is based on equality propagation, which allows the simplifier to detect and propagate equalities entailed by the conjunction being decided. The paper also discusses the correctness of the equality propagation procedure. It proves that the procedure is correct if it returns satisfiable, and that it always halts. The procedure is used to determine the satisfiability of a conjunction of literals. The algorithm uses variables F_S and F_T, which contain conjunctions of literals. The algorithm first assigns conjunctions to F_S and F_T, then checks if either is unsatisfiable. If not, it propagates equalities between variables. If necessary, it performs case splitting to handle nonconvex formulas. The paper also discusses the simplification of Boolean structure. The simplifier first replaces logical operators with if-then-else expressions, then recursively simplifies the resulting conditional expressions. The simplifier uses a symbolic evaluator to determine the simplest equivalent form of the expression. The simplifier is used in the Stanford Pascal Verifier to verify Pascal programs.This paper presents a method for combining decision procedures for multiple theories into a single decision procedure for their combination. The method is based on a technique called equality propagation. The authors describe a simplifier that uses this method to find a normal form for expressions involving various functions and predicates, including arithmetic, arrays, lists, and uninterpreted functions. The simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier. The paper discusses two examples of theorems that arise in program manipulation. The first example involves proving that two consecutive loop executions "commute," while the second example involves verifying that a random integer generated from a random real number falls within a specified range. These theorems are not mathematically interesting but are used to verify routine facts or catch errors in program manipulation. The paper describes four quantifier-free theories: the theory of real numbers under + and ≤, the theory of arrays under store and select, the theory of list structure with car, cdr, cons, and atom, and the theory of equality with uninterpreted function symbols. The authors present a general method for combining decision procedures for two quantifier-free theories into a single decision procedure for their combination. This method is based on equality propagation, which allows the simplifier to detect and propagate equalities entailed by the conjunction being decided. The paper also discusses the correctness of the equality propagation procedure. It proves that the procedure is correct if it returns satisfiable, and that it always halts. The procedure is used to determine the satisfiability of a conjunction of literals. The algorithm uses variables F_S and F_T, which contain conjunctions of literals. The algorithm first assigns conjunctions to F_S and F_T, then checks if either is unsatisfiable. If not, it propagates equalities between variables. If necessary, it performs case splitting to handle nonconvex formulas. The paper also discusses the simplification of Boolean structure. The simplifier first replaces logical operators with if-then-else expressions, then recursively simplifies the resulting conditional expressions. The simplifier uses a symbolic evaluator to determine the simplest equivalent form of the expression. The simplifier is used in the Stanford Pascal Verifier to verify Pascal programs.