mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Lev's fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-11 10:12:39 -07:00
parent f90db2ba1c
commit de69b01e92
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_seq.cpp
View file

@ -4996,6 +4996,7 @@ void theory_seq::add_extract_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";); TRACE("seq", tout << mk_pp(e, m) << "\n";);
expr* s = nullptr, *i = nullptr, *l = nullptr; expr* s = nullptr, *i = nullptr, *l = nullptr;
VERIFY(m_util.str.is_extract(e, s, i, l)); VERIFY(m_util.str.is_extract(e, s, i, l));
#if 0
if (is_tail(s, i, l)) { if (is_tail(s, i, l)) {
add_tail_axiom(e, s); add_tail_axiom(e, s);
return; return;
@ -5012,6 +5013,7 @@ void theory_seq::add_extract_axiom(expr* e) {
add_extract_suffix_axiom(e, s, i); add_extract_suffix_axiom(e, s, i);
return; return;
} }
#endif
expr_ref x(mk_skolem(m_pre, s, i), m); expr_ref x(mk_skolem(m_pre, s, i), m);
expr_ref ls = mk_len(s); expr_ref ls = mk_len(s);
expr_ref lx = mk_len(x); expr_ref lx = mk_len(x);