mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

fix #6742

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-13 19:22:31 -07:00
parent 4a9c4ca2ce
commit 3727f70363
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bool_rewriter.cpp
View file

@ -229,7 +229,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
pos_lits.mark(arg); pos_lits.mark(arg);
} }
buffer.push_back(arg); buffer.push_back(arg);
s |= prev && lt(arg, prev); s |= prev && arg->get_id() < prev->get_id();
prev = arg; prev = arg;
} }
@ -327,7 +327,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
} }
else { else {
flat_args.push_back(arg); flat_args.push_back(arg);
ordered &= (!prev || !lt(arg, prev)); ordered &= (!prev || arg->get_id() >= prev->get_id());
prev = arg; prev = arg;
} }
} }