From 3533a090105a5e26064bae50635e3f52a0c7846a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Jul 2014 23:48:49 +0200 Subject: [PATCH] bit2bool bug reported by Sagar Chaki Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_bit_blast.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 112541541..90d410ab1 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -88,11 +88,12 @@ namespace datalog { for (unsigned j = 0; j < arity_q; ++j) { sort* s = q->get_domain(j); arg = m.mk_var(j, s); + expr* t = arg; if (m_bv.is_bv_sort(s)) { - expr* args[1] = { arg }; unsigned sz = m_bv.get_bv_size(s); for (unsigned k = 0; k < sz; ++k) { - proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args); + parameter p(k); + proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t); sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj); } }