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

fix nightly, fix regression identified by Nuno

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-28 18:03:15 -07:00
parent b8532bec7e
commit 6abea2de2c
2 changed files with 25 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2719,6 +2719,23 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) {
if (m_mkbv2num) {
unsigned i;
for (i = 0; i < num; i++)
if (!m().is_true(args[i]) && !m().is_false(args[i]))
return BR_FAILED;
numeral val;
numeral two(2);
i = num;
while (i > 0) {
--i;
val *= two;
if (m().is_true(args[i]))
val++;
}
result = mk_numeral(val, num);
return BR_DONE;
}
return BR_FAILED;
}