From 8d37495b7c83f749eec8a4c33b7c51b82c1b0e19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Jun 2021 22:22:41 -0700 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_etable.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h index f4e693e34..68ae95cd2 100644 --- a/src/ast/euf/euf_etable.h +++ b/src/ast/euf/euf_etable.h @@ -87,11 +87,8 @@ namespace euf { bool operator()(enode * n1, enode * n2) const { SASSERT(n1->num_args() == 2); SASSERT(n2->num_args() == 2); - if (n1->get_decl() != n2->get_decl()) return false; - - SASSERT(n1->get_decl() == n2->get_decl()); enode* c1_1 = get_root(n1, 0); enode* c1_2 = get_root(n1, 1); enode* c2_1 = get_root(n2, 0);