From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Mar 2020 15:57:00 +0000 (-0500)
Subject: Fix (#4017)
X-Git-Tag: cvc5-1.0.0~3515
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55f258cd92d7bc6fbb7a3b96712495f6885d871c;p=cvc5.git

Fix (#4017)

Fixes #4001.

This assertion was more of a conjecture (stating that easy cases of miniscoping are already handled). However some option combinations can break this invariant, regardless the code should do the correct thing.
---

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 6a54e8393..187c765d1 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1792,7 +1792,6 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
         }
       }
       Assert(!qvl1.empty());
-      Assert(!qvl2.empty() || !qvsh.empty());
       //check for literals that only contain shared variables
       std::vector<Node> qlitsh;
       std::vector<Node> qlit2;