From d4539b8887306fb88add26efcc1fec36a90dbccb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Aug 2016 11:42:14 +0800 Subject: [PATCH] fix dt2bv transformation to only work with constants, issue #725 Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/dt2bv_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 86717c807..e8763475b 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -112,7 +112,7 @@ class dt2bv_tactic : public tactic { unsigned idx = m_t.m_dt.get_constructor_idx(f); result = m_t.m_bv.mk_numeral(idx, bv_size); } - else { + else if (is_uninterp_const(a)) { // create a fresh variable, add bounds constraints for it. unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); result = m.mk_fresh_const(f->get_name().str().c_str(), m_t.m_bv.mk_sort(bv_size)); @@ -130,6 +130,9 @@ class dt2bv_tactic : public tactic { m_t.m_ext->insert(f, f_def); m_t.m_filter->insert(to_app(result)->get_decl()); } + else { + return false; + } m_cache.insert(a, result); ++m_t.m_num_translated; return true;