Remove unused data members from `TheoryArrays` (#8197)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 5a0e8f597ecbcab909108d7cedf61a85555b3c0c..d7f36cde1d4929ce5f604cf70f0e04c844b586c6 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -107,7 +107,6 @@ TheoryArrays::TheoryArrays(Env& env,
       d_defValues(context()),
       d_readTableContext(new context::Context()),
       d_arrayMerges(context()),
-      d_inCheckModel(false),
       d_dstrat(new TheoryArraysDecisionStrategy(this)),
       d_dstratInit(false)
 {
@@ -412,11 +411,6 @@ bool TheoryArrays::propagateLit(TNode literal)
     return false;
   }
 
-  // Propagate away
-  if (d_inCheckModel && context()->getLevel() != d_topLevel)
-  {
-    return true;
-  }
   bool ok = d_out->propagate(literal);
   if (!ok) {
     d_state.notifyInConflict();
@@ -2122,12 +2116,6 @@ bool TheoryArrays::dischargeLemmas()
 
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
-  if (d_inCheckModel)
-  {
-    // if in check model, don't send the conflict
-    d_state.notifyInConflict();
-    return;
-  }
   d_im.conflictEqConstantMerge(a, b);
 }
 

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7c705804908d95782a8bd01c3e7035151c093de8..636d7e8f5a6560e2e1768e3b0a0d4aefa82027b5 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -445,10 +445,6 @@ class TheoryArrays : public Theory {
   void queueRowLemma(RowLemmaType lem);
   bool dischargeLemmas();
 
-  std::vector<Node> d_decisions;
-  bool d_inCheckModel;
-  int d_topLevel;
-
   /**
    * The decision strategy for the theory of arrays, which calls the
    * getNextDecisionEngineRequest function below.