From a87f7a14d33a6f9fe8c97b2ab583b85eaec5b862 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Jan 2019 13:46:04 -0800 Subject: [PATCH] ever so gentle slap over the fingers for not using real regular expressions, #2058 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 4 ++++ src/smt/theory_seq.cpp | 7 ++++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 7d45c9707..49d545894 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1720,6 +1720,10 @@ namespace z3 { m_vector = s.m_vector; return *this; } + ast_vector_tpl& set(unsigned idx, ast& a) { + Z3_ast_vector_set(ctx(), m_vector, idx, a); + return *this; + } /* Disabled pending C++98 build upgrade bool contains(T const& x) const { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e8af44d7e..e384c7b1f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -4584,7 +4584,12 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { IF_VERBOSE(11, verbose_stream() << mk_pp(s, m) << " in " << re << "\n"); eautomaton* a = get_automaton(re); - if (!a) return; + if (!a) { + std::stringstream strm; + strm << "expression " << re << " does not correspond to a supported regular expression"; + TRACE("seq", tout << strm.str() << "\n";); + throw default_exception(strm.str()); + } m_s_in_re.push_back(s_in_re(lit, s, re, a)); m_trail_stack.push(push_back_vector>(m_s_in_re));