fix #4927

Z3Prover · Jan 8, 2021 · 690bc51 · 690bc51
1 parent bb56443
commit 690bc51
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git 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
@@ -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++) {