projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 10507bb) | patch
Fix (#4017)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Mar 2020 15:57:00 +0000 (10:57 -0500)
committerGitHub <noreply@github.com>
Wed, 11 Mar 2020 15:57:00 +0000 (10:57 -0500)
commit55f258cd92d7bc6fbb7a3b96712495f6885d871c
treef29de0680ce41a5b0069a906a54640651ae9dedftree
parent10507bb67177a1e52bdd89535c3c6d77cc62507acommit | 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.
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history