1 files changed, 7 insertions, 3 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index a7b33ae26..af6cae796 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -276,9 +276,13 @@ void usortsToBitVectors(const LogicInfo& d_logic,
     for (size_t i = 0, size = assertions->size(); i < size; ++i)
     {
       Node old = (*assertions)[i];
-      assertions->replace(i, usVarsToBVVars.apply((*assertions)[i]));
-      Trace("uninterpretedSorts-to-bv")
-          << "  " << old << " => " << (*assertions)[i] << "\n";
+      Node newA = usVarsToBVVars.apply((*assertions)[i]);
+      if (newA != old)
+      {
+        assertions->replace(i, newA);
+        Trace("uninterpretedSorts-to-bv")
+            << "  " << old << " => " << (*assertions)[i] << "\n";
+      }
     }
   }
 }