From a63e4b48cae1a98c967cace1aa0f79a3d63575e2 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 28 Jun 2018 14:21:32 -0400
Subject: [PATCH] Fix order of arguments when normalizing a conjunction

---
 src/muz/spacer/spacer_util.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 3ea0917b7..ec01218f1 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -666,9 +666,6 @@ namespace {
             flatten_and(out, v);
 
             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) {
                     // remove redundant inequalities
                     simplify_bounds(v);
@@ -680,6 +677,8 @@ namespace {
                     v.reset();
                     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",
                       tout << "Normalized:\n"