Skip to content

Commit 201a53c

Browse files
author
Daniel Kroening
committed
fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc
1 parent e0b4515 commit 201a53c

File tree

2 files changed

+9
-10
lines changed

2 files changed

+9
-10
lines changed

src/solvers/miniBDD/miniBDD.cpp

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -339,15 +339,14 @@ mini_bddt mini_bdd_mgrt::mk(
339339
}
340340
}
341341

342-
bool mini_bdd_mgrt::reverse_keyt::operator<(
343-
const mini_bdd_mgrt::reverse_keyt &other) const
342+
bool operator < (const mini_bdd_mgrt::reverse_keyt &x,
343+
const mini_bdd_mgrt::reverse_keyt &y)
344344
{
345-
if(var<other.var || low<other.low)
346-
return true;
347-
if(var>other.var || low>other.low)
348-
return false;
349-
350-
return high<other.high;
345+
if(x.var<y.var) return true;
346+
if(x.var>y.var) return false;
347+
if(x.low<y.low) return true;
348+
if(x.low>y.low) return false;
349+
return x.high<y.high;
351350
}
352351

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

src/solvers/miniBDD/miniBDD.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -123,10 +123,10 @@ class mini_bdd_mgrt
123123
unsigned var, low, high;
124124
reverse_keyt(
125125
unsigned _var, const mini_bddt &_low, const mini_bddt &_high);
126-
127-
bool operator<(const reverse_keyt &other) const;
128126
};
129127

128+
friend bool operator<(const reverse_keyt &, const reverse_keyt &);
129+
130130
typedef std::map<reverse_keyt, mini_bdd_nodet *> reverse_mapt;
131131
reverse_mapt reverse_map;
132132

0 commit comments

Comments
 (0)