From de8b2041e6d09d86a243831db49c8b57bef7700d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Jul 2021 00:03:32 +0200
Subject: [PATCH] make bpp work with nullptr

---
 src/ast/ast_ll_pp.cpp      | 4 +++-
 src/sat/smt/euf_solver.cpp | 6 ++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index 62dbd74b5..f7ba8132f 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -303,7 +303,9 @@ public:
     }
 
     void display_bounded(ast * n, unsigned depth) {
-        if (is_app(n)) {
+        if (!n)
+   	     m_out << "null";    
+        else if (is_app(n)) {
             display(to_expr(n), depth);
         }
         else if (is_var(n)) {
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index e8c9bb54f..f66c4a331 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -286,11 +286,9 @@ namespace euf {
 
     void solver::asserted(literal l) {
         expr* e = m_bool_var2expr.get(l.var(), nullptr);
-        if (!e) {
-            TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";);
+	TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
+        if (!e) 
             return;        
-        }
-        TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
         euf::enode* n = m_egraph.find(e);
         if (!n)
             return;