mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
update format and checker for implied-eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f0184c3fde
commit
7135283135
|
@ -465,8 +465,6 @@ namespace euf {
|
|||
|
||||
void solver::display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
|
||||
expr_ref hint(proof_hint, m);
|
||||
if (!proof_hint)
|
||||
verbose_stream() << hint << "\n";
|
||||
if (!hint)
|
||||
hint = m.mk_const(m_smt, m.mk_proof_sort());
|
||||
visit_expr(out, hint);
|
||||
|
|
|
@ -240,9 +240,6 @@ namespace euf {
|
|||
m_literals[i] = lits[i];
|
||||
base_ptr += sizeof(literal) * n_lits;
|
||||
m_eqs = reinterpret_cast<enode_pair*>(base_ptr);
|
||||
if (!pma) {
|
||||
verbose_stream() << "null\n";
|
||||
}
|
||||
for (i = 0; i < n_eqs; ++i) {
|
||||
m_eqs[i] = eqs[i];
|
||||
if (m_eqs[i].first->get_id() > m_eqs[i].second->get_id())
|
||||
|
|
Loading…
Reference in a new issue