From 48d20142488fbd644b1be53f42d30517adc59f6f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 27 Nov 2016 00:00:04 +0000 Subject: Fix bug in implementation of `NotExpr`. It should not implement `compareContents()`. This bug would not have affected correctness but it would have affected performance because if `Expr::compare()` was called on two structually equal `NotExpr` then its children would be checked for structually equality twice - once in NotExpr::compareContents()` and once in `Expr::compare()`. This partially addresses #515 . --- include/klee/Expr.h | 6 ------ 1 file changed, 6 deletions(-) (limited to 'include') diff --git a/include/klee/Expr.h b/include/klee/Expr.h index d70cfdc9..500d7d46 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -765,12 +765,6 @@ public: unsigned getNumKids() const { return numKids; } ref getKid(unsigned i) const { return expr; } - int compareContents(const Expr &b) const { - const NotExpr &eb = static_cast(b); - if (expr != eb.expr) return expr < eb.expr ? -1 : 1; - return 0; - } - virtual ref rebuild(ref kids[]) const { return create(kids[0]); } -- cgit 1.4.1