diff --git a/tests/solve_ndisj.ref b/tests/solve_ndisj.ref
new file mode 100644
index 0000000000000000000000000000000000000000..64a2dc8e334bfc8384132fbf5279262a9c644181
--- /dev/null
+++ b/tests/solve_ndisj.ref
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Ltac call to "solve_ndisj" failed.
+No applicable tactic.
diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
new file mode 100644
index 0000000000000000000000000000000000000000..3ed8e1f91825fc0494e8f2d04cf09879efd2ba27
--- /dev/null
+++ b/tests/solve_ndisj.v
@@ -0,0 +1,26 @@
+From stdpp Require Import namespaces strings.
+
+Lemma test1 (N1 N2 : namespace) :
+  N1 ## N2 â†’ â†‘N1 âŠ†@{coPset} âŠ¤ âˆ– â†‘N2.
+Proof. solve_ndisj. Qed.
+
+Lemma test2 (N1 N2 : namespace) :
+  N1 ## N2 â†’ â†‘N1.@"x" âŠ†@{coPset} âŠ¤ âˆ– â†‘N1.@"y" âˆ– â†‘N2.
+Proof. solve_ndisj. Qed.
+
+Lemma test3 (N : namespace) :
+  âŠ¤ âˆ– â†‘N âŠ†@{coPset} âŠ¤ âˆ– â†‘N.@"x".
+Proof. solve_ndisj. Qed.
+
+Lemma test4 (N : namespace) :
+  âŠ¤ âˆ– â†‘N âŠ†@{coPset} âŠ¤ âˆ– â†‘N.@"x" âˆ– â†‘N.@"y".
+Proof. solve_ndisj. Qed.
+
+Lemma test5 (N1 N2 : namespace) :
+  âŠ¤ âˆ– â†‘N1 âˆ– â†‘N2 âŠ†@{coPset} âŠ¤ âˆ– â†‘N1.@"x" âˆ– â†‘N2 âˆ– â†‘N1.@"y".
+Proof.
+  Fail solve_ndisj. (* FIXME: it should be able to solve this. *)
+  apply namespace_subseteq_difference.
+  { apply ndot_preserve_disjoint_r. set_solver. }
+  solve_ndisj.
+Qed.