From bbfac99b22949b5ac1d7892e74036fefb49d1ba7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Aug 2019 13:52:42 -0700 Subject: [PATCH] fix #2469 Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 2 +- src/tactic/core/elim_uncnstr_tactic.cpp | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index c147e6c67..00136c021 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -193,7 +193,7 @@ extern "C" { MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP); MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP); MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP); - MK_BINARY(Z3_mk_seq_nth, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP); + MK_BINARY(Z3_mk_seq_nth, mk_c(c)->get_seq_fid(), OP_SEQ_NTH, SKIP); MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP); MK_TERNARY(Z3_mk_seq_index, mk_c(c)->get_seq_fid(), OP_SEQ_INDEX, SKIP); MK_BINARY(Z3_mk_seq_last_index, mk_c(c)->get_seq_fid(), OP_SEQ_LAST_INDEX, SKIP); diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index c26e7b9eb..bca13366f 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -93,7 +93,6 @@ class elim_uncnstr_tactic : public tactic { } v = m().mk_fresh_const(nullptr, m().get_sort(t)); - std::cout << mk_pp(t, m()) << " -> " << mk_pp(v, m()) << "\n"; TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";); TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";); m_fresh_vars.push_back(v);