mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

fix #6894

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-14 17:10:53 -07:00
parent 50d76a2fe3
commit b87a91379c
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/simplifiers/solve_context_eqs.cpp
View file

@ -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;
}