diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 5 | ||||
-rw-r--r-- | test/regress/regress1/bags/duplicate_removal1.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress1/bags/duplicate_removal2.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress1/bags/emptybag1.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress1/bags/intersection_min1.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress1/bags/intersection_min2.smt2 | 9 |
6 files changed, 50 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 94be987f7..128f9c567 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1430,6 +1430,11 @@ set(regress_1_tests regress1/bug800.smt2 regress1/bags/difference_remove1.smt2 regress1/bags/disequality.smt2 + regress1/bags/duplicate_removal1.smt2 + regress1/bags/duplicate_removal2.smt2 + regress1/bags/emptybag1.smt2 + regress1/bags/intersection_min1.smt2 + regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 regress1/bags/subbag1.smt2 regress1/bags/subbag2.smt2 diff --git a/test/regress/regress1/bags/duplicate_removal1.smt2 b/test/regress/regress1/bags/duplicate_removal1.smt2 new file mode 100644 index 000000000..2b662c6e5 --- /dev/null +++ b/test/regress/regress1/bags/duplicate_removal1.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Bag String)) +(declare-fun B () (Bag String)) +(assert (= B (duplicate_removal A))) +(assert (distinct (as emptybag (Bag String)) A B)) +(check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal2.smt2 b/test/regress/regress1/bags/duplicate_removal2.smt2 new file mode 100644 index 000000000..7dacaae43 --- /dev/null +++ b/test/regress/regress1/bags/duplicate_removal2.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun A () (Bag String)) +(declare-fun B () (Bag String)) +(assert (= B (duplicate_removal A))) +(assert (distinct (as emptybag (Bag String)) A B)) +(assert (= B (union_max A B))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/emptybag1.smt2 b/test/regress/regress1/bags/emptybag1.smt2 new file mode 100644 index 000000000..f7f92599d --- /dev/null +++ b/test/regress/regress1/bags/emptybag1.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun A () (Bag String)) +(declare-fun x () String) +(declare-fun y () Int) +(assert (= x "x")) +(assert (= A (as emptybag (Bag String)))) +(assert (= (bag.count x A) y)) +(assert(> y 1)) +(check-sat) diff --git a/test/regress/regress1/bags/intersection_min1.smt2 b/test/regress/regress1/bags/intersection_min1.smt2 new file mode 100644 index 000000000..f5a515b9c --- /dev/null +++ b/test/regress/regress1/bags/intersection_min1.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Bag String)) +(declare-fun B () (Bag String)) +(declare-fun C () (Bag String)) +(assert (= C (intersection_min A B))) +(assert (distinct (as emptybag (Bag String)) C)) +(assert (distinct A B C)) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/intersection_min2.smt2 b/test/regress/regress1/bags/intersection_min2.smt2 new file mode 100644 index 000000000..66afa2f3a --- /dev/null +++ b/test/regress/regress1/bags/intersection_min2.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun A () (Bag String)) +(declare-fun B () (Bag String)) +(declare-fun C () (Bag String)) +(assert (= C (intersection_min A B))) +(assert (= C (union_disjoint A B))) +(assert (distinct (as emptybag (Bag String)) C)) +(check-sat) |