From 0a83ae67bff3fe12f2fff295fddc82fb2f73032f Mon Sep 17 00:00:00 2001
From: katelman <katelman@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 27 Apr 2009 20:30:16 +0000
Subject: [PATCH] IMPORTANT:

STP appears to be failing about half of the regressions in stp-tests/test. I
have just noticed this an made no attempt to fix it. I suspect it is due to
recent changes, as my personal branch 02_07_2009 does not have the same
problem.

OTHER:

I fixed a CNF conversion memory bug. IMPLIES and ITE cases were not setting the
sibling rename flag correctly, well, at all.


git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@71 e59a4935-1847-0410-ae03-e826735625c1
---
 AST/ToCNF.cpp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/AST/ToCNF.cpp b/AST/ToCNF.cpp
index 59d2d21..d66a7d0 100644
--- a/AST/ToCNF.cpp
+++ b/AST/ToCNF.cpp
@@ -1061,6 +1061,9 @@ private:
       CNFInfo* x0 = info[varphi[0]];
       CNFInfo* x1 = info[varphi[1]];
       convertFormulaToCNF(varphi[0], defs);
+      if(x0->clausesneg->size() > 1){
+         setDoSibRenamingPos(*x1);
+      }
       convertFormulaToCNF(varphi[1], defs);
       BeevMgr::ClauseList* psi = 
          PRODUCT(*(x0->clausesneg), *(x1->clausespos));
@@ -1078,7 +1081,13 @@ private:
       CNFInfo* x1 = info[varphi[1]];
       CNFInfo* x2 = info[varphi[2]];
       convertFormulaToCNF(varphi[0], defs);
+      if(x0->clausesneg->size() > 1){
+         setDoSibRenamingPos(*x1);
+      }
       convertFormulaToCNF(varphi[1], defs);
+      if(x0->clausespos->size() > 1){
+         setDoSibRenamingPos(*x2);
+      }
       convertFormulaToCNF(varphi[2], defs);
       BeevMgr::ClauseList* psi1 = PRODUCT(*(x0->clausesneg)
          , *(x1->clausespos));
@@ -1335,7 +1344,13 @@ private:
       CNFInfo* x1 = info[varphi[1]];
       CNFInfo* x2 = info[varphi[2]];
       convertFormulaToCNF(varphi[0], defs);
+      if(x0->clausesneg->size() > 1){
+         setDoSibRenamingNeg(*x1);
+      }
       convertFormulaToCNF(varphi[1], defs);
+      if(x0->clausespos->size() > 1){
+         setDoSibRenamingNeg(*x2);
+      }
       convertFormulaToCNF(varphi[2], defs);
       BeevMgr::ClauseList* psi1 = PRODUCT(*(x0->clausesneg)
          , *(x1->clausesneg));
-- 
2.47.3