Mark quantifier instantiations as needs justify (#5684)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Dec 2020 21:07:55 +0000 (15:07 -0600)
committerGitHub <noreply@github.com>
Wed, 16 Dec 2020 21:07:55 +0000 (15:07 -0600)
commitd5de3d822b978be11c98da5f026ab5f2ca9d0a83
tree20e5992cc228af8bcabddbad8347e6212691bc0b
parentbc55a9c137f92d0a21574c10a74f194e3abf4073
Mark quantifier instantiations as needs justify (#5684)

This avoids a solution soundness issue when disabling all NL strategies and using --nl-rlv=always.
src/theory/quantifiers_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 [new file with mode: 0644]