699   bool watchedByUnitClause(Literal Lit) const {  in watchedByUnitClause()
700     for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause;  in watchedByUnitClause()
709       assert(Clause.front() == Lit);  in watchedByUnitClause()
725   bool isCurrentlyFalse(Literal Lit) const {  in isCurrentlyFalse()
726     return static_cast<int8_t>(VarAssignments[var(Lit)]) ==  in isCurrentlyFalse()
727            static_cast<int8_t>(Lit & 1);  in isCurrentlyFalse()
731   bool isWatched(Literal Lit) const {  in isWatched()
732     return CNF.WatchedHead[Lit] != NullClause;  in isWatched()
745     for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {  in watchedLiterals()  local
746       if (CNF.WatchedHead[Lit] == NullClause)  in watchedLiterals()
748       WatchedLiterals.insert(Lit);  in watchedLiterals()
774     for (Literal Lit : watchedLiterals()) {  in unassignedVarsFormingWatchedLiteralsAreActive()  local
775       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()