diff --git a/benchmarks/18-flat_quantifiers/03-nls_unfolding_v1.smt2 b/benchmarks/18-flat_quantifiers/03-nls_unfolding_v1.smt2
new file mode 100644
index 0000000..32d0633
--- /dev/null
+++ b/benchmarks/18-flat_quantifiers/03-nls_unfolding_v1.smt2
@@ -0,0 +1,31 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(set-option :use-builtin-definitions)
+
+(declare-const x NLS_t)
+(declare-const y NLS_t)
+(declare-const z NLS_t)
+
+(assert
+  (and
+    (sep
+      (nls x y z)
+      (distinct x y)
+    )
+    (not
+      (pto x (c_nls y z))
+    )
+  )
+)
+
+(assert (not
+  (exists ((n Loc))
+    (sep
+      (pto x (c_nls y n))
+      (pto n z)
+    )
+  )
+))
+
+(check-sat)
diff --git a/benchmarks/18-flat_quantifiers/04-nls_unfolding_v2.smt2 b/benchmarks/18-flat_quantifiers/04-nls_unfolding_v2.smt2
new file mode 100644
index 0000000..cb0e5fe
--- /dev/null
+++ b/benchmarks/18-flat_quantifiers/04-nls_unfolding_v2.smt2
@@ -0,0 +1,37 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(set-option :use-builtin-definitions)
+
+(declare-const x NLS_t)
+
+(assert
+  (and
+    (sep
+      (nls x nil nil)
+      (distinct x nil)
+    )
+    (not
+      (pto x (c_nls nil nil))
+    )
+  )
+)
+
+(assert (not
+  (or
+    (exists ((n Loc))
+      (sep
+        (pto x (c_nls nil n))
+        (pto n nil)
+      )
+    )
+    (exists ((t NLS_t))
+      (sep
+        (pto x (c_nls t nil))
+        (pto t (c_nls nil nil))
+      )
+    )
+  )
+))
+
+(check-sat)
diff --git a/benchmarks/18-flat_quantifiers/05-nls_unfolding_v3.smt2 b/benchmarks/18-flat_quantifiers/05-nls_unfolding_v3.smt2
new file mode 100644
index 0000000..b72e281
--- /dev/null
+++ b/benchmarks/18-flat_quantifiers/05-nls_unfolding_v3.smt2
@@ -0,0 +1,37 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(set-option :use-builtin-definitions)
+
+(declare-const x NLS_t)
+
+(assert
+  (and
+    (sep
+      (nls x nil nil)
+      (distinct x nil)
+    )
+    (not
+      (pto x (c_nls nil nil))
+    )
+  )
+)
+
+(assert (not
+  (or
+    (exists ((n Loc))
+      (sep
+        (pto x (c_nls nil n))
+        (ls n nil)
+      )
+    )
+    (exists ((t NLS_t))
+      (sep
+        (pto x (c_nls t nil))
+        (pto t (c_nls nil nil))
+      )
+    )
+  )
+))
+
+(check-sat)