diff --git a/tests/multiset_solver.ref b/tests/multiset_solver.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
new file mode 100644
index 0000000000000000000000000000000000000000..a52397cf5059a6fca1c4e3b2cbe491aad62b74ce
--- /dev/null
+++ b/tests/multiset_solver.v
@@ -0,0 +1,18 @@
+From stdpp Require Import gmultiset.
+
+Section test.
+  Context `{Countable A}.
+  Implicit Types x y : A.
+  Implicit Types X Y : gmultiset A.
+
+  Lemma test1 x y X : {[x]} ⊎ ({[y]} ⊎ X) ≠ ∅.
+  Proof. multiset_solver. Qed.
+  Lemma test2 x y X : {[x]} ⊎ ({[y]} ⊎ X) = {[y]} ⊎ ({[x]} ⊎ X).
+  Proof. multiset_solver. Qed.
+  Lemma test3 x : {[x]} ⊎ ∅ ≠@{gmultiset A} ∅.
+  Proof. multiset_solver. Qed.
+  Lemma test4 x y z X Y :
+    {[z]} ⊎ X = {[y]} ⊎ Y →
+    {[x]} ⊎ ({[z]} ⊎ X) = {[y]} ⊎ ({[x]} ⊎ Y).
+  Proof. multiset_solver. Qed.
+End test.