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

bugfix?

Browse source
This commit is contained in:
Jakob Rath 2024-01-29 16:51:10 +01:00
parent 75527e8e19
commit 8de2503f9f
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/polysat/monomials.cpp
View file

@ -180,7 +180,7 @@ namespace polysat {
pdd qs = c.value(rational(1), mon.num_bits());
for (unsigned k = mon.size(); k-- > 0; )
if (k != j)
qs *= mon.arg_vals[k];
qs *= mon.args[k];
c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), C.eq(qs, 1), C.eq(p) }, true);
return true;
}