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

fix lemma

Browse source
This commit is contained in:
Jakob Rath 2023-03-11 10:36:25 +01:00
parent f2ff1145bd
commit 592b206097
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/op_constraint.cpp
View file

@ -545,7 +545,7 @@ namespace polysat {
// p != 0 ==> odd(r) // p != 0 ==> odd(r)
if (parity_rv != 0) if (parity_rv != 0)
return s.mk_clause("r = inv p & p != 0 ==> odd(r)", {~invc, ~s.eq(p()), s.odd(r())}, true); return s.mk_clause("r = inv p & p != 0 ==> odd(r)", {~invc, s.eq(p()), s.odd(r())}, true);
pdd prod = p() * r(); pdd prod = p() * r();
rational prodv = (pv * rv).val(); rational prodv = (pv * rv).val();