mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

Fix order of arguments when normalizing a conjunction

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-28 14:21:32 -04:00
parent a8c9e3a837
commit a63e4b48ca
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/spacer/spacer_util.cpp
View file

@ -666,9 +666,6 @@ namespace {
flatten_and(out, v); flatten_and(out, v);
if (v.size() > 1) { if (v.size() > 1) {
// sort arguments of the top-level and
std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
if (use_simplify_bounds) { if (use_simplify_bounds) {
// remove redundant inequalities // remove redundant inequalities
simplify_bounds(v); simplify_bounds(v);
@ -680,6 +677,8 @@ namespace {
v.reset(); v.reset();
egraph.to_lits(v); egraph.to_lits(v);
} }
// sort arguments of the top-level and
std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
TRACE("spacer_normalize", TRACE("spacer_normalize",
tout << "Normalized:\n" tout << "Normalized:\n"