diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-11 10:57:00 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-11 10:57:00 -0500 |
| commit | 55f258cd92d7bc6fbb7a3b96712495f6885d871c (patch) | |
| tree | f29de0680ce41a5b0069a906a54640651ae9dedf /src | |
| parent | 10507bb67177a1e52bdd89535c3c6d77cc62507a (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
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; |