fixes for bug347

it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 5e4616628..5f49ab3ab 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -65,12 +65,12 @@ private:
       }
     }
 
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
       if (t1.getKind() == kind::CONST_BOOLEAN) {
-        return d_acm.propagate(t1.iffNode(t2));
+        d_acm.propagate(t1.iffNode(t2));
       } else {
-        return d_acm.propagate(t1.eqNode(t2));
+        d_acm.propagate(t1.eqNode(t2));
       }
     }
    };