Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.

1 files changed, 2 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 386b8bbd4..e36d163a4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -668,6 +668,8 @@ void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuil
       TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
       if (atom.getKind() == kind::EQUAL) {
         explainEquality(theoryId, literal, builder);
+      } else if(literal.getKind() == kind::AND){
+        explainEqualities(theoryId, literal, builder);
       } else {
         builder << literal;
       }