From 1f4b954a2cc7667a56a3007fa75c125fba93ed23 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Mar 2017 14:45:21 -0600
Subject: Eliminate Boolean term conversion. Generalizes removeITE pass to
 remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as
 theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

---
 src/printer/cvc/cvc_printer.cpp | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/printer/cvc/cvc_printer.cpp')

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index a9eab4a8c..01978b2e5 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -225,7 +225,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
 
     // BUILTIN
     case kind::EQUAL:
-      op << '=';
+      if( n[0].getType().isBoolean() ){
+        op << "<=>";
+      }else{
+        op << '=';
+      }
       opType = INFIX;
       break;
     case kind::ITE:
@@ -294,10 +298,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << "XOR";
       opType = INFIX;
       break;
-    case kind::IFF:
-      op << "<=>";
-      opType = INFIX;
-      break;
     case kind::IMPLIES:
       op << "=>";
       opType = INFIX;
-- 
cgit v1.2.3