summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-07-21 09:19:31 -0500
committerGitHub <noreply@github.com>2018-07-21 09:19:31 -0500
commit0d12fcbb5f1c047f951a69aa6ef4ae127f499312 (patch)
treed177dd93a13a8ae4ac5c9a22ab8c5aa97537d19d /src/util
parent585d2ac394e99a155ed40aa2da2fb550ff60fc7b (diff)
Optimizations and fixes for computing whether a type is finite (#2179)
Diffstat (limited to 'src/util')
-rw-r--r--src/util/cardinality.h3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index b45f6bcc2..956468e30 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -135,8 +135,7 @@ class CVC4_PUBLIC Cardinality {
/** Returns true iff this cardinality is finite. */
bool isFinite() const { return d_card > 0; }
/** Returns true iff this cardinality is one */
- bool isOne() const { return d_card == 1; }
-
+ bool isOne() const { return d_card == 2; }
/**
* Returns true iff this cardinality is finite and large (i.e.,
* at the ceiling of representable finite cardinalities).
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback