Removing throw specifiers from OutputChannel and subclasses. (#1209)

1 files changed, 11 insertions, 9 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 892b331ea..402ba61ff 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -193,19 +193,21 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(
   return result;
 }
 
-bool TheoryEngine::EngineOutputChannel::propagate(TNode literal)
-  throw(AssertionException, UnsafeInterruptException) {
-  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
-  ++ d_statistics.propagations;
+bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) {
+  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
+                             << ">::propagate(" << literal << ")" << std::endl;
+  ++d_statistics.propagations;
   d_engine->d_outputChannelUsed = true;
   return d_engine->propagate(literal, d_theory);
 }
 
-void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
-  throw(AssertionException, UnsafeInterruptException) {
-  Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
-  Assert (pf == NULL); // Theory shouldn't be producing proofs yet
-  ++ d_statistics.conflicts;
+void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
+                                                 Proof* proof) {
+  Trace("theory::conflict")
+      << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
+      << ")" << std::endl;
+  Assert(!proof);  // Theory shouldn't be producing proofs yet
+  ++d_statistics.conflicts;
   d_engine->d_outputChannelUsed = true;
   d_engine->conflict(conflictNode, d_theory);
 }