1 files changed, 0 insertions, 28 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ac06d266d..a834ca300 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -749,34 +749,6 @@ bool TheoryEngine::presolve() {
   return false;
 }/* TheoryEngine::presolve() */
 
-void TheoryEngine::postsolve() {
-  // no longer in SAT mode
-  d_inSatMode = false;
-  // Reset the interrupt flag
-  d_interrupted = false;
-  bool CVC4_UNUSED wasInConflict = d_inConflict;
-
-  try {
-    // Definition of the statement that is to be run by every theory
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)    \
-  if (theory::TheoryTraits<THEORY>::hasPostsolve) \
-  {                                               \
-    theoryOf(THEORY)->postsolve();                \
-    Assert(!d_inConflict || wasInConflict)        \
-        << "conflict raised during postsolve()";  \
-  }
-
-    // Postsolve for each theory using the statement above
-    CVC4_FOR_EACH_THEORY;
-  } catch(const theory::Interrupted&) {
-    Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl;
-  }
-}/* TheoryEngine::postsolve() */
-
-
 void TheoryEngine::notifyRestart() {
   // Reset the interrupt flag
   d_interrupted = false;