• ABORT : SAT::DPLLT
• BUDGET_EXCEEDED : SatSolver
• COMPUTE_TRANS_CLOSURE : CVCL::Expr
• CONSISTENT : SAT::DPLLT
• ENQUEUE : CVCL::TheoryDatatypeLazy
• FALSE : SAT::Var
• IMPLIED_LITERAL : CVCL::Expr
• INCONSISTENT : SAT::DPLLT
• IS_ATOMIC : CVCL::Expr
• IS_FINITE : CVCL::Expr
• IS_INT_ASSUMPTION : CVCL::Expr
• IS_JUSTIFIED : CVCL::Expr
• IS_SELECTED : CVCL::Expr
• IS_TRANSLATED : CVCL::Expr
• IS_USER_ASSUMPTION : CVCL::Expr
• IS_USER_REGISTERED_ATOM : CVCL::Expr
• MAYBE_CONSISTENT : SAT::DPLLT
• MERGE1 : CVCL::TheoryDatatypeLazy
• MERGE2 : CVCL::TheoryDatatypeLazy
• OUT_OF_MEMORY : SatSolver
• REWRITE_NORMAL : CVCL::Expr
• SATISFIABLE : SatSolver, SAT::DPLLT
• TRUE : SAT::Var
• UNKNOWN : SatSolver, SAT::Var
• UNSAT : SAT::DPLLT
• UNSATISFIABLE : SatSolver
• VALID_IS_ATOMIC : CVCL::Expr
• VALID_TYPE : CVCL::Expr
• WELL_FOUNDED : CVCL::Expr

---