mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix bv size

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-15 22:11:35 -07:00
parent 4e4346576a
commit bae4d54955
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/muz/ddnf/ddnf.cpp
View file

@ -738,7 +738,8 @@ namespace datalog {
VERIFY(m_expr2tbv.find(e, t));
var_ref w(m);
compile_var(v, w);
ddnf_nodes const& ns = m_ddnfs.lookup(0xFFFFF, *t);
unsigned num_bits = bv.get_bv_size(e);
ddnf_nodes const& ns = m_ddnfs.lookup(num_bits, *t);
ddnf_nodes::iterator it = ns.begin(), end = ns.end();
expr_ref_vector eqs(m);
sort* s = m.get_sort(w);