307   if (l1 == true_literal) return l2;  in eval_and()
308   if (l2 == true_literal) return l1;  in eval_and()
319   if (l1 == true_literal) return true_literal;  in eval_or()
320   if (l2 == true_literal) return true_literal;  in eval_or()
322   if (l1 == not(l2)) return true_literal;  in eval_or()
329   if (l1 == true_literal) return not(l2);  in eval_xor()
330   if (l2 == true_literal) return not(l1);  in eval_xor()
332   if (l1 == not(l2)) return true_literal;  in eval_xor()
353   if (aux1 == true_literal) return aux2;  in eval_ite()
354   if (aux2 == true_literal) return aux1;  in eval_ite()
385   check_and_aux(m, false_literal, true_literal);  in check_and()
386   check_and_aux(m, true_literal, false_literal);  in check_and()
387   check_and_aux(m, true_literal, true_literal);  in check_and()
405   check_or_aux(m, false_literal, true_literal);  in check_or()
406   check_or_aux(m, true_literal, false_literal);  in check_or()
407   check_or_aux(m, true_literal, true_literal);  in check_or()
426   check_implies_aux(m, false_literal, true_literal);  in check_implies()
427   check_implies_aux(m, true_literal, false_literal);  in check_implies()
428   check_implies_aux(m, true_literal, true_literal);  in check_implies()
446   check_xor_aux(m, false_literal, true_literal);  in check_xor()
447   check_xor_aux(m, true_literal, false_literal);  in check_xor()
448   check_xor_aux(m, true_literal, true_literal);  in check_xor()
466   check_iff_aux(m, false_literal, true_literal);  in check_iff()
467   check_iff_aux(m, true_literal, false_literal);  in check_iff()
468   check_iff_aux(m, true_literal, true_literal);  in check_iff()
488   check_ite_aux(m, false_literal, false_literal, true_literal);  in check_ite()
489   check_ite_aux(m, false_literal, true_literal, false_literal);  in check_ite()
490   check_ite_aux(m, false_literal, true_literal, true_literal);  in check_ite()
491   check_ite_aux(m, true_literal, false_literal, false_literal);  in check_ite()
492   check_ite_aux(m, true_literal, false_literal, true_literal);  in check_ite()
493   check_ite_aux(m, true_literal, true_literal, false_literal);  in check_ite()
494   check_ite_aux(m, true_literal, true_literal, true_literal);  in check_ite()
639   a[0] = true_literal;  in test3()
943   l1 = true_literal;  in check_iff_assertion4()
964   l1 = true_literal;  in check_iff_assertion5()
965   l2 = true_literal;  in check_iff_assertion5()