mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

fix #4927

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-08 15:40:15 -08:00
parent bb56443e71
commit 690bc51b7f
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/arith_decl_plugin.h
View file

@ -411,6 +411,9 @@ public:
app * mk_int(int i) { app * mk_int(int i) {
return mk_numeral(rational(i), true); return mk_numeral(rational(i), true);
} }
app * mk_int(unsigned i) {
return mk_numeral(rational(i), true);
}
app * mk_int(rational const& r) { app * mk_int(rational const& r) {
return mk_numeral(r, true); return mk_numeral(r, true);
} }

2
src/tactic/arith/lia2card_tactic.cpp
View file

@ -192,7 +192,7 @@ public:
expr_ref b = mk_bounded(axioms, to_app(x), lo.get_unsigned(), hi.get_unsigned()); expr_ref b = mk_bounded(axioms, to_app(x), lo.get_unsigned(), hi.get_unsigned());
rep.insert(x, b); rep.insert(x, b);
m_bounds.insert(x, bound(lo.get_unsigned(), hi.get_unsigned(), 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++) { for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {