testlemma regressions

diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2
new file mode 100644 (file)
index 0000000..23bde47
--- /dev/null
+++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(assert (= x y))
+(check-sat)
+(get-model)

diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2
new file mode 100644 (file)
index 0000000..97ac584
--- /dev/null
+++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+(set-logic QF_UFLRA_SETS)
+(set-info :status sat)
+(declare-fun x () (Set Real))
+(declare-fun y () (Set Real))
+(assert (not (= x y)))
+(check-sat)
+(get-model)

diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2
index 74ce727475e9348315f9b556dbc98d6f50931d84..6f80b71475cec0c5af45eb57f3da89c60a33a7d2 100644 (file)
--- a/test/regress/regress0/sets/sets-testlemma.smt2
+++ b/test/regress/regress0/sets/sets-testlemma.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFBV_SETS)
 (set-info :status sat)
 (declare-fun x () (Set (_ BitVec 2)))
 (declare-fun y () (Set (_ BitVec 2)))