- _ -

• __SAT_STATUS__ : xchaff_solver.h
• __SGI_STL_INTERNAL_RELOPS : minisat_global.h
• _cvc3__assumptions_h_ : assumptions.h
• _cvc3__include__clause_h_ : clause.h
• _CVC3_TRUSTED_ : quant_theorem_producer.cpp , datatype_theorem_producer.cpp , core_theorem_producer.cpp , bitvector_theorem_producer.cpp , array_theorem_producer.cpp , arith_theorem_producer_old.cpp , arith_theorem_producer3.cpp , arith_theorem_producer.cpp , theorem_producer.cpp , common_theorem_producer.cpp , search_theorem_producer.cpp , Object.h , dpllt_minisat.cpp , cnf_theorem_producer.cpp , uf_theorem_producer.cpp , simulate_theorem_producer.cpp , records_theorem_producer.cpp

- c -

• CHECK : xchaff_utils.h
• CHECK_FULL : xchaff_utils.h
• CHECK_PROOFS : theorem_producer.h
• CHECK_SOUND : theorem_producer.h
• CLASS_NAME : records_theorem_producer.cpp , quant_theorem_producer.cpp , uf_theorem_producer.cpp , arith_theorem_producer_old.cpp , array_theorem_producer.cpp , arith_theorem_producer.cpp , arith_theorem_producer3.cpp
• CVC_DLL : type.h , os.h

- d -

• DBG_PRINT : debug.h
• DBG_PRINT_MSG : debug.h
• DebugAssert : debug.h , hash_table.h

- f -

• FatalAssert : debug.h
• FLIPPED : xchaff_base.h
• followChaff : search_fast.cpp

- h -

• HASH_VALUE_ONE : theory_bitvector.cpp
• HASH_VALUE_ZERO : theory_bitvector.cpp

- i -

• IF_DEBUG : debug.h

- n -

• NULL_CLAUSE : xchaff_base.h

- p -

• PRIME : expr_value.h

- r -

• REG : expr_manager.cpp
• REG_TYPE : expr_manager.cpp

- s -

• STARTUP_LIT_POOL_SIZE : xchaff_dbase.h

- t -

• TEMPLATE_FAIL : minisat_global.h
• TRACE : debug.h
• TRACE_MSG : debug.h

- v -

• vals3 : circuit.cpp
• vals4 : circuit.cpp
• VERSION : main.cpp