mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

#5336

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-19 22:12:52 -07:00
parent 2138ef2ad0
commit f7d1cce69a
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/euf/euf_etable.h
View file

@ -88,6 +88,9 @@ namespace euf {
SASSERT(n1->num_args() == 2); SASSERT(n1->num_args() == 2);
SASSERT(n2->num_args() == 2); SASSERT(n2->num_args() == 2);
if (n1->get_decl() != n2->get_decl())
return false;
SASSERT(n1->get_decl() == n2->get_decl()); SASSERT(n1->get_decl() == n2->get_decl());
enode* c1_1 = get_root(n1, 0); enode* c1_1 = get_root(n1, 0);
enode* c1_2 = get_root(n1, 1); enode* c1_2 = get_root(n1, 1);