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, 1 insertions, 2 deletions

diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 1a38d7332..fccd2e6bc 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -92,9 +92,8 @@ private:
       return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
     }
 
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       d_sharedTerms.conflict(t1, t2, true);
-      return false;
     }
   };