diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-13 14:28:47 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-13 14:28:47 -0700 |
| commit | 459cb24dafae7b6253476cfae07a54fc5a4a9166 (patch) | |
| tree | 6f2ad56e2b4d5e878a6509555cba3d3c2aff2498 /test/regress | |
| parent | 39a85cc99f3b9f3d203490f5918ebe56bd916d64 (diff) | |
CBQI BV: Added EXTRACT handling. (#1240)
This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index ec24fdd8b..a2f5c18b5 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -104,11 +104,9 @@ TESTS = \ qbv-test-urem-rewrite.smt2 \ qbv-inequality2.smt2 \ qbv-test-invert-bvult-1.smt2 \ - intersection-example-onelane.proof-node22337.smt2 - -# solved, but fail an assertion due to unhandled EXTRACT case -# nested9_true-unreach-call.i_575.smt2 -# small-pipeline-fixpoint-3.smt2 + intersection-example-onelane.proof-node22337.smt2 \ + nested9_true-unreach-call.i_575.smt2 \ + small-pipeline-fixpoint-3.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine |