From fc7bebbc12a38260b35442d7f9fe2da83d2525f1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 10 Jul 2010 21:52:59 +0000
Subject: cnf bugfix for SMT2 ???

---
 src/prop/cnf_stream.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9136a73c3..e95322348 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -364,6 +364,13 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     case AND:
       nodeLit = handleAnd(node);
       break;
+    case EQUAL:
+      if(node[0].getType().isBoolean() && node[1].getType().isBoolean()) {
+        nodeLit = handleIff(node[0].iffNode(node[1]));
+      } else {
+        nodeLit = convertAtom(node);
+      }
+      break;
     default:
       {
         //TODO make sure this does not contain any boolean substructure
-- 
cgit v1.2.3