mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #1819

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-10 13:53:44 -07:00
parent def6f19edb
commit a37d05d54b
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_arith_int.h
View file

@ -396,7 +396,9 @@ namespace smt {
for (; it != end; ++it) {
if (!it->is_dead() && it->m_var != b && is_free(it->m_var)) {
theory_var v = it->m_var;
expr * bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(rational::zero(), is_int(v)));
expr* e = get_enode(v)->get_owner();
bool _is_int = m_util.is_int(e);
expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int));
context & ctx = get_context();
ctx.internalize(bound, true);
ctx.mark_as_relevant(bound);