diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 64746158a..6c9016b2a 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1059,6 +1059,8 @@ namespace smt { template inf_eps_rational theory_arith::maximize(theory_var v, expr_ref& blocker, bool& has_shared) { TRACE("bound_bug", display_var(tout, v); display(tout);); + if (get_context().get_fparams().m_threads > 1) + throw default_exception("multi-threaded optimization is not supported"); has_shared = false; if (!m_nl_monomials.empty()) { has_shared = true;