114 …   tout << " was asserted\nliteral: "; m_ctx.display_literal(tout, js.get_literal()); tout << "\n";  in eq_justification2literals()
125             m_antecedents->push_back(js.get_literal());  in eq_justification2literals()
302             r = std::max(r, m_ctx.get_assign_level(js.get_literal()));  in get_max_lvl()
548 … TRACE("conflict_smt2", m_ctx.display_literals_smt2(tout, consequent, ~js.get_literal()) << "\n";);  in resolve()
549                 SASSERT(consequent.var() != js.get_literal().var());  in resolve()
550                 process_antecedent(js.get_literal(), num_marks);  in resolve()
709                 if (!process_antecedent_for_minimization(js.get_literal())) {  in implied_by_marked()
849 …TRACE("proof_gen_bug", tout << js.get_literal() << "\n"; m_ctx.display_literal_info(tout, js.get_l…  in get_proof()
850             return norm_eq_proof(n1, n2, get_proof(js.get_literal()));  in get_proof()
985                 SASSERT(l == false_literal || l == cls->get_literal(0) || l == cls->get_literal(1));  in get_proof()
987                     if (cls->get_literal(0) == l) {  in get_proof()
991                         SASSERT(l == cls->get_literal(1));  in get_proof()
992                         proof * pr = get_proof(~cls->get_literal(0));  in get_proof()
1000                     proof * pr = get_proof(~cls->get_literal(i));  in get_proof()
1012                           tout << cls->get_literal(i).index() << "\n";  in get_proof()
1014                           m_ctx.literal2expr(cls->get_literal(i), l_expr);  in get_proof()
1026                            tout << cls->get_literal(i).index() << "\n";  in get_proof()
1028                            m_ctx.literal2expr(cls->get_literal(i), l_expr);  in get_proof()
1098                 if (cls->get_literal(0) == l) {  in visit_b_justification()
1102                     SASSERT(cls->get_literal(1) == l);  in visit_b_justification()
1103                     if (get_proof(~cls->get_literal(0)) == nullptr)  in visit_b_justification()
1109                 SASSERT(cls->get_literal(i) != l);  in visit_b_justification()
1110                 if (get_proof(~cls->get_literal(i)) == nullptr)  in visit_b_justification()
1147                 if (get_proof(js.get_literal()) == nullptr)  in visit_trans_proof()
1418                     SASSERT(cls->get_literal(0) == consequent || cls->get_literal(1) == consequent);  in mk_unsat_core()
1419                     if (cls->get_literal(0) == consequent) {  in mk_unsat_core()
1423                         process_antecedent_for_unsat_core(~cls->get_literal(0));  in mk_unsat_core()
1428                     literal l = cls->get_literal(i);  in mk_unsat_core()
1438                 SASSERT(consequent.var() != js.get_literal().var());  in mk_unsat_core()
1439                 process_antecedent_for_unsat_core(js.get_literal());  in mk_unsat_core()