40   const ivector_t* literals = &conflict->disjuncts.element_list;  in conflict_check()
81   int_mset_construct(&conflict->disjuncts, NULL_TERM);  in conflict_construct()
105   int_mset_destruct(&conflict->disjuncts);  in conflict_destruct()
374   if (int_mset_contains(&conflict->disjuncts, disjunct)) {  in conflict_add_disjunct()
431   assert(!int_mset_contains(&conflict->disjuncts, disjunct));  in conflict_add_disjunct()
432   int_mset_add(&conflict->disjuncts, disjunct);  in conflict_add_disjunct()
453   assert(int_mset_contains(&conflict->disjuncts, disjunct));  in conflict_remove_disjunct()
468   int_mset_remove_all(&conflict->disjuncts, disjunct);  in conflict_remove_disjunct()
500   ivector_t* disjuncts = int_mset_get_list(&conflict->disjuncts);  in conflict_recompute_level_info()  local
501   for (i = 0; i < disjuncts->size; ++ i) {  in conflict_recompute_level_info()
502     conflict_add_disjunct(&new_conflict, disjuncts->data[i]);  in conflict_recompute_level_info()
533   ivector_t disjuncts;  in conflict_resolve_propagation()  local
535   init_ivector(&disjuncts, 0);  in conflict_resolve_propagation()
553     ivector_push(&disjuncts, current_element->D);  in conflict_resolve_propagation()
564   for (i = 0; i < disjuncts.size; ++ i) {  in conflict_resolve_propagation()
565     term_t disjunct = disjuncts.data[i];  in conflict_resolve_propagation()
575     disjuncts.data[i] = conflict_disjunct_substitute(conflict, disjunct, var, substitution);  in conflict_resolve_propagation()
578       trace_term_ln(conflict->tracer, conflict->terms, disjuncts.data[i]);  in conflict_resolve_propagation()
586   for (i = 0; i < disjuncts.size; ++ i) {  in conflict_resolve_propagation()
587     conflict_add_disjunct(conflict, disjuncts.data[i]);  in conflict_resolve_propagation()
596   delete_ivector(&disjuncts);  in conflict_resolve_propagation()
666   return int_mset_get_list(&conflict->disjuncts);  in conflict_get_literals()