From b87a91379ce6ac5d71dc5b46805e0df77b90219c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Sep 2023 17:10:53 -0700 Subject: [PATCH] fix #6894 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/solve_context_eqs.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp index 31696dc54..c58786f0e 100644 --- a/src/ast/simplifiers/solve_context_eqs.cpp +++ b/src/ast/simplifiers/solve_context_eqs.cpp @@ -311,11 +311,12 @@ namespace euf { return p == i; }; - // retrieve oldest parent of i whose sign is false + // retrieve oldest parent of i within the same alternation of and unsigned pi = i; + auto [_s, _depth, _f, _p] = todo[i]; while (pi != 0) { auto [s, depth, f, p] = todo[pi]; - if (s) + if (depth != _depth) break; pi = p; }