summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/theory_quantifiers.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp11
1 files changed, 3 insertions, 8 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index f24a4bb2b..1682b4d0c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -16,8 +16,7 @@
#include "theory/quantifiers/theory_quantifiers.h"
-
-#include "base/cvc4_assert.h"
+#include "base/check.h"
#include "expr/kind.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/instantiation_engine.h"
@@ -147,15 +146,11 @@ void TheoryQuantifiers::check(Effort e) {
//do nothing
break;
case kind::INST_CLOSURE:
- default:
- Unhandled(assertion[0].getKind());
- break;
+ default: Unhandled() << assertion[0].getKind(); break;
}
}
break;
- default:
- Unhandled(assertion.getKind());
- break;
+ default: Unhandled() << assertion.getKind(); break;
}
}
// call the quantifiers engine to check
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback