Fixes for handling set universe: restrict upwards rule for universe to memberships into variable sets, do not variable eliminate sets during ppAssert.

3 files changed, 23 insertions, 1 deletions

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index c2e3546d9..9413dfba3 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -79,7 +79,9 @@ TESTS =	\
 	complement.cvc \
 	complement2.cvc \
   complement3.cvc \
-  sharing-simp.smt2
+  sharing-simp.smt2 \
+  pre-proc-univ.smt2 \
+  nonvar-univ.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/nonvar-univ.smt2 b/test/regress/regress0/sets/nonvar-univ.smt2
new file mode 100644
index 000000000..c71c984a2
--- /dev/null
+++ b/test/regress/regress0/sets/nonvar-univ.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () (Set Int))
+(declare-fun P ((Set Int)) Bool)
+
+(assert (P x))
+(assert (not (P (singleton 0))))
+(assert (member 1 x))
+(assert (not (member 0 (as univset (Set Int)))))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/pre-proc-univ.smt2 b/test/regress/regress0/sets/pre-proc-univ.smt2
new file mode 100644
index 000000000..1b4bf8b41
--- /dev/null
+++ b/test/regress/regress0/sets/pre-proc-univ.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () (Set Int))
+
+(assert (= x (union (singleton 0) (singleton 1))))
+
+(assert (not (member 0 (as univset (Set Int)))))
+
+(check-sat)