Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)
authorMathias Preiner <mathias.preiner@gmail.com>
Thu, 12 Oct 2017 00:58:33 +0000 (17:58 -0700)
committerGitHub <noreply@github.com>
Thu, 12 Oct 2017 00:58:33 +0000 (17:58 -0700)
commitd6d8cd9e46e4e3ac39f468e45b107ec4a0e5b9a2
treedd634a60e67807dcf51477508f99bb0f8fa2f48a
parent435d9f0118914c634defa509e6c54a57c7b954ce
Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)
src/theory/quantifiers/bv_inverter.cpp
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 [new file with mode: 0644]
test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 [new file with mode: 0644]
test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 [new file with mode: 0644]
test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 [new file with mode: 0644]
test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 [new file with mode: 0644]