summaryrefslogtreecommitdiff
path: root/src/theory/output_channel.h
diff options
context:
space:
mode:
authorJordy Ruiz <jordy.ruiz@irit.fr>2015-05-22 10:36:23 +0200
committerJordy Ruiz <jordy.ruiz@irit.fr>2015-05-22 10:36:23 +0200
commitf713c6c9769bf810cddb8286e756e18bd2794a48 (patch)
tree4f93e2afc08a574ce5a2ebe1b07c8d43f4453e64 /src/theory/output_channel.h
parent520c5903a4c399b7c5beaa2d353bbf9324009ee7 (diff)
Added throw LogicException to method lemma.
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r--src/theory/output_channel.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index fdf253d3f..bef39f536 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -22,6 +22,7 @@
#include "util/cvc4_assert.h"
#include "theory/interrupted.h"
#include "util/resource_manager.h"
+#include "smt/logic_exception.h"
namespace CVC4 {
namespace theory {
@@ -120,7 +121,7 @@ public:
*/
virtual LemmaStatus lemma(TNode n, bool removable = false,
bool preprocess = false)
- throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
+ throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0;
/**
* Request a split on a new theory atom. This is equivalent to
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback