From c5c711ad6a584e7ccfe72316aa2521bb20345587 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sat, 18 Nov 2023 16:01:27 +0000
Subject: [PATCH] counterexamples: don't print all poison blocks

---
 ir/memory.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/ir/memory.cpp b/ir/memory.cpp
index 8fbd73299..1fd5a1379 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -283,7 +283,7 @@ expr Byte::nonptrValue() const {
 
 expr Byte::isPoison() const {
   if (!does_int_mem_access)
-    return !ptrNonpoison();
+    return  does_ptr_mem_access ? !ptrNonpoison() : true;
 
   expr np = nonptrNonpoison();
   if (byte_has_ptr_bit() && bits_poison_per_byte == 1) {
@@ -2426,8 +2426,15 @@ void Memory::print(ostream &os, const Model &m) const {
       os << '\n';
 
       if (!local && bid < numNonlocals()) {
+        expr array = m[mk_block_val_array(bid)].simplify();
+        // don't bother with all-poison blocks
+        expr val;
+        if (array.isConstArray(val) &&
+            Byte(*this, std::move(val)).isPoison().isTrue())
+          continue;
+
         os << "Contents:\n";
-        print_array(os, m[mk_block_val_array(bid)].simplify());
+        print_array(os, array);
         os << '\n';
       }
     }