Minor improvements to theory model builder interface. (#2408)

1 files changed, 13 insertions, 5 deletions

diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 68e8c6b49..bff230b5c 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -68,13 +68,14 @@ class TheoryEngineModelBuilder : public ModelBuilder
    * are building fails to satisfy a quantified formula.
    */
   bool buildModel(Model* m) override;
-  /** Debug check model.
+
+  /** postprocess model
    *
-   * This throws an assertion failure if the model
-   * contains an equivalence class with two terms t1 and t2
-   * such that t1^M != t2^M.
+   * This is called when m is a model that will be returned to the user. This
+   * method checks the internal consistency of the model if we are in a debug
+   * build.
    */
-  void debugCheckModel(Model* m);
+  void postProcessModel(bool incomplete, Model* m);
 
  protected:
   /** pointer to theory engine */
@@ -102,6 +103,13 @@ class TheoryEngineModelBuilder : public ModelBuilder
   virtual void debugModel(TheoryModel* m) {}
   //-----------------------------------end virtual functions
 
+  /** Debug check model.
+   *
+   * This throws an assertion failure if the model contains an equivalence
+   * class with two terms t1 and t2 such that t1^M != t2^M.
+   */
+  void debugCheckModel(TheoryModel* m);
+
   /** is n assignable?
    *
    * A term n is assignable if its value