summaryrefslogtreecommitdiff
path: root/src/preprocessing/util
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-03-15 20:58:57 +0100
committerGitHub <noreply@github.com>2021-03-15 19:58:57 +0000
commit429514c9cb6d187adca027ffc7542cf35543e85d (patch)
tree9d9aab55577496739577036c5cc582598d395679 /src/preprocessing/util
parent5bbb45b820b9d695c29182f4dd2fc13fd9997e4b (diff)
Replace HistogramStat by IntegralHistogramStat (#6126)
This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
Diffstat (limited to 'src/preprocessing/util')
-rw-r--r--src/preprocessing/util/ite_utilities.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index 856e3be58..90c240478 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -306,7 +306,7 @@ class ITESimplifier
IntStat d_specialEqualityFolds;
IntStat d_simpITEVisits;
- HistogramStat<uint32_t> d_inSmaller;
+ IntegralHistogramStat<uint32_t> d_inSmaller;
Statistics();
~Statistics();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback