From: Tim King <taking@cs.nyu.edu>
Date: Sat, 10 Nov 2012 23:55:34 +0000 (+0000)
Subject: Fix to quantifier rewritting not being idempotent. See bug 441.
X-Git-Tag: cvc5-1.0.0~7621
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ed555a82d64772dcbac7772e0770c9015b11a8e8;p=cvc5.git

Fix to quantifier rewritting not being idempotent. See bug 441.
---

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 063875235..d25e516fe 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -224,8 +224,12 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
         InstConstantAttribute ica;
         n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
       }
+
+      // This is required if substitute in computePrenex() is used.
+      return RewriteResponse(REWRITE_AGAIN_FULL, n );
+    }else{
+      return RewriteResponse(REWRITE_DONE, n );
     }
-    return RewriteResponse(REWRITE_DONE, n );
   }
   return RewriteResponse(REWRITE_DONE, in);
 }
@@ -493,6 +497,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       }
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+      Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl;
       return newBody;
     }else{
       return body;