From ad90f3a4df383c22f364eb39237615364bb0fb27 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 1 May 2024 22:34:00 -0700 Subject: [PATCH] Update uf_plugin.c --- src/mcsat/uf/uf_plugin.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mcsat/uf/uf_plugin.c b/src/mcsat/uf/uf_plugin.c index bcfea452d..b8411b04a 100644 --- a/src/mcsat/uf/uf_plugin.c +++ b/src/mcsat/uf/uf_plugin.c @@ -234,8 +234,8 @@ void uf_plugin_add_to_eq_graph(uf_plugin_t* uf, term_t t, bool record) { term_t r1 = app_term(terms, t, t_desc->arity - 2, t_desc->arg + 1); variable_db_get_variable(uf->ctx->var_db, r1); weq_graph_add_select_term(&uf->weq_graph, r1); - // if the domain is finite then we add this extra read term - if (is_finite_type(terms->types, term_type(terms, t_desc->arg[1]))) { + // if the element domain is finite then we add this extra read term + if (is_finite_type(terms->types, term_type(terms, t_desc->arg[2]))) { term_t r2 = app_term(terms, t_desc->arg[0], t_desc->arity - 2, t_desc->arg + 1); variable_db_get_variable(uf->ctx->var_db, r2); weq_graph_add_select_term(&uf->weq_graph, r2);