mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Oops.. constants go through get_cg_root now

Browse source
This commit is contained in:
Can Cebeci 2026-07-08 11:11:35 -07:00
parent bc753b510d
commit 872cc0f3f1
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.h
View file

@ -1227,8 +1227,8 @@ namespace smt {
static bool is_eq(enode const * n1, enode const * n2) { return n1->get_root() == n2->get_root(); }
enode * get_cg_root(enode * n) const {
SASSERT(n->get_num_args() > 0);
SASSERT(n->uses_cg_table() || n->is_cgr());
if (!n->uses_cg_table())
return n;
// Fast path: if e is already the congruence root, avoid table lookup.
// This is important for performance, since get_cg_root is called on every generation lookup.
if (n->is_cgr())