fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc#1062
fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc#1062
Conversation
src/solvers/miniBDD/miniBDD.cpp
Outdated
|
|
||
| bool mini_bdd_mgrt::reverse_keyt::operator<( | ||
| const mini_bdd_mgrt::reverse_keyt &other) const | ||
| bool operator < (const mini_bdd_mgrt::reverse_keyt &x, |
There was a problem hiding this comment.
bool operator<(
const mini_bdd_mgrt::reverse_keyt &x,
const mini_bdd_mgrt::reverse_keyt &y)
src/solvers/miniBDD/miniBDD.cpp
Outdated
| return false; | ||
|
|
||
| return high<other.high; | ||
| if(x.var<y.var) return true; |
There was a problem hiding this comment.
if(x.var<y.var)
return true;
etc
|
Do we have a test case that exhibits the problem? |
|
BDD2, BDD3 and BDD5 in `regression/ebmc` fail without this
…On 27 June 2017 at 11:10, Peter Schrammel ***@***.***> wrote:
Do we have a test case that exhibits the problem?
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#1062 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/ACeHTDrKwy7Um3k7GY0-SKckK2wOyqqNks5sIMcVgaJpZM4OF71x>
.
|
Are these now routinely run in some Travis set up? What about enabling/reviving |
tautschnig
left a comment
There was a problem hiding this comment.
Apart from various minor comments: there needs to be some convincing regression test story. If the regression test is run in some non-public repository then that's better than nothing, but really the regression test should live with the repository holding the source here.
| }; | ||
|
|
||
| friend bool operator<(const reverse_keyt &, const reverse_keyt &); | ||
|
|
There was a problem hiding this comment.
Why is this changed to a friend rather than being a member?
|
Apart from various minor comments: there needs to be some convincing regression test story. If the regression test is run in some non-public repository then that's better than nothing, but really the regression test should live with the repository holding the source here.
> };
+ friend bool operator<(const reverse_keyt &, const reverse_keyt &);
+
Why is this changed to a `friend` rather than being a member?
This is just the literal revert of the change that caused the
problem. It is very well possible to do the fix with a member function.
|
|
Michael Tautschnig <notifications@github.com> writes:
> BDD2, BDD3 and BDD5 in `regression/ebmc` fail without this
Are these now routinely run in some Travis set up?
not yet, but hopefully will be soon
|
I wasn't quite aware that I had broken this in 61f747d. Note to self: do not mix unrelated changes, because they will escape code review... |
201a53c to
cdc822b
Compare
|
Now uses a friend. |
|
The linter warnings are to be addressed; but adding some sort of test appears to be most important. |
7b73499 to
882dab6
Compare
|
An attempt has been made to add a test; the sad result is that this one gets stuck on the fixed variant as well, suggesting that there's still some bug, either in miniBDD, or in the test. |
|
Thank you for adding this test! How about reviving the previous unit test to see whether some very basic operations at least succeed? |
dd0e58d to
319fcca
Compare
|
Success! The test now passes on the fixed version, and fails on the previous one. |
|
Thank you for adding this test! Could the linter please be made happy or, where appropriate, be silenced? |
319fcca to
b65a006
Compare
b65a006 to
6b9fb16
Compare
|
Done. Note that this has required a change to util/invariant.h. |
6b9fb16 to
ff945b3
Compare
This fixes a segfault in ebmc -- this may even be worth a position in a whitepaper on test generation!