1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 231d0ee9e..e5154476a 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -83,10 +83,15 @@ public:
 };/* class TermArgTrie */
 
 
+namespace fmcheck {
+  class FullModelChecker;
+}
+
 class TermDb {
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class ::CVC4::theory::inst::Trigger;
   friend class ::CVC4::theory::rrinst::Trigger;
+  friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;