summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.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/theory_engine.h
parent520c5903a4c399b7c5beaa2d353bbf9324009ee7 (diff)
Added throw LogicException to method lemma.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h2
1 files changed, 1 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback