mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 09:50:23 +00:00
Code Activity

Fix issue http://z3.codeplex.com/workitem/45

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-06-05 13:50:22 -07:00
parent b6d9d8a601
commit 110fa0b7fb
2 changed files with 33 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/simplifier/poly_simplifier_plugin.cpp
View file

@ -285,6 +285,7 @@ bool poly_simplifier_plugin::merge_monomials(bool inv, expr * n1, expr * n2, exp
else
result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k1), b);
}
TRACE("merge_monomials", tout << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";);
return true;
}