More work on arithmetic single invocation synthesis conjectures.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4f1a5163e..0dd8b5f71 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -753,6 +753,10 @@ public:
     return d_theoryTable[theoryId];
   }
 
+  inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
+    return d_logicInfo.isTheoryEnabled(theoryId);
+  }
+  
   /**
    * Returns the equality status of the two terms, from the theory
    * that owns the domain type.  The types of a and b must be the same.