rpms
/
z3
2
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Another try with the -gcc-10-s390x patch.

This commit is contained in:
Jerry James 2020-01-23 14:22:43 -07:00
parent 7f69c91f2c
commit 8a9847e6d4
1 changed files with 8 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
z3-gcc-10-s390x.patch
View File

@ -1,15 +1,12 @@
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);
}
--- a/src/util/lp/lp_primal_core_solver.cpp
+++ b/src/util/lp/lp_primal_core_solver.cpp
@@ -38,5 +38,6 @@ template void lp::lp_primal_core_solver<
template bool lp::lp_primal_core_solver<lp::mpq, lp::mpq>::update_basis_and_x_tableau(int, int, lp::mpq const&);
template bool lp::lp_primal_core_solver<double, double>::update_basis_and_x_tableau(int, int, double const&);
template bool lp::lp_primal_core_solver<lp::mpq, lp::numeric_pair<lp::mpq> >::update_basis_and_x_tableau(int, int, lp::numeric_pair<lp::mpq> const&);
+template void lp::lp_primal_core_solver<rational, lp::numeric_pair<rational> >::update_inf_cost_for_column_tableau(unsigned);
+// 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);
}