summaryrefslogtreecommitdiff
path: root/src/compat/cvc3_compat.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-06-21 21:12:36 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-06-21 23:41:54 -0400
commitbc7b92859698a0b23aa20dc8811be8bbe84e164e (patch)
treeda4060830ba94f71683aa4f5852924097fd19b59 /src/compat/cvc3_compat.cpp
parent4ba5382a32cb80aacbff11178f0da7b6493c8d48 (diff)
Fix compiler warnings (mostly unused variables).
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r--src/compat/cvc3_compat.cpp5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index b4ab57283..37d4c503d 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -416,6 +416,8 @@ bool Expr::isAtomicFormula() const {
case CVC4::kind::IFF:
case CVC4::kind::IMPLIES:
return false;
+ default:
+ ; /* fall through */
}
for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
if (!CVC3::Expr(*k).isAtomic()) {
@@ -450,8 +452,9 @@ bool Expr::isBoolConnective() const {
case CVC4::kind::XOR:
case CVC4::kind::ITE:
return true;
+ default:
+ return false;
}
- return false;
}
bool Expr::isPropLiteral() const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback