summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extraBddMisc.c3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 7d63980a..0bc4a8c5 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1707,9 +1707,6 @@ cuddBddPermuteRecur( DdManager * manager /* DD manager */ ,
/* If problem already solved, look up answer and return. */
if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL )
{
-#ifdef DD_DEBUG
- bddPermuteRecurHits++;
-#endif
return ( Cudd_NotCond( res, N != node ) );
}