mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
ever so gentle slap over the fingers for not using real regular expressions, #2058
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6f6880812b
commit
a87f7a14d3
|
@ -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 {
|
||||
|
|
|
@ -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<theory_seq, vector<s_in_re>>(m_s_in_re));
|
||||
|
|
Loading…
Reference in a new issue