diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index d25df5b069c..d21e7a12a48 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -1057,7 +1057,6 @@ namespace euf { SASSERT(true_lit != sat::null_literal); return (void*)(r->to_ptr(true_lit)); }; - r->m_egraph.copy_from(m_egraph, copy_justification); r->set_solver(s); r->m_egraph.copy_from(m_egraph, copy_justification); for (euf::enode* n : r->m_egraph.nodes()) {