diff options
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index d63bd252b..dc48da56f 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -49,13 +49,10 @@ Node SkolemCache::mkTypedSkolemCached( a = a.isNull() ? a : Rewriter::rewrite(a); b = b.isNull() ? b : Rewriter::rewrite(b); - if (d_skolemCachePreOnly[a][b].find(id) != d_skolemCachePreOnly[a][b].end()) - { - d_statistics.d_numCachedSkolemsPre += 1; - } - else + if (d_skolemCachePreOnly[a][b].find(id) == d_skolemCachePreOnly[a][b].end()) { d_skolemCachePreOnly[a][b][id] = Node::null(); + d_statistics.d_numCachedSkolemsPre += 1; } if (options::skolemSharing() && tn == d_strType) @@ -68,11 +65,11 @@ Node SkolemCache::mkTypedSkolemCached( { Node sk = mkTypedSkolem(tn, c); d_skolemCache[a][b][id] = sk; + d_statistics.d_numCachedSkolemsPost += 1; return sk; } else { - d_statistics.d_numCachedSkolemsPost += 1; d_statistics.d_numSkolems += 1; } return it->second; |