mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

make sorting of soft constraints the same across implementations of std::sort

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-25 11:32:35 -07:00
parent e6df7b73aa
commit 8a0d79251e
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/maxres.cpp
View file

@ -435,7 +435,9 @@ public:
maxres& mr;
compare_asm(maxres& mr):mr(mr) {}
bool operator()(expr* a, expr* b) const {
return mr.get_weight(a) > mr.get_weight(b);
rational w1 = mr.get_weight(a);
rational w2 = mr.get_weight(b);
return w1 > w2 || (w1 == w2 && a->get_id() > b->get_id());
}
};