Skip to content

Commit a71ca41

Browse files
author
Daniel Kroening
committed
disable linter for assertions
1 parent 564f64c commit a71ca41

File tree

1 file changed

+19
-0
lines changed

1 file changed

+19
-0
lines changed

src/solvers/miniBDD/miniBDD.cpp

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
2222

2323
void mini_bdd_nodet::remove_reference()
2424
{
25+
// NOLINTNEXTLINE(build/deprecated)
2526
assert(reference_counter!=0);
2627

2728
reference_counter--;
@@ -208,7 +209,9 @@ class mini_bdd_applyt
208209

209210
mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y)
210211
{
212+
// NOLINTNEXTLINE(build/deprecated)
211213
assert(x.is_initialized() && y.is_initialized());
214+
// NOLINTNEXTLINE(build/deprecated)
212215
assert(x.node->mgr==y.node->mgr);
213216

214217
// dynamic programming
@@ -270,7 +273,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
270273
auto &t=stack.top();
271274
const mini_bddt &x=t.x;
272275
const mini_bddt &y=t.y;
276+
// NOLINTNEXTLINE(build/deprecated)
273277
assert(x.is_initialized() && y.is_initialized());
278+
// NOLINTNEXTLINE(build/deprecated)
274279
assert(x.node->mgr==y.node->mgr);
275280

276281
switch(t.phase)
@@ -297,9 +302,13 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
297302
{
298303
t.var=x.var();
299304
t.phase=stack_elementt::phaset::FINISH;
305+
// NOLINTNEXTLINE(build/deprecated)
300306
assert(x.low().var()>t.var);
307+
// NOLINTNEXTLINE(build/deprecated)
301308
assert(y.low().var()>t.var);
309+
// NOLINTNEXTLINE(build/deprecated)
302310
assert(x.high().var()>t.var);
311+
// NOLINTNEXTLINE(build/deprecated)
303312
assert(y.high().var()>t.var);
304313
stack.push(stack_elementt(t.lr, x.low(), y.low()));
305314
stack.push(stack_elementt(t.hr, x.high(), y.high()));
@@ -308,7 +317,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
308317
{
309318
t.var=x.var();
310319
t.phase=stack_elementt::phaset::FINISH;
320+
// NOLINTNEXTLINE(build/deprecated)
311321
assert(x.low().var()>t.var);
322+
// NOLINTNEXTLINE(build/deprecated)
312323
assert(x.high().var()>t.var);
313324
stack.push(stack_elementt(t.lr, x.low(), y));
314325
stack.push(stack_elementt(t.hr, x.high(), y));
@@ -317,7 +328,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
317328
{
318329
t.var=y.var();
319330
t.phase=stack_elementt::phaset::FINISH;
331+
// NOLINTNEXTLINE(build/deprecated)
320332
assert(y.low().var()>t.var);
333+
// NOLINTNEXTLINE(build/deprecated)
321334
assert(y.high().var()>t.var);
322335
stack.push(stack_elementt(t.lr, x, y.low()));
323336
stack.push(stack_elementt(t.hr, x, y.high()));
@@ -337,6 +350,7 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
337350
}
338351
}
339352

353+
// NOLINTNEXTLINE(build/deprecated)
340354
assert(u.is_initialized());
341355

342356
return u;
@@ -364,6 +378,7 @@ mini_bddt mini_bddt::operator^(const mini_bddt &other) const
364378

365379
mini_bddt mini_bddt::operator!() const
366380
{
381+
// NOLINTNEXTLINE(build/deprecated)
367382
assert(is_initialized());
368383
return node->mgr->True()^*this;
369384
}
@@ -406,8 +421,11 @@ mini_bddt mini_bdd_mgrt::mk(
406421
const mini_bddt &low,
407422
const mini_bddt &high)
408423
{
424+
// NOLINTNEXTLINE(build/deprecated)
409425
assert(var<=var_table.size());
426+
// NOLINTNEXTLINE(build/deprecated)
410427
assert(low.var()>var);
428+
// NOLINTNEXTLINE(build/deprecated)
411429
assert(high.var()>var);
412430

413431
if(low.node_number()==high.node_number())
@@ -501,6 +519,7 @@ mini_bddt restrictt::RES(const mini_bddt &u)
501519
{
502520
// replace 'var' in 'u' by constant 'value'
503521

522+
// NOLINTNEXTLINE(build/deprecated)
504523
assert(u.is_initialized());
505524
mini_bdd_mgrt *mgr=u.node->mgr;
506525

0 commit comments

Comments
 (0)