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

compile

Browse source
This commit is contained in:
Jakob Rath 2023-02-01 16:44:52 +01:00
parent 53bbb49031
commit 845f5f89e1
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/bv_polysat.cpp
View file

@ -147,7 +147,7 @@ namespace bv {
for (expr* arg : *a) { for (expr* arg : *a) {
expr_ref b2b(m); expr_ref b2b(m);
b2b = bv.mk_bit2bool(a, i); b2b = bv.mk_bit2bool(a, i);
sat::literal bit_i = ctx.internalize(b2b, false, false, m_is_redundant); sat::literal bit_i = ctx.internalize(b2b, false, false);
sat::literal lit = expr2literal(arg); sat::literal lit = expr2literal(arg);
add_equiv(lit, bit_i); add_equiv(lit, bit_i);
ctx.add_aux_equiv(lit, bit_i); ctx.add_aux_equiv(lit, bit_i);