projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 39a85cc) | patch
CBQI BV: Added EXTRACT handling. (#1240)
authorAina Niemetz <aina.niemetz@gmail.com>
Fri, 13 Oct 2017 21:28:47 +0000 (14:28 -0700)
committerGitHub <noreply@github.com>
Fri, 13 Oct 2017 21:28:47 +0000 (14:28 -0700)
commit459cb24dafae7b6253476cfae07a54fc5a4a9166
tree6f2ad56e2b4d5e878a6509555cba3d3c2aff2498tree
parent39a85cc99f3b9f3d203490f5918ebe56bd916d64commit | diff
CBQI BV: Added EXTRACT handling. (#1240)

This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled.
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history