From c839f5827615728e913bd32d8ac41ed8a2fad73e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Dec 2019 15:37:40 -0800 Subject: [PATCH] fix #2796 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 6 +++--- src/tactic/arith/bv2real_rewriter.cpp | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index bddb744cb..79c596b18 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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); diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp index 2a811b9c0..2398a2a32 100644 --- a/src/tactic/arith/bv2real_rewriter.cpp +++ b/src/tactic/arith/bv2real_rewriter.cpp @@ -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); }