mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 05:29:28 +00:00
Code Activity

Remove unused variable in polynomial.cpp

Browse source 
Removed unused variable 'sz2' in polynomial multiplication.
This commit is contained in:
Nikolaj Bjorner 2025-09-15 10:43:09 -07:00 • committed by GitHub
parent b0bc41457f
commit 6752be7263
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polynomial/polynomial.cpp
View file

@ -3016,7 +3016,6 @@ namespace polynomial {
} }
m_som_buffer.reset(); m_som_buffer.reset();
unsigned sz1 = p1->size(); unsigned sz1 = p1->size();
unsigned sz2 = p2->size();
for (unsigned i = 0; i < sz1; i++) { for (unsigned i = 0; i < sz1; i++) {
checkpoint(); checkpoint();
numeral const & a1 = p1->a(i); numeral const & a1 = p1->a(i);
@ -3026,6 +3025,7 @@ namespace polynomial {
m_som_buffer.add(a); m_som_buffer.add(a);
auto p = m_som_buffer.mk(); auto p = m_som_buffer.mk();
#if 0 #if 0
unsigned sz2 = p2->size();
if (sz1 > 2 && sz2 > 2) { if (sz1 > 2 && sz2 > 2) {
auto s1 = sw.get_seconds(); auto s1 = sw.get_seconds();
IF_VERBOSE(0, verbose_stream() << "polynomial muladd time: " << sz1 << " " << sz2 << " " << s1 << "\n"); IF_VERBOSE(0, verbose_stream() << "polynomial muladd time: " << sz1 << " " << sz2 << " " << s1 << "\n");