diff --git a/src/util/lp/lp_settings.cpp b/src/util/lp/lp_settings.cpp index 342ec65e6e..50ff025c87 100644 --- a/src/util/lp/lp_settings.cpp +++ b/src/util/lp/lp_settings.cpp @@ -4,6 +4,7 @@ Author: Lev Nachmanson */ +#include #include "util/numerics/double.h" #include "util/lp/lp_settings.h" namespace lean { @@ -93,7 +94,7 @@ bool vectors_are_equal(T * a, std::vector &b, unsigned n) { } } else { for (unsigned i = 0; i < n; i ++){ - if (fabs(numeric_traits::get_double(a[i] - b[i])) > 0.000001) { + if (std::abs(numeric_traits::get_double(a[i] - b[i])) > 0.000001) { std::cout << "a[" << i <<"]" << a[i] << ", " << "b[" << i <<"]" << b[i] << std::endl; return false; } @@ -146,4 +147,3 @@ bool vectors_are_equal(const std::vector & a, const std::vector &b) { return true; } } -