From b96ca4eacc3c27b88a882e5ab7fcc64cf2c591c8 Mon Sep 17 00:00:00 2001
From: sjfink <sjfink@f5eafffb-2e1d-0410-98e4-8ec43c5233c4>
Date: Mon, 16 Jul 2007 17:06:15 +0000
Subject: [PATCH] bug fixes

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1488 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
---
 .../src/com/ibm/wala/logic/Disjunction.java   | 21 +++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
index 1a43ee547..e608cc8b5 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
@@ -110,17 +110,26 @@ public class Disjunction extends AbstractBinaryFormula implements IMaxTerm {
   public IFormula getF2() {
     Collection<? extends IFormula> c = HashSetFactory.make(clauses);
     c.remove(getF1());
-    return make(c);
+    if (c.size() == 1) {
+      return c.iterator().next();
+    } else {
+      return make(c);
+    }
   }
 
   public static Disjunction make(Collection<? extends IFormula> clauses) {
+    assert clauses.size() >= 2;
     Collection<IFormula> newClauses = HashSetFactory.make();
     for (IFormula c : clauses) {
-      assert !(c instanceof Disjunction);
-      if (Simplifier.isTautology(c)) {
-        return make(BooleanConstantFormula.TRUE);
-      } else if (!Simplifier.isContradiction(c)) {
-        newClauses.add(c);
+      if (c instanceof Disjunction) {
+        Disjunction d = (Disjunction) c;
+        newClauses.addAll(d.clauses);
+      } else {
+        if (Simplifier.isTautology(c)) {
+          return make(BooleanConstantFormula.TRUE);
+        } else if (!Simplifier.isContradiction(c)) {
+          newClauses.add(c);
+        }
       }
     }
     if (newClauses.isEmpty()) {