mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

Don't simplify bounds when normalizing a lemma

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-28 10:59:28 -04:00
parent f7512d6d5c
commit e8e27f0daf
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/spacer/spacer_context.cpp
View file

@ -538,7 +538,8 @@ void lemma::mk_expr_core() {
SASSERT(!m_cube.empty()); SASSERT(!m_cube.empty());
m_body = ::mk_and(m_cube); m_body = ::mk_and(m_cube);
// normalize works better with a cube // normalize works better with a cube
normalize(m_body, m_body); normalize(m_body, m_body, false /* no simplify bounds */, false /* term_graph */);
m_body = ::push_not(m_body); m_body = ::push_not(m_body);
if (!m_zks.empty() && has_zk_const(m_body)) { if (!m_zks.empty() && has_zk_const(m_body)) {