From 55f258cd92d7bc6fbb7a3b96712495f6885d871c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Mar 2020 10:57:00 -0500
Subject: [PATCH] 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.
---
 src/theory/quantifiers/quantifiers_rewriter.cpp | 1 -
 1 file changed, 1 deletion(-)

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;
-- 
2.30.2