mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 15:13:23 +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:13:56 -07:00
parent bae4d54955
commit 31c7f79afd
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -735,10 +735,11 @@ namespace datalog {
void compile_eq(expr* e, expr_ref& result, var* v, unsigned hi, unsigned lo, expr* c) { void compile_eq(expr* e, expr_ref& result, var* v, unsigned hi, unsigned lo, expr* c) {
tbv* t; tbv* t;
// TBD: hi, lo are ignored.
VERIFY(m_expr2tbv.find(e, t)); VERIFY(m_expr2tbv.find(e, t));
var_ref w(m); var_ref w(m);
compile_var(v, w); compile_var(v, w);
unsigned num_bits = bv.get_bv_size(e); unsigned num_bits = bv.get_bv_size(c);
ddnf_nodes const& ns = m_ddnfs.lookup(num_bits, *t); ddnf_nodes const& ns = m_ddnfs.lookup(num_bits, *t);
ddnf_nodes::iterator it = ns.begin(), end = ns.end(); ddnf_nodes::iterator it = ns.begin(), end = ns.end();
expr_ref_vector eqs(m); expr_ref_vector eqs(m);