From 73d8f935bb107c4c9f1325d3370a89f873ec10d0 Mon Sep 17 00:00:00 2001
From: Dave Thaler <dthaler@microsoft.com>
Date: Fri, 22 Oct 2021 19:07:32 -0700
Subject: [PATCH] Make verbose output format for invariants more readable

Use separate lines for each set of invariants related to the same
category (e.g., each register).

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
---
 src/string_constraints.cpp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/string_constraints.cpp b/src/string_constraints.cpp
index 7a51ca7e0..3538efc38 100644
--- a/src/string_constraints.cpp
+++ b/src/string_constraints.cpp
@@ -127,11 +127,19 @@ std::ostream& operator<<(std::ostream& o, const string_invariant& inv) {
     // Intervals
     bool first = true;
     o << "[";
-    for (const auto& item : inv.maybe_inv.value()) {
+    auto& set = inv.maybe_inv.value();
+    std::string lastbase;
+    for (const auto& item : set) {
         if (first)
             first = false;
         else
             o << ", ";
+        size_t pos = item.find_first_of(".=[");
+        std::string base = item.substr(0, pos);
+        if (base != lastbase) {
+            o << "\n    ";
+            lastbase = base;
+        }
         o << item;
     }
     o << "]";