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

2 files changed, 3 insertions, 2 deletions

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 1de3854b9..34536445f 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -57,9 +57,10 @@ public:
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n)
+  bool propagate(TNode n)
     throw(AssertionException) {
     push(PROPAGATE, n);
+    return true;
   }
 
   void propagateAsDecision(TNode n)
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index ff6cba936..2d6730949 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -51,7 +51,7 @@ class FakeOutputChannel : public OutputChannel {
   void conflict(TNode n) throw(AssertionException) {
     Unimplemented();
   }
-  void propagate(TNode n) throw(AssertionException) {
+  bool propagate(TNode n) throw(AssertionException) {
     Unimplemented();
   }
   void propagateAsDecision(TNode n) throw(AssertionException) {