From 38823d6c79b121fca6e6392a2fb4e45ca74deea1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Apr 2013 08:16:02 -0700 Subject: [PATCH] [PDR] fix expansion of BV literals Signed-off-by: Nuno Lopes --- src/muz_qe/pdr_prop_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp index daa52992f..863e5c03e 100644 --- a/src/muz_qe/pdr_prop_solver.cpp +++ b/src/muz_qe/pdr_prop_solver.cpp @@ -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); }