From 1af326bf069d03e50f3d20e786ad08e5d3f50101 Mon Sep 17 00:00:00 2001 From: Karthik Nukala Date: Tue, 10 Sep 2024 11:20:43 -0700 Subject: [PATCH] bug in FF extension (yices_sum_component) to Yices API --- src/api/yices_api.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 9ca060b83..bfd44b311 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -7256,8 +7256,8 @@ EXPORTED int32_t yices_sum_component(term_t t, int32_t i, mpq_t coeff, term_t *t int32_t _o_yices_sum_component(term_t t, int32_t i, mpq_t coeff, term_t *term) { if (! check_good_term(__yices_globals.manager, t) || - ! check_constructor(__yices_globals.terms, t, YICES_ARITH_SUM) || - ! check_constructor(__yices_globals.terms, t, YICES_ARITH_FF_SUM) || + !(check_constructor(__yices_globals.terms, t, YICES_ARITH_SUM) || + check_constructor(__yices_globals.terms, t, YICES_ARITH_FF_SUM)) || ! check_child_idx(__yices_globals.terms, t, i)) { return -1; }