summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r--src/parser/smt2/smt2.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ae0607b53..b693eae5b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -15,6 +15,9 @@
**/
#include "parser/smt2/smt2.h"
+#include <algorithm>
+
+#include "base/check.h"
#include "expr/type.h"
#include "options/options.h"
#include "parser/antlr_input.h"
@@ -23,8 +26,6 @@
#include "printer/sygus_print_callback.h"
#include "util/bitvector.h"
-#include <algorithm>
-
// ANTLR defines these, which is really bad!
#undef true
#undef false
@@ -303,6 +304,7 @@ void Smt2::addTheory(Theory theory) {
addOperator(kind::IS_INTEGER, "is_int");
addOperator(kind::TO_REAL, "to_real");
// falling through on purpose, to add Ints part of Reals_Ints
+ CVC4_FALLTHROUGH;
case THEORY_INTS:
defineType("Int", getExprManager()->integerType());
addArithmeticOperators();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback