diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 54eeea3e082..1aeecdaac0f 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -411,6 +411,9 @@ class arith_util : public arith_recognizers {
     app * mk_int(int i) {
         return mk_numeral(rational(i), true);
     }
+    app * mk_int(unsigned i) {
+        return mk_numeral(rational(i), true);
+    }
     app * mk_int(rational const& r) {
         return mk_numeral(r, true);
     }
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 52e2b0e3a02..7f333dc1b44 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -192,7 +192,7 @@ class lia2card_tactic : public tactic {
                 expr_ref b = mk_bounded(axioms, to_app(x), lo.get_unsigned(), hi.get_unsigned());
                 rep.insert(x, b);
                 m_bounds.insert(x, bound(lo.get_unsigned(), hi.get_unsigned(), b));
-                TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";);
+                TRACE("pb", tout << "add bound " << lo << " " << hi << ": " << mk_pp(x, m) << "\n";);
             }
         }
         for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {