mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 22:33:40 +00:00
Code Activity

Fixed assignment bug for shifts/band

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-11-21 16:40:28 +01:00
parent 0341851958
commit b116d5ac9e
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/constraint_manager.cpp
View file

@ -324,7 +324,7 @@ namespace polysat {
pdd r = m.mk_var(s.add_var(sz)); pdd r = m.mk_var(s.add_var(sz));
m_dedup.op_constraint_expr.insert(args, r.var()); m_dedup.op_constraint_expr.insert(args, r.var());
s.assign_eh(mk_op_constraint(op, p, q, r), null_dependency); s.add_clause(mk_op_constraint(op, p, q, r), false);
return r; return r;
} }