projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1ec2e46) | patch
Remove spurious assertion (#4117)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 19 Mar 2020 06:01:05 +0000 (01:01 -0500)
committerGitHub <noreply@github.com>
Thu, 19 Mar 2020 06:01:05 +0000 (01:01 -0500)
commit9c960866c9e71e543c5688aac826a8150c899ca6
tree623f5edb8e68b4b98c734c393c48c13da5d85355tree
parent1ec2e4637e092f1e62005bb3cffc3696d6099679commit | diff
Remove spurious assertion (#4117)

Fixes #4106.

The assertion was the wrong polarity (should have been Assert(options::cbqiAll()); but regardless is no longer an invariant of CEGQI).
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history