From 6ff61d1f802f15a9747b5082f745991438649047 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Apr 2020 22:43:14 -0700 Subject: [PATCH] fix #4062 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ae55f38de..99dc19fe9 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1821,6 +1821,10 @@ void theory_seq::init_search_eh() { m_re2aut.reset(); m_res.reset(); m_automata.reset(); + auto as = get_context().get_fparams().m_arith_mode; + if (m_has_seq && as != AS_OLD_ARITH && as != AS_NEW_ARITH) { + throw default_exception("illegal arithmetic solver used with string solver"); + } } void theory_seq::init_model(expr_ref_vector const& es) {