From 79eb6a0e66ee32aedeb90d3eaa64dd1c8aed6880 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 31 Mar 2020 12:22:43 +0100 Subject: [PATCH] reduce_invertible: fix mk_diagonal for BV 0 switch from -x to ~x --- src/tactic/core/reduce_invertible_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index f7c0dadbf..8d967098e 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -415,7 +415,7 @@ private: return false; } 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; } } @@ -424,13 +424,13 @@ private: bool has_diagonal(expr* e) { return - m_bv.is_bv(e) || + m_bv.is_bv(e) || m.is_bool(e) || m_arith.is_int_real(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_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);