#5336

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jun 20, 2021 · f7d1cce · f7d1cce
1 parent 2138ef2
commit f7d1cce
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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);