z3/z3-gcc-10-s390x.patch

16 lines
730 B
Diff
Raw Normal View History

Add explicit template instantiation to work around an s390x problem:
https://bugzilla.redhat.com/show_bug.cgi?id=1794127
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -829,6 +829,9 @@ void lar_solver::update_x_and_inf_costs_
update_x_and_inf_costs_for_column_with_changed_bounds(j);
}
+// See https://bugzilla.redhat.com/show_bug.cgi?id=1794127
+extern template void lp::lp_primal_core_solver<rational, lp::numeric_pair<rational> >::update_inf_cost_for_column_tableau(unsigned int);
+
void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() {
for (auto j : m_columns_with_changed_bound.m_index)
update_x_and_inf_costs_for_column_with_changed_bounds(j);