From be1df279ecac4bb3a9a07008368540d1b860faba Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 31 Jul 2017 14:11:07 -0400
Subject: [PATCH] make proof_checker less verbose

---
 src/ast/proof_checker/proof_checker.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp
index 45223cdb7..df4a8e344 100644
--- a/src/ast/proof_checker/proof_checker.cpp
+++ b/src/ast/proof_checker/proof_checker.cpp
@@ -1299,7 +1299,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
         is_pos = !is_pos;
     }
     if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) {
-        IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";);
+        IF_VERBOSE(2, verbose_stream() << "Not arith literal: " << mk_pp(lit, m) << "\n";);
         return false;
     }
     SASSERT(lit->get_num_args() == 2);
@@ -1363,7 +1363,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
         rw(sum);
     }
 
-    IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
+    IF_VERBOSE(2, verbose_stream() << "coeff,lit,sum " << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
 #endif
 
     return true;