summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/theory_arrays.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index c0777f79f..f66f3f7a4 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -684,6 +684,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
TNode n = arrays[i];
// Compute default value for this array - there is one default value for every mayEqual equivalence class
+ d_mayEqualEqualityEngine.addTerm(n); // add the term in case it isn't there already
TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(n);
it = defValues.find(mayRep);
// If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback