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

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index b25bf503d..a9722690b 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -72,7 +72,9 @@ public:
    * @param n - a conflict at the current decision level.  This should
    * be an AND-kinded node of literals that are TRUE in the current
    * assignment and are in conflict (i.e., at least one must be
-   * assigned false).
+   * assigned false), or else a literal by itself (in the case of a
+   * unit conflict) which is assigned TRUE (and T-conflicting) in the
+   * current assignment.
    *
    * @param safe - whether it is safe to be interrupted
    */