From debe04350cf620c3e54b6ed84c43c75e62c619a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Aug 2025 09:30:03 -0700 Subject: [PATCH] fix #7796 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/extract_eqs.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp index ffc8c7cb7..8789fa569 100644 --- a/src/ast/simplifiers/extract_eqs.cpp +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -115,7 +115,7 @@ namespace euf { if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2)) eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d)); } - if (m.is_and(f, x1, y1) && m.is_or(x, x1, x2) && m.is_or(y1, y1, y2)) { + if (m.is_and(f, x1, y1) && m.is_or(x1, x1, x2) && m.is_or(y1, y1, y2)) { expr* z = nullptr, *t = nullptr, *s = nullptr; if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2)) eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d));