1 files changed, 12 insertions, 18 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index c98c36f13..9af564a05 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1609,7 +1609,7 @@ void TheoryArrays::setNonLinear(TNode a)
       Assert(store.getKind() == kind::STORE);
       TNode j = store[1];
       TNode c = store[0];
-      lem = make_quad(store, c, j, i);
+      lem = std::make_tuple(store, c, j, i);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(lem);
     }
@@ -1836,7 +1836,7 @@ void TheoryArrays::checkStore(TNode a) {
     for(; it < js->size(); ++it) {
       TNode j = (*js)[it];
       if (i == j) continue;
-      lem = make_quad(a,b,i,j);
+      lem = std::make_tuple(a, b, i, j);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
       queueRowLemma(lem);
     }
@@ -1877,7 +1877,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     Assert(store.getKind()==kind::STORE);
     TNode j = store[1];
     if (i == j) continue;
-    lem = make_quad(store, store[0], j, i);
+    lem = std::make_tuple(store, store[0], j, i);
     Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
     queueRowLemma(lem);
   }
@@ -1889,7 +1889,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
       Assert(instore.getKind()==kind::STORE);
       TNode j = instore[1];
       if (i == j) continue;
-      lem = make_quad(instore, instore[0], j, i);
+      lem = std::make_tuple(instore, instore[0], j, i);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(lem);
     }
@@ -1936,7 +1936,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
       Assert(store.getKind() == kind::STORE);
       TNode j = store[1];
       TNode c = store[0];
-      lem = make_quad(store, c, j, i);
+      lem = std::make_tuple(store, c, j, i);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(lem);
     }
@@ -1951,7 +1951,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
         Assert(store.getKind() == kind::STORE);
         TNode j = store[1];
         TNode c = store[0];
-        lem = make_quad(store, c, j, i);
+        lem = std::make_tuple(store, c, j, i);
         Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
         queueRowLemma(lem);
       }
@@ -1965,10 +1965,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
   Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
                      << options::arraysPropagate() << std::endl;
 
-  TNode a = lem.first;
-  TNode b = lem.second;
-  TNode i = lem.third;
-  TNode j = lem.fourth;
+  TNode a, b, i, j;
+  std::tie(a, b, i, j) = lem;
 
   Assert(a.getType().isArray() && b.getType().isArray());
   if (d_equalityEngine.areEqual(a,b) ||
@@ -2024,10 +2022,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
     return;
   }
-  TNode a = lem.first;
-  TNode b = lem.second;
-  TNode i = lem.third;
-  TNode j = lem.fourth;
+  TNode a, b, i, j;
+  std::tie(a, b, i, j) = lem;
 
   Assert(a.getType().isArray() && b.getType().isArray());
   if (d_equalityEngine.areEqual(a,b) ||
@@ -2156,10 +2152,8 @@ bool TheoryArrays::dischargeLemmas()
       continue;
     }
 
-    TNode a = l.first;
-    TNode b = l.second;
-    TNode i = l.third;
-    TNode j = l.fourth;
+    TNode a, b, i, j;
+    std::tie(a, b, i, j) = l;
     Assert(a.getType().isArray() && b.getType().isArray());
 
     NodeManager* nm = NodeManager::currentNM();