mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #2796

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-10 15:37:40 -08:00
parent 184f7cedf6
commit c839f58276
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_seq.cpp
View file

@ -2045,7 +2045,7 @@ bool theory_seq::is_pre(expr* e, expr*& s, expr*& i) {
}
bool theory_seq::is_post(expr* e, expr*& s, expr*& l) {
return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), l = to_app(e)->get_arg(2), true);
return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), l = to_app(e)->get_arg(1), true);
}
expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
@ -5318,12 +5318,12 @@ void theory_seq::add_extract_axiom(expr* e) {
add_extract_suffix_axiom(e, s, i);
return;
}
expr_ref x(mk_skolem(m_pre, s, i), m);
expr_ref x(mk_skolem(m_pre, s, i, l), m);
expr_ref ls = mk_len(s);
expr_ref lx = mk_len(x);
expr_ref le = mk_len(e);
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i), l), m);
expr_ref y(mk_skolem(m_post, s, i, ls_minus_i_l), m);
expr_ref y(mk_skolem(m_post, s, ls_minus_i_l, i, l), m);
expr_ref xe = mk_concat(x, e);
expr_ref xey = mk_concat(x, e, y);
expr_ref zero(m_autil.mk_int(0), m);

2
src/tactic/arith/bv2real_rewriter.cpp
View file

@ -152,7 +152,7 @@ void bv2real_util::mk_sbv2real(expr* e, expr_ref& result) {
expr* bv2real_util::mk_bv_mul(rational const& n, expr* t) {
if (n.is_one()) return t;
expr_ref s(mk_sbv(n), m());
expr_ref s(mk_sbv(n), m());
return mk_bv_mul(s, t);
}