mirror of
https://github.com/Z3Prover/z3
synced 2025-06-05 21:53:23 +00:00
revert lt change
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b78c7887f6
commit
dda9242616
1 changed files with 2 additions and 2 deletions
|
@ -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 && arg->get_id() < prev->get_id();
|
s |= prev && lt(arg, prev);
|
||||||
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 || arg->get_id() >= prev->get_id());
|
ordered &= (!prev || !lt(arg, prev));
|
||||||
prev = arg;
|
prev = arg;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue