mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-17 17:14:51 -08:00
parent f7eb5f8840
commit f2149fb5a6
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/dd/dd_pdd.cpp
View file

@ -272,9 +272,7 @@ namespace dd {
// compute a*q*qc - b*p*pc
//
bool pdd_manager::try_spoly(pdd const& a, pdd const& b, pdd& r) {
if (!common_factors(a, b, m_p, m_q, m_pc, m_qc)) return false;
r = spoly(a, b, m_p, m_q, m_pc, m_qc);
return true;
return common_factors(a, b, m_p, m_q, m_pc, m_qc) && (r = spoly(a, b, m_p, m_q, m_pc, m_qc), true);
}
pdd pdd_manager::spoly(pdd const& a, pdd const& b, unsigned_vector const& p, unsigned_vector const& q, rational const& pc, rational const& qc) {