From 94dfcfbb9ac7bb3223c4c950038aa9f6d02cccb8 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 28 Feb 2022 18:19:02 -0800
Subject: [PATCH] Remove unused data members from `TheoryArrays` (#8197)

---
 src/theory/arrays/theory_arrays.cpp | 12 ------------
 src/theory/arrays/theory_arrays.h   |  4 ----
 2 files changed, 16 deletions(-)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 5a0e8f597..d7f36cde1 100644
--- 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 7c7058049..636d7e8f5 100644
--- 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.
-- 
2.30.2