Bug in BitBlaster

[Stephan Falke]

Hi,

It seems that some of the current changes to BitBlaster.cpp have
introduced two problems:

1) BitBlaster.cpp does not compile on my machine since a loop counter
declared on line 1247 is used outside its loop.
2) If the declaration of the loop counter is moved outside the loop,
than a segmentation fault occurs in line 1255.

The attached patch fixes these problems (assuming my understanding of
the code is correct...)

Kind regards,
Stephan

Index: src/to-sat/BitBlaster.cpp
===================================================================
--- src/to-sat/BitBlaster.cpp (revision 1481)
+++ src/to-sat/BitBlaster.cpp (working copy)
@@ -1252,7 +1252,7 @@
assert(products[i].size() == 1);
results.push_back(products[i].back());
}
- assert(products[i+1].size() ==0); // i+1 is defined but should
never be used.
+ assert(products[bitWidth].size() == 0); // is defined but should
never be used.

assert(results.size() == ((unsigned)bitWidth));
return results;

[Trevor Hansen]

Hi Stephan,

> It seems that some of the current changes to BitBlaster.cpp have
> introduced two problems:

Thanks for the bug report, this was fixed in revision 1482.

Thanks!

Trevor