Fixed missing \ in uflra/Makefile.ma

Fixed another model bug and added previously failing fuzz testcase

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 92e04ed24..8358fe6c9 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -177,6 +177,9 @@ class TheoryArrays : public Theory {
   /** For debugging only- checks invariants about when things are preregistered*/
   context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
 
+  /** Helper for preRegisterTerm, also used internally */
+  void preRegisterTermInternal(TNode n, bool internalAssert = true);
+
   public:
 
   void preRegisterTerm(TNode n);
@@ -215,6 +218,8 @@ class TheoryArrays : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
   private:
+  /** Helper function for collectModelInfo */
+  void collectReads(TNode n, std::set<Node>& readSet, std::set<Node>& cache);
   public:
 
   void collectModelInfo( TheoryModel* m, bool fullModel );
@@ -331,6 +336,7 @@ class TheoryArrays : public Theory {
   context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
   context::CDO<bool> d_sharedTerms;
   context::CDList<TNode> d_reads;
+  context::CDList<TNode> d_readsInternal;
   std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
 
   // The decision requests we have for the core