From 872cc0f3f1947618dc70f9ff7e4cc6e7072b935e Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Wed, 8 Jul 2026 11:11:35 -0700 Subject: [PATCH] Oops.. constants go through get_cg_root now --- src/smt/smt_context.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 000de5da14..0a5ad1d5c7 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -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())