From f7d1cce69a8dc1fc3a90bf325984a38329481b0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Jun 2021 22:12:52 -0700 Subject: [PATCH] #5336 Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_etable.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h index 6274af14266..f4e693e3433 100644 --- a/src/ast/euf/euf_etable.h +++ b/src/ast/euf/euf_etable.h @@ -88,6 +88,9 @@ namespace euf { 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);