From 7a03f194567f1322dc0b6548c29fe102a92cea87 Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Sun, 29 Apr 2018 13:08:57 +0200
Subject: [PATCH] fixing smt code ending up in log files (verbose logging)

---
 src/smt/smt_context_pp.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index f4f56df5d..f072a1d13 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -580,20 +580,20 @@ namespace smt {
         case b_justification::BIN_CLAUSE: {
             literal l2 = j.get_literal();
             out << "bin-clause ";
-            display_literal_verbose(out, l2);
+            display_literal(out, l2);
             break;
         }
         case b_justification::CLAUSE: {
             clause * cls = j.get_clause();
             out << "clause ";
-            if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
+            if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
             break;
         }
         case b_justification::JUSTIFICATION: {
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals_verbose(out, lits);
+            display_literals(out, lits);
             break;
         }
         default: