From bdc7bfde875a53fcc782bc71bd26610013c2c04d Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Fri, 4 Apr 2014 13:10:18 -0700
Subject: [PATCH] duality quantifier simplification fix

---
 src/duality/duality_rpfp.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 8040310ec..ef37dd8a2 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -561,7 +561,7 @@ namespace Duality {
       }
       decl_kind op = is_forall ? Or : And;
       if(free.empty())
-	return SimplifyAndOr(not_free,op == And);
+	return DeleteBound(0,1,SimplifyAndOr(not_free,op == And));
       expr q = clone_quantifier(is_forall ? Forall : Exists,t, SimplifyAndOr(free, op == And));
       if(!not_free.empty())
 	q = ctx.make(op,q,DeleteBound(0,1,SimplifyAndOr(not_free, op == And)));