mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 07:15:47 +00:00
Code Activity

trigger also parity constraints in linear case

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-06 05:18:50 -08:00
parent ef811a3dd8
commit fdba85e39f
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -643,8 +643,6 @@ namespace polysat {
signed_constraint a_is_odd, x_is_odd, b_is_odd;
if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
return false;
if (a.is_val())
return false;
if (!is_forced_odd(b, b_is_odd)) {
if (!is_forced_odd(a, a_is_odd))
return false;