Three things:

1. Infrastructure for unit T-conflicts added to SAT proxy
   (and also the theory output channel documentation);
   previously theories could not communicate unit T-conflicts
   with the SAT layer because that layer had an implicit
   assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true".  These could
   conceivably occur in artificial benchmarks in this form:
     (let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 744a3d966..ee88df126 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -51,6 +51,11 @@ public:
   }
 
   static RewriteResponse preRewrite(TNode node) {
+    if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+      if(node[0] == node[1]) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+      }
+    }
     return RewriteResponse(REWRITE_DONE, node);
   }