Skip to content

Commit 439ef97

Browse files
author
Daniel Kroening
committed
fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc
1 parent 8e70eaa commit 439ef97

File tree

2 files changed

+12
-6
lines changed

2 files changed

+12
-6
lines changed

src/solvers/miniBDD/miniBDD.cpp

+11-5
Original file line numberDiff line numberDiff line change
@@ -463,14 +463,20 @@ mini_bddt mini_bdd_mgrt::mk(
463463
}
464464

465465
bool mini_bdd_mgrt::reverse_keyt::operator<(
466-
const mini_bdd_mgrt::reverse_keyt &other) const
466+
const mini_bdd_mgrt::reverse_keyt &y) const
467467
{
468-
if(var<other.var || low<other.low)
468+
const reverse_keyt &x=*this;
469+
470+
if(x.var<y.var)
469471
return true;
470-
if(var>other.var || low>other.low)
472+
else if(x.var>y.var)
471473
return false;
472-
473-
return high<other.high;
474+
else if(x.low<y.low)
475+
return true;
476+
else if(x.low>y.low)
477+
return false;
478+
else
479+
return x.high<y.high;
474480
}
475481

476482
void mini_bdd_mgrt::DumpTable(std::ostream &out) const

src/solvers/miniBDD/miniBDD.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ class mini_bdd_mgrt
124124
reverse_keyt(
125125
unsigned _var, const mini_bddt &_low, const mini_bddt &_high);
126126

127-
bool operator<(const reverse_keyt &other) const;
127+
bool operator<(const reverse_keyt &) const;
128128
};
129129

130130
typedef std::map<reverse_keyt, mini_bdd_nodet *> reverse_mapt;

0 commit comments

Comments
 (0)