mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix the build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-21 15:18:45 -07:00
parent 108bfa55ad
commit bf5b06285b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -360,7 +360,7 @@ bool horner::interval_from_term(const nex* e, interv & i) const {
lp::explanation exp; lp::explanation exp;
if (c().explain_by_equiv(norm_t, exp)) { if (c().explain_by_equiv(norm_t, exp)) {
m_intervals.set_zero_interval_with_explanation(i, exp); m_intervals.set_zero_interval_with_explanation(i, exp);
TRACE("nla_horner", tout << "explain_by_equiv\n"); TRACE("nla_horner", tout << "explain_by_equiv\n";);
return true; return true;
} }
lpvar j = find_term_column(norm_t, a); lpvar j = find_term_column(norm_t, a);