Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.

http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5

1 files changed, 6 insertions, 6 deletions

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d17caba45..6592e86cf 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -261,11 +261,8 @@ class TheoryArrays : public Theory {
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      if (Theory::theoryOf(t1) == THEORY_BOOL) {
-        return d_arrays.propagate(t1.iffNode(t2));
-      } else {
-        return d_arrays.propagate(t1.eqNode(t2));
-      }
+      d_arrays.conflict(t1, t2);
+      return false;
     }
   };
 
@@ -275,9 +272,12 @@ class TheoryArrays : public Theory {
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
 
-  // Are we in conflict?
+  /** Are we in conflict? */
   context::CDO<bool> d_conflict;
 
+  /** Conflict when merging constants */
+  void conflict(TNode a, TNode b);
+
   /** The conflict node */
   Node d_conflictNode;