diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3e59aebe6..efc2eb3fe 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1752,7 +1752,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; } -void TheoryArrays::propagate(RowLemmaType lem) +void TheoryArrays::propagateLemma(RowLemmaType lem) { Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = " << options::arraysPropagate() << std::endl; @@ -1839,7 +1839,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // If propagating, check propagations int prop = options::arraysPropagate(); if (prop > 0) { - propagate(lem); + propagateLemma(lem); } // Prefer equality between indexes so as not to introduce new read terms @@ -1969,7 +1969,7 @@ bool TheoryArrays::dischargeLemmas() int prop = options::arraysPropagate(); if (prop > 0) { - propagate(l); + propagateLemma(l); if (d_state.isInConflict()) { return true; |