mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 07:15:26 +00:00
Code Activity

fix a bug in nla_intervals - add explanations when getting intervals from a term

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-28 17:18:51 -08:00
parent ab92c20106
commit 66dd93a035
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -166,7 +166,7 @@ rational core::product_value(const unsigned_vector & m) const {
bool core::check_monic(const monic& m) const { bool core::check_monic(const monic& m) const {
SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int());
bool ret = product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); bool ret = product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var());
CTRACE("nla_solver", !ret, print_monic(m, tout) << '\n';); CTRACE("nla_solver_check_monic", !ret, print_monic(m, tout) << '\n';);
return ret; return ret;
} }