mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

fix dt2bv transformation to only work with constants, issue #725

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-08-30 11:42:14 +08:00
parent 882c3bd0cd
commit d4539b8887
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/bv/dt2bv_tactic.cpp
View file

@ -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;