ALWAYS_FAIL = FALSE;
CLH_SPINLOCK = FALSE;
COUNT_ASYNC_CHECKS = FALSE;
ENTER_METHODS = TRUE;
EXIT_METHODS = TRUE;
PREDICTION_IGNORED = FALSE;
SIMULATE_NO_QUEUE = FALSE;
SINGLE_THREADED_MODE = FALSE;
VERBOSE_LOGGING = FALSE;

HELPER_COUNT = 3;
HEURISTIC_DELETE_THRESHOLD = 32;
HEURISTIC_SCORE_DIVISOR = 1;
HEURISTIC_SCORE_MINIMUM = 0;
HEURISTIC_WARMUP_THRESHOLD = 0;
HYBRID_DISABLE_THRESHOLD = 32;
HYBRID_ENABLE_THRESHOLD = 32;
INSTRUCTION_LIMIT = 1000;
NESTED_FORK_MINIMUM_LENGTH = 0;
NESTED_FORK_MINIMUM_PERIOD = 0;
NESTING_DEPTH = 1;
NESTING_HEIGHT = 1;
STACK_COPYING_DEPTH = 1;