mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
nits
This commit is contained in:
parent
d0ef5948aa
commit
4b495e4b96
|
@ -217,14 +217,14 @@ template <typename T, typename X> void lp_dual_simplex<T, X>::fill_costs_bounds_
|
|||
m_can_enter_basis[j] = true;
|
||||
this->set_scaled_cost(j);
|
||||
this->m_lower_bounds[j] = numeric_traits<T>::zero();
|
||||
this->m_upper_bounds[j] =numeric_traits<T>::one();
|
||||
this->m_upper_bounds[j] = numeric_traits<T>::one();
|
||||
break;
|
||||
}
|
||||
case column_type::free_column: {
|
||||
m_can_enter_basis[j] = true;
|
||||
this->set_scaled_cost(j);
|
||||
this->m_upper_bounds[j] = free_bound;
|
||||
this->m_lower_bounds[j] = -free_bound;
|
||||
this->m_upper_bounds[j] = free_bound;
|
||||
this->m_lower_bounds[j] = -free_bound;
|
||||
break;
|
||||
}
|
||||
case column_type::boxed:
|
||||
|
|
|
@ -362,6 +362,11 @@ br_status bv2real_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
|
|||
tout << mk_pp(args[i], m()) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
|
||||
if (u().memory_exceeded()) {
|
||||
std::cout << "tactic exception\n";
|
||||
throw tactic_exception("bv2real-memory exceeded");
|
||||
}
|
||||
if(f->get_family_id() == m_arith.get_family_id()) {
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_NUM: return BR_FAILED;
|
||||
|
|
Loading…
Reference in a new issue