From 5cbcd9a88ad5f5f259be8066c854c9bddd4327db Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Mar 2020 11:24:00 -0700
Subject: [PATCH] fix #3410

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_aux.h | 2 ++
 1 file changed, 2 insertions(+)

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<typename Ext>
     inf_eps_rational<inf_rational> theory_arith<Ext>::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;