From 7c2ea3c85221fce27d8c4d2b7d41a00e103b8cf5 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 12 Aug 2016 12:09:45 -0500 Subject: 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. --- test/regress/regress0/sets/Makefile.am | 3 ++- test/regress/regress0/sets/dt-simp-mem.smt2 | 9 +++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/sets/dt-simp-mem.smt2 (limited to 'test/regress/regress0/sets') 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) -- cgit v1.2.3