diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 9354b53f6..cd6e2e353 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -229,7 +229,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args pos_lits.mark(arg); } buffer.push_back(arg); - s |= prev && lt(arg, prev); + s |= prev && arg->get_id() < prev->get_id(); prev = arg; } @@ -327,7 +327,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args, } else { flat_args.push_back(arg); - ordered &= (!prev || !lt(arg, prev)); + ordered &= (!prev || arg->get_id() >= prev->get_id()); prev = arg; } }