mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 01:46:15 +00:00
Code Activity

reduce_invertible: fix mk_diagonal for BV 0

Browse source 
switch from -x to ~x
This commit is contained in:
Nuno Lopes 2020-03-31 12:22:43 +01:00
parent 0b6b267ec4
commit 79eb6a0e66
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -415,7 +415,7 @@ private:
return false; return false;
} }
else if (is_var(v) && is_non_singleton_sort(m.get_sort(v))) { else if (is_var(v) && is_non_singleton_sort(m.get_sort(v))) {
new_v = m.mk_var(to_var(v)->get_idx(), m.mk_bool_sort()); new_v = m.mk_var(to_var(v)->get_idx(), m.mk_bool_sort());
return true; return true;
} }
} }
@ -424,13 +424,13 @@ private:
bool has_diagonal(expr* e) { bool has_diagonal(expr* e) {
return return
m_bv.is_bv(e) || m_bv.is_bv(e) ||
m.is_bool(e) || m.is_bool(e) ||
m_arith.is_int_real(e); m_arith.is_int_real(e);
} }
expr * mk_diagonal(expr* e) { expr * mk_diagonal(expr* e) {
if (m_bv.is_bv(e)) return m_bv.mk_bv_neg(e); if (m_bv.is_bv(e)) return m_bv.mk_bv_not(e);
if (m.is_bool(e)) return m.mk_not(e); if (m.is_bool(e)) return m.mk_not(e);
if (m_arith.is_int(e)) return m_arith.mk_add(m_arith.mk_int(1), e); if (m_arith.is_int(e)) return m_arith.mk_add(m_arith.mk_int(1), e);
if (m_arith.is_real(e)) return m_arith.mk_add(m_arith.mk_real(1), e); if (m_arith.is_real(e)) return m_arith.mk_add(m_arith.mk_real(1), e);