diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-03 19:00:40 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-03 17:00:40 -0700 |
| commit | 4873b5e515d8b3e5e70c42c50e8f680b26ba2331 (patch) | |
| tree | 0472c0e4dc6e4de4a1b1fba8cd08dff10c06111a /test | |
| parent | 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 (diff) | |
Sets subtypes (#1095)
Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/sets-of-sets-subtypes.smt2 | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 48c81a13b..70cb56b8f 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -744,6 +744,7 @@ REG0_TESTS = \ regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 \ regress0/sets/sets-equal.smt2 \ regress0/sets/sets-inter.smt2 \ + regress0/sets/sets-of-sets-subtypes.smt2 \ regress0/sets/sets-poly-int-real.smt2 \ regress0/sets/sets-poly-nonint.smt2 \ regress0/sets/sets-sample.smt2 \ diff --git a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 new file mode 100644 index 000000000..86a1d93b4 --- /dev/null +++ b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_LIRAFS) +(set-info :status unsat) + +(declare-fun s () (Set (Set Real))) +(declare-fun t () (Set (Set Int))) + +(declare-fun x () (Set Int)) +(declare-fun y () (Set Real)) + +(assert (member 0.5 y)) +(assert (member y s)) +(assert (or (= s t) (= s (singleton (singleton 1.0))) (= s (singleton (singleton 0.0))))) + +(check-sat) |