From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 12 Mar 2014 17:53:22 +0000 (-0400)
Subject: testlemma regressions
X-Git-Tag: cvc5-1.0.0~7002^2~9
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c1f794f35cca4be9ad1ca0135806430d06101eb2;p=cvc5.git

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
index 000000000..23bde47fd
--- /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
index 000000000..97ac5841a
--- /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 74ce72747..6f80b7147 100644
--- 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)))