From 690bc51b7fffff5a7d647eafb536f62c8aaa9e07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Jan 2021 15:40:15 -0800 Subject: [PATCH] fix #4927 --- src/ast/arith_decl_plugin.h | 3 +++ src/tactic/arith/lia2card_tactic.cpp | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 54eeea3e0..1aeecdaac 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -411,6 +411,9 @@ public: 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 52e2b0e3a..7f333dc1b 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -192,7 +192,7 @@ public: 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++) {