summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/bv/bv_subtheory.h28
1 files changed, 12 insertions, 16 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index deb366a99..454f89b6c 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -37,26 +37,22 @@ enum SubTheory {
SUB_ALGEBRAIC = 4
};
-inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
+inline std::ostream& operator<<(std::ostream& out, SubTheory subtheory) {
switch (subtheory) {
- case SUB_BITBLAST:
- out << "BITBLASTER";
- break;
- case SUB_CORE:
- out << "BV_CORE_SUBTHEORY";
- break;
- case SUB_INEQUALITY:
- out << "BV_INEQUALITY_SUBTHEORY";
- case SUB_ALGEBRAIC:
- out << "BV_ALGEBRAIC_SUBTHEORY";
- default:
- Unreachable();
- break;
+ case SUB_BITBLAST:
+ return out << "BITBLASTER";
+ case SUB_CORE:
+ return out << "BV_CORE_SUBTHEORY";
+ case SUB_INEQUALITY:
+ return out << "BV_INEQUALITY_SUBTHEORY";
+ case SUB_ALGEBRAIC:
+ return out << "BV_ALGEBRAIC_SUBTHEORY";
+ default:
+ break;
}
- return out;
+ Unreachable();
}
-
// forward declaration
class TheoryBV;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback