From 8a0d79251e6cf169e5ac7c24993bf94057efa85d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Jul 2019 11:32:35 -0700
Subject: [PATCH] make sorting of soft constraints the same across
 implementations of std::sort

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxres.cpp    | 4 +++-
 src/sat/ba_solver.cpp | 6 +++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 25b51372e..483db7e70 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -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());
         }
     };
 
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 63387c866..99dab4ecf 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2991,7 +2991,7 @@ namespace sat {
             init_use_lists();
             remove_unused_defs();
             set_non_external();
-            //if (get_config().m_elim_vars && !s().get_config().m_incremental && !s().tracking_assumptions()) elim_pure();
+            elim_pure();
             for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
             for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);    
             unit_strengthen();
@@ -3563,6 +3563,7 @@ namespace sat {
     }
 
     void ba_solver::remove_unused_defs() {
+        if (incremental_mode()) return;
         // remove constraints where indicator literal isn't used.
         for (constraint* cp : m_constraints) {
             constraint& c = *cp;
@@ -3634,6 +3635,9 @@ namespace sat {
     }
 
     unsigned ba_solver::elim_pure() {
+        if (!get_config().m_elim_vars || incremental_mode()) {
+            return 0;
+        }
         // eliminate pure literals
         unsigned pure_literals = 0;
         for (unsigned v = 0; v < s().num_vars(); ++v) {