From e09636065b0a648f176d9d7c3252a47485ca1a80 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 18 Aug 2023 15:30:39 +0200
Subject: [PATCH] don't crash on null_literal

---
 src/math/polysat/solver.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index da27b8943..67771aaba 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1643,6 +1643,8 @@ namespace polysat {
     }
 
     std::ostream& lit_pp::display(std::ostream& out) const {
+        if (lit == sat::null_literal)
+            return out << "<null_literal>";
         signed_constraint const c = s.lit2cnstr(lit);
         out << lpad(5, lit) << ": " << rpad(30, c);
         if (!c)