Support for separation logic. Enable cbqi by default for pure BV.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 382d4cf65..e8518b1f6 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -781,6 +781,14 @@ public:
   assertions_iterator facts_end() const {
     return d_facts.end();
   }
+  /**
+   * Whether facts have been asserted to this theory.
+   *
+   * @return true iff facts have been asserted to this theory.
+   */
+  bool hasFacts() { 
+    return !d_facts.empty(); 
+  }
 
   typedef context::CDList<TNode>::const_iterator shared_terms_iterator;