summaryrefslogtreecommitdiff
path: root/test/regress/regress1/bags/union_max2.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/bags/union_max2.smt2')
-rw-r--r--test/regress/regress1/bags/union_max2.smt26
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress1/bags/union_max2.smt2 b/test/regress/regress1/bags/union_max2.smt2
index dd4bceff5..1366130bf 100644
--- a/test/regress/regress1/bags/union_max2.smt2
+++ b/test/regress/regress1/bags/union_max2.smt2
@@ -4,8 +4,8 @@
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(declare-fun y () Int)
-(assert (= A (union_max (bag x 1) (bag y 2))))
-(assert (= A (union_disjoint B (bag y 2))))
+(assert (= A (bag.union_max (bag x 1) (bag y 2))))
+(assert (= A (bag.union_disjoint B (bag y 2))))
(assert (= x y))
-(assert (distinct (as emptybag (Bag Int)) B))
+(assert (distinct (as bag.empty (Bag Int)) B))
(check-sat) \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback