1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress1/bags/fold2.smt2 b/test/regress/regress1/bags/fold2.smt2
new file mode 100644
index 000000000..9863a11c6
--- /dev/null
+++ b/test/regress/regress1/bags/fold2.smt2
@@ -0,0 +1,15 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(set-option :uf-lazy-ll true)
+(set-option :strings-exp true)
+(define-fun min ((x String) (y String)) String (ite (str.< x y) x y))
+(declare-fun A () (Bag String))
+(declare-fun x () String)
+(declare-fun minimum () String)
+(assert (= minimum (bag.fold min "zzz" A)))
+(assert (str.< "aaa" minimum ))
+(assert (str.< minimum "zzz"))
+(assert (distinct x minimum))
+(assert (= (bag.count x A) 2))
+(check-sat)