From 37fdef4efb1cd50b34459a56bb5cb387828dbb11 Mon Sep 17 00:00:00 2001
From: Marton Hajdu <mezpusz@hotmail.com>
Date: Mon, 3 Nov 2025 18:44:16 +0100
Subject: [PATCH] Add minimal test with some syntax sugar

---
 Test/SyntaxSugar.hpp    |  4 ++++
 UnitTests/tProperty.cpp | 38 ++++++++++++++++++++++++++++++++++++++
 cmake/sources.cmake     |  1 +
 3 files changed, 43 insertions(+)
 create mode 100644 UnitTests/tProperty.cpp

diff --git a/Test/SyntaxSugar.hpp b/Test/SyntaxSugar.hpp
index c4ec567c9..aadfa2a0d 100644
--- a/Test/SyntaxSugar.hpp
+++ b/Test/SyntaxSugar.hpp
@@ -26,6 +26,7 @@
 #include "Lib/Environment.hpp"
 #include "Kernel/Inference.hpp"
 #include "Kernel/Clause.hpp"
+#include "Kernel/FormulaUnit.hpp"
 #include "Kernel/SortHelper.hpp"
 #include "Kernel/NumTraits.hpp"
 #include "Kernel/ApplicativeHelper.hpp"
@@ -720,6 +721,9 @@ inline Stack<Clause*> clauses(std::initializer_list<std::initializer_list<Lit>>
   return out;
 }
 
+inline FormulaUnit* formula(Lit lit)
+{ return new FormulaUnit(new AtomicFormula(lit), Inference(Kernel::NonspecificInference0(UnitInputType::ASSUMPTION, InferenceRule::INPUT))); }
+
 inline void createTermAlgebra(SortSugar sort, std::initializer_list<FuncSugar> fs) {
   // avoid redeclaration
   if (env.signature->isTermAlgebraSort(sort.sugaredExpr())) {
diff --git a/UnitTests/tProperty.cpp b/UnitTests/tProperty.cpp
new file mode 100644
index 000000000..5488caca0
--- /dev/null
+++ b/UnitTests/tProperty.cpp
@@ -0,0 +1,38 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+
+#include "Test/UnitTesting.hpp"
+#include "Test/SyntaxSugar.hpp"
+
+#include "Shell/Property.hpp"
+
+using namespace Shell;
+
+/**
+ * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses.
+ * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available
+ */
+#define MY_SYNTAX_SUGAR                                                                    \
+  DECL_DEFAULT_VARS                                                                        \
+  DECL_SORT(s)                                                                             \
+  DECL_FUNC(f, {s}, s)                                                                     \
+  DECL_CONST(c, s)                                                                         \
+  DECL_PRED(p, {s})                                                                        \
+
+TEST_FUN(test01) {
+  __ALLOW_UNUSED(MY_SYNTAX_SUGAR);
+
+  auto units = UnitList::empty();
+  UnitList::push(clause({ f(c) == c, ~p(x) }), units);
+  UnitList::push(formula(f(c) != c), units);
+
+  auto prop = Property::scan(units);
+  ASS_EQ(prop->category(), Property::NEQ);
+}
diff --git a/cmake/sources.cmake b/cmake/sources.cmake
index 5604a9b09..97d50e28e 100644
--- a/cmake/sources.cmake
+++ b/cmake/sources.cmake
@@ -67,6 +67,7 @@ set(UNIT_TESTS
     UnitTests/tList.cpp
     UnitTests/tOption.cpp
     UnitTests/tOptionConstraints.cpp
+    UnitTests/tProperty.cpp
     UnitTests/tPushUnaryMinus.cpp
     UnitTests/tQKbo.cpp
     UnitTests/tQuotientE.cpp