diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp
index 08d69ff25..5cf981ee2 100644
--- a/src/ast/proofs/proof_checker.cpp
+++ b/src/ast/proofs/proof_checker.cpp
@@ -104,8 +104,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
         m_todo.pop_back();
         result = check1(curr.get(), side_conditions);
         if (!result) {
-            IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););
-            UNREACHABLE();
+            IF_VERBOSE(1, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););
         }
     }
 
@@ -1393,7 +1392,7 @@ bool proof_checker::check_arith_proof(proof* p) {
         }
     }
 
-    unsigned num_parents     = m.get_num_parents(p);
+    unsigned num_parents = m.get_num_parents(p);
     for (unsigned i = 0; i < num_parents; i++) {
         proof * a = m.get_parent(p, i);
         SASSERT(m.has_fact(a));
@@ -1401,6 +1400,11 @@ bool proof_checker::check_arith_proof(proof* p) {
             return false;
         }
     }
+    TRACE("proof_checker", 
+          for (unsigned i = 0; i < num_parents; i++) 
+              tout << coeffs[i] << " * " << mk_bounded_pp(m.get_fact(m.get_parent(p, i)), m) << "\n";
+          tout << "fact:" << mk_bounded_pp(fact, m) << "\n";);
+    
     if (m.is_or(fact)) {
         app* disj = to_app(fact);
         unsigned num_args = disj->get_num_args();
@@ -1435,7 +1439,7 @@ bool proof_checker::check_arith_proof(proof* p) {
     rw(sum);
 
     if (!m.is_false(sum)) {
-        IF_VERBOSE(0, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";);
+        IF_VERBOSE(1, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";);
         m_dump_lemmas = true;
         dump_proof(p);
         return false;
diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h
index bf271bc75..2e55be210 100644
--- a/src/ast/proofs/proof_utils.h
+++ b/src/ast/proofs/proof_utils.h
@@ -122,7 +122,7 @@ public:
     {
         DEBUG_CODE(proof_checker pc(m);
                    expr_ref_vector side(m);
-                   SASSERT(pc.check(pr, side));
+                   if (!pc.check(pr, side)) IF_VERBOSE(1, verbose_stream() << "check failed: " << mk_pp(pr, m) << "\n");
                   );
         obj_map<app, app*> cache;
         bool_rewriter brwr(m);
@@ -236,7 +236,7 @@ public:
         DEBUG_CODE(
             proof_checker pc(m);
             expr_ref_vector side(m);
-            SASSERT(pc.check(r, side));
+            if (!pc.check(r, side)) IF_VERBOSE(1, verbose_stream() << mk_pp(r, m) << "check failed\n");
         );
 
         res = r ;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index ade915fb6..5da77cd29 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2534,7 +2534,8 @@ namespace smt {
         b1->push_justification(ante, numeral(1), coeffs_enabled());
         b2->push_justification(ante, numeral(1), coeffs_enabled());
         TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
-              tout << "bounds: " << b1 << " " << b2 << "\n";);
+              display_bound(tout, b1, 0);
+              display_bound(tout, b2, 0););
         set_conflict(ante, ante, "farkas");
     }