Fix preregistration in TheorySep before declare-heap (#5411)

Followup to fix for #5343. This catches cases where separation logic constraints are preregistered to TheorySep before the heap has been declared, which should also result in an error.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 2cd7aba91..9e96dccc3 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -100,6 +100,8 @@ class TheorySep : public Theory {
   /** finish initialization */
   void finishInit() override;
   //--------------------------------- end initialization
+  /** preregister term */
+  void preRegisterTerm(TNode n) override;
 
   std::string identify() const override { return std::string("TheorySep"); }
 
@@ -284,6 +286,11 @@ class TheorySep : public Theory {
   TypeNode getReferenceType( Node n );
   TypeNode getDataType( Node n );
   /**
+   * Register reference data types for atom. Calls the method below for
+   * the appropriate types.
+   */
+  void registerRefDataTypesAtom(Node atom);
+  /**
    * This is called either when:
    * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
    * (B) an atom specifying the heap type tn1/tn2 is registered to this theory.