From 052e6cec477d3cd67cee462feb1f863d7c60d404 Mon Sep 17 00:00:00 2001
From: Yurii Kostyukov <kostyukov.yurii@gmail.com>
Date: Tue, 24 Oct 2023 13:28:09 +0300
Subject: [PATCH] [fix] rewriting ordering for terms with equal height

---
 include/klee/Expr/Expr.h |  4 ++--
 lib/Expr/Constraints.cpp | 32 ++++++++++++++------------------
 lib/Expr/Expr.cpp        | 10 ++++++----
 3 files changed, 22 insertions(+), 24 deletions(-)

diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
index df98d892f98..4646b1a3c8e 100644
--- a/include/klee/Expr/Expr.h
+++ b/include/klee/Expr/Expr.h
@@ -304,8 +304,8 @@ class Expr {
   std::string toString() const;
 
   /// Returns the pre-computed hash of the current expression
-  virtual unsigned hash() const { return hashValue; }
-  virtual unsigned height() const { return heightValue; }
+  unsigned hash() const { return hashValue; }
+  unsigned height() const { return heightValue; }
 
   /// (Re)computes the hash of the current expression.
   /// Returns the hash value.
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 241c1a329b7..ae00a3303ce 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -423,27 +423,23 @@ Simplificator::simplifyExpr(const constraints_ty &constraints,
 
   for (auto &constraint : constraints) {
     if (const EqExpr *ee = dyn_cast<EqExpr>(constraint)) {
-      ref<Expr> left = ee->left;
-      ref<Expr> right = ee->right;
-      if (right->height() < left->height()) {
-        left = ee->right;
-        right = ee->left;
-      }
-      if (isa<ConstantExpr>(ee->left)) {
-        equalities.insert(std::make_pair(ee->right, ee->left));
-        equalitiesParents.insert({ee->right, constraint});
-      } else {
-        equalities.insert(std::make_pair(constraint, Expr::createTrue()));
-        equalities.insert(std::make_pair(right, left));
-        equalitiesParents.insert({constraint, constraint});
-        equalitiesParents.insert({right, constraint});
+      ref<Expr> small = ee->left;
+      ref<Expr> big = ee->right;
+      if (!isa<ConstantExpr>(small)) {
+        auto hr = big->height(), hl = small->height();
+        if (hr < hl || (hr == hl && big < small))
+          std::swap(small, big);
+        equalities.emplace(constraint, Expr::createTrue());
+        equalitiesParents.emplace(constraint, constraint);
       }
+      equalities.emplace(big, small);
+      equalitiesParents.emplace(big, constraint);
     } else {
-      equalities.insert(std::make_pair(constraint, Expr::createTrue()));
-      equalitiesParents.insert({constraint, constraint});
+      equalities.emplace(constraint, Expr::createTrue());
+      equalitiesParents.emplace(constraint, constraint);
       if (const NotExpr *ne = dyn_cast<NotExpr>(constraint)) {
-        equalities.insert(std::make_pair(ne->expr, Expr::createFalse()));
-        equalitiesParents.insert({ne->expr, constraint});
+        equalities.emplace(ne->expr, Expr::createFalse());
+        equalitiesParents.emplace(ne->expr, constraint);
       }
     }
   }
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index c889af5ed4a..4f26cb1aaa9 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -153,11 +153,13 @@ int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
     return 0;
 
   Kind ak = getKind(), bk = b.getKind();
-  if (ak != bk)
-    return (ak < bk) ? -1 : 1;
+  int kc = (ak > bk) - (ak < bk);
+  if (kc)
+    return kc;
 
-  if (hashValue != b.hashValue)
-    return (hashValue < b.hashValue) ? -1 : 1;
+  int hc = (hashValue > b.hashValue) - (hashValue < b.hashValue);
+  if (hc)
+    return hc;
 
   if (int res = compareContents(b))
     return res;