summaryrefslogtreecommitdiff
path: root/src/theory/arrays/theory_arrays.cpp
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2015-03-25 15:04:10 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2015-03-25 15:04:10 -0400
commitde819295a17aafec36455cde1b4c912951b49273 (patch)
tree90b96607ebd6c0448c5145698dafdcc049607b8b /src/theory/arrays/theory_arrays.cpp
parent973cbd67611a2943714fd9544d098ec1472a40b8 (diff)
change const are triggers from false to true in equality engines
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r--src/theory/arrays/theory_arrays.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 94f3f573e..c770fb7ae 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -61,15 +61,15 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
- d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , false),
+ d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
d_ppFacts(u),
// d_ppCache(u),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
d_isPreRegistered(c),
- d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", false),
+ d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", false),
+ d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
d_conflict(c, false),
d_backtracker(c),
d_infoMap(c, &d_backtracker),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback