From: Jordy Ruiz <jordy.ruiz@irit.fr>
Date: Fri, 22 May 2015 08:36:23 +0000 (+0200)
Subject: Added throw LogicException to method lemma.
X-Git-Tag: cvc5-1.0.0~6322^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f713c6c9769bf810cddb8286e756e18bd2794a48;p=cvc5.git

Added throw LogicException to method lemma.
---

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
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0dd8b5f71..8aedc65f0 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -303,7 +303,7 @@ class TheoryEngine {
       return d_engine->propagate(literal, d_theory);
     }
 
-    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;