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, 15 insertions, 7 deletions

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 40c17e016..f34699e2b 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -28,6 +28,7 @@ namespace CVC4 {
 namespace prop {
 
 void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) {
+  Assert(conflict.size() == 0);
   // Try theory propagation
   bool ok = d_theoryEngine->check(effort);
   // If in conflict construct the conflict clause
@@ -35,15 +36,22 @@ void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict)
     // We have a conflict, get it
     Node conflictNode = d_theoryEngine->getConflict();
     Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
-    // Go through the literals and construct the conflict clause
-    Node::const_iterator literal_it = conflictNode.begin();
-    Node::const_iterator literal_end = conflictNode.end();
-    while (literal_it != literal_end) {
+    if(conflictNode.getKind() == kind::AND) {
+      // Go through the literals and construct the conflict clause
+      Node::const_iterator literal_it = conflictNode.begin();
+      Node::const_iterator literal_end = conflictNode.end();
+      while (literal_it != literal_end) {
+        // Get the literal corresponding to the node
+        SatLiteral l = d_cnfStream->getLiteral(*literal_it);
+        // Add the negation to the conflict clause and continue
+        conflict.push(~l);
+        literal_it ++;
+      }
+    } else { // unit conflict
       // Get the literal corresponding to the node
-      SatLiteral l = d_cnfStream->getLiteral(*literal_it);
-      // Add the negation to the conflict clause and continue
+      SatLiteral l = d_cnfStream->getLiteral(conflictNode);
+      // construct the unit conflict clause
       conflict.push(~l);
-      literal_it ++;
     }
   }
 }