diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-10 18:38:16 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-10 18:38:16 +0200 |
| commit | 07504bdc61fe1d18af2fabe56fcee89e531b033c (patch) | |
| tree | e2bfddf7e0df15f1109afa598eb1e3754eab3e90 /test | |
| parent | 13438b29f61268fe93e96c11fed502bcce40427e (diff) | |
Models for codatatypes. Fixes bug 662.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rwxr-xr-x | test/regress/regress0/datatypes/cdt-model-cade15.smt2 | 17 |
2 files changed, 19 insertions, 1 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 45060dbd3..fc110ed92 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -65,7 +65,8 @@ TESTS = \ stream-singleton.smt2 \ is_test.smt2 \ manos-model.smt2 \ - bug625.smt2 + bug625.smt2 \ + cdt-model-cade15.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/cdt-model-cade15.smt2 b/test/regress/regress0/datatypes/cdt-model-cade15.smt2 new file mode 100755 index 000000000..5b570a915 --- /dev/null +++ b/test/regress/regress0/datatypes/cdt-model-cade15.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream)))))
+
+(declare-const z Stream)
+(declare-const x Stream)
+(declare-const y Stream)
+(declare-const u Stream)
+(declare-const v Stream)
+(declare-const w Stream)
+
+(assert (= u (C z)))
+(assert (= v (D z)))
+(assert (= w (E y)))
+(assert (= x (C v)))
+(assert (distinct x y z u v w))
+(check-sat)
\ No newline at end of file |