diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-12 12:09:45 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-12 12:09:59 -0500 |
| commit | 7c2ea3c85221fce27d8c4d2b7d41a00e103b8cf5 (patch) | |
| tree | 534cb48ad237e5ac6e682f55ea7104c9bb1b97f7 /test/regress/regress0/sets | |
| parent | ea1a0bc57bbd90421c76c2c4811882ce3ef90eb3 (diff) | |
Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
Diffstat (limited to 'test/regress/regress0/sets')
| -rw-r--r-- | test/regress/regress0/sets/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sets/dt-simp-mem.smt2 | 9 |
2 files changed, 11 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 19f6313fb..98e7e744c 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -62,7 +62,8 @@ TESTS = \ union-1a.smt2 \ union-1b-flip.smt2 \ union-1b.smt2 \ - union-2.smt2 + union-2.smt2 \ + dt-simp-mem.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2 new file mode 100644 index 000000000..a38544aa2 --- /dev/null +++ b/test/regress/regress0/sets/dt-simp-mem.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((D (A (a Int))))) +(declare-fun x1 () D) +(declare-fun S () (Set D)) +(declare-fun P (D) Bool) +(assert (member x1 S)) +(assert (=> (member (A 0) S) (P x1))) +(check-sat) |