diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:35:03 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:50:58 -0500 |
| commit | 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch) | |
| tree | 9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /test/regress | |
| parent | d6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff) | |
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 5 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 8 |
2 files changed, 7 insertions, 6 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9a16f68ca..17a2ea2ef 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -172,7 +172,6 @@ BUG_TESTS = \ bug576.smt2 \ bug576a.smt2 \ bug578.smt2 \ - bug585.cvc \ bug586.cvc \ bug593.smt2 \ bug595.cvc \ @@ -189,8 +188,10 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # bug512 -- taking too long, --time-per not working perhaps? in any case, # we have a minimized version still getting tested # bug639 -- still fails, reopened bug +# bug585 -- contains subrange type (not supported) DISABLED_TESTS = \ - bug512.smt2 + bug512.smt2 \ + bug585.cvc EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index b437f1878..572e2790d 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -27,11 +27,11 @@ TESTS = \ rec1.cvc \ rec2.cvc \ rec4.cvc \ - rec5.cvc \ datatype.cvc \ datatype0.cvc \ datatype1.cvc \ datatype2.cvc \ + datatype3.cvc \ datatype4.cvc \ datatype13.cvc \ empty_tuprec.cvc \ @@ -83,10 +83,10 @@ TESTS = \ tuple-no-clash.cvc \ jsat-2.6.smt2 +# rec5 -- no longer support subrange types FAILING_TESTS = \ - datatype-dump.cvc - -# takes a long time to build model on debug : datatype3.cvc + datatype-dump.cvc \ + rec5.cvc EXTRA_DIST = $(TESTS) |