diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-08 14:32:16 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-08 14:32:16 -0800 |
| commit | 707571c8b4a572b9554f9068df796f1257cb587d (patch) | |
| tree | e7773fec0ee9d2460149a391d183448956ec1d63 /test/unit/Makefile.am | |
| parent | 1bf7e9db3bb501e1f3deeb905e8dec68bc028b71 (diff) | |
Fixed side conditions for CBQI BV, added unit tests. (#1434)
This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL,
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.
It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).
This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak
This simplifies to checking not (SC <=> exists x. s * x = t).
Diffstat (limited to 'test/unit/Makefile.am')
| -rw-r--r-- | test/unit/Makefile.am | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 9de940a0d..dfa3c79b6 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -13,6 +13,7 @@ UNIT_TESTS += \ theory/theory_arith_white \ theory/theory_bv_white \ theory/theory_bv_bvgauss_white \ + theory/theory_quantifiers_bv_inverter_white \ theory/type_enumerator_white \ expr/node_white \ expr/node_black \ |