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

[PDR] fix expansion of BV literals

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-04-16 08:16:02 -07:00
parent 1f5097cdaa
commit 38823d6c79
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz_qe/pdr_prop_solver.cpp
View file

@ -145,7 +145,8 @@ namespace pdr {
rational two(2);
for (unsigned j = 0; j < bv_size; ++j) {
parameter p(j);
expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
//expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c));
if ((r % two).is_zero()) {
e = m.mk_not(e);
}