From 48fd2bcfe85b508b14eb751ac4189e083ba1b173 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 18 Dec 2023 12:02:41 +0100 Subject: [PATCH] restore commment --- src/ast/euf/euf_egraph.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 0f5f220dc..dd6c9b9da 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -274,8 +274,7 @@ namespace euf { void pop(unsigned num_scopes); /** - * \brief Merge nodes, all effects are deferred to the propagation step. (TODO: is that comment outdated? at least in polysat::slicing it seems we almost never need to call propagate() separately.) - * The root of the merged class will be root(n2), unless there is a specific reason to prefer root(n1). + \brief merge nodes, all effects are deferred to the propagation step. */ void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); } void new_diseq(enode* n);