diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a138fe4f4..66175ebaa 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2824,11 +2824,9 @@ public: bool proofs_enabled() const { return m.proofs_enabled(); } - bool use_tableau() const { return lp_params(ctx().get_params()).simplex_strategy() < 2; } + void set_upper_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { set_bound(vi, ci, v, false); } - bool set_upper_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, false); } - - bool set_lower_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, true); } + void set_lower_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, true); } bool set_bound(lp::var_index vi, lp::constraint_index ci, rational const& v, bool is_lower) {