mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-13 06:30:54 +00:00
Code Activity

fix model gen for regex terms in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-03-06 17:04:07 -05:00
parent 577cb19745
commit 4d5c1dcfb6
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_str.h
View file

@ -63,9 +63,14 @@ namespace smt {
m_strings.insert(sym); m_strings.insert(sym);
return u.str.mk_string(sym); return u.str.mk_string(sym);
} }
} else {
UNREACHABLE(); return NULL;
} }
sort* seq = 0;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
}
TRACE("t_str", tout << "unexpected sort in get_fresh_value(): " << mk_pp(s, m_manager) << std::endl;);
UNREACHABLE(); return NULL;
} }
virtual void register_value(expr * n) { /* Ignore */ } virtual void register_value(expr * n) { /* Ignore */ }
}; };