3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-26 20:48:19 +08:00
parent 9903c722af
commit 72c3473400

View file

@ -166,12 +166,10 @@ namespace smt {
SASSERT(m_is_optimal); SASSERT(m_is_optimal);
flows.reset(); flows.reset();
flows.append(m_flows); flows.append(m_flows);
numeral cost(0); objective = numeral::zero();
for (unsigned int i = 0; i < m_flows.size(); ++i) { for (unsigned int i = 0; i < m_flows.size(); ++i) {
// FIXME: this * operator is not supported objective += m_costs[i] * m_flows[i];
cost += m_costs[i] * m_flows[i];
} }
objective = cost;
} }
// Minimize cost flows // Minimize cost flows