diff --git a/CMakeLists.txt b/CMakeLists.txt
index fa98228..c667240 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -32,3 +32,8 @@ endif(PROJECT_IS_TOP_LEVEL)
 
 add_subdirectory(src)
 add_subdirectory(src/pogPrinter)
+
+if(PROJECT_IS_TOP_LEVEL)
+  enable_testing()
+  add_subdirectory(tests)
+endif()
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
new file mode 100644
index 0000000..26de877
--- /dev/null
+++ b/tests/CMakeLists.txt
@@ -0,0 +1,36 @@
+include(FetchContent)
+FetchContent_Declare(
+  googletest
+  GIT_REPOSITORY https://github.com/google/googletest.git
+  GIT_TAG v1.14.0
+)
+set(gtest_force_shared_crt ON CACHE BOOL "" FORCE)
+FetchContent_MakeAvailable(googletest)
+
+include(GoogleTest)
+
+# Sanitizers for Debug builds (GCC/Clang only)
+if(CMAKE_BUILD_TYPE STREQUAL "Debug")
+  if(CMAKE_CXX_COMPILER_ID STREQUAL GNU OR CMAKE_CXX_COMPILER_ID MATCHES Clang$)
+    add_compile_options(-fsanitize=address,undefined -fno-omit-frame-pointer)
+    add_link_options(-fsanitize=address,undefined)
+  endif()
+endif()
+
+function(bast_add_test name)
+  add_executable(${name} ${name}.cpp)
+  target_link_libraries(${name} PRIVATE BAST_LIB tinyxml2 GTest::gtest_main)
+  target_include_directories(${name} PRIVATE ${CMAKE_SOURCE_DIR}/src)
+  gtest_discover_tests(${name})
+endfunction()
+
+bast_add_test(test_hash)
+bast_add_test(test_btype)
+bast_add_test(test_vars)
+bast_add_test(test_expr)
+bast_add_test(test_pred)
+bast_add_test(test_subst)
+bast_add_test(test_readExpr)
+bast_add_test(test_readPred)
+bast_add_test(test_readBType)
+bast_add_test(test_readSubst)
diff --git a/tests/test_btype.cpp b/tests/test_btype.cpp
new file mode 100644
index 0000000..831225e
--- /dev/null
+++ b/tests/test_btype.cpp
@@ -0,0 +1,286 @@
+#include "btype.h"
+
+#include <gtest/gtest.h>
+
+// --- Primitive types ---
+
+TEST(BType, PrimitiveKinds) {
+  EXPECT_EQ(BType::INT.getKind(), BType::Kind::INTEGER);
+  EXPECT_EQ(BType::BOOL.getKind(), BType::Kind::BOOLEAN);
+  EXPECT_EQ(BType::FLOAT.getKind(), BType::Kind::FLOAT);
+  EXPECT_EQ(BType::REAL.getKind(), BType::Kind::REAL);
+  EXPECT_EQ(BType::STRING.getKind(), BType::Kind::STRING);
+}
+
+TEST(BType, PrimitiveEquality) {
+  EXPECT_EQ(BType::INT, BType::INT);
+  EXPECT_EQ(BType::BOOL, BType::BOOL);
+  EXPECT_NE(BType::INT, BType::BOOL);
+  EXPECT_NE(BType::FLOAT, BType::REAL);
+  EXPECT_NE(BType::STRING, BType::INT);
+}
+
+TEST(BType, PrimitiveToString) {
+  EXPECT_EQ(BType::INT.to_string(), "INT");
+  EXPECT_EQ(BType::BOOL.to_string(), "BOOL");
+  EXPECT_EQ(BType::FLOAT.to_string(), "FLOAT");
+  EXPECT_EQ(BType::REAL.to_string(), "REAL");
+  EXPECT_EQ(BType::STRING.to_string(), "STRING");
+}
+
+TEST(BType, DefaultConstructorIsInteger) {
+  BType t;
+  EXPECT_EQ(t.getKind(), BType::Kind::INTEGER);
+  EXPECT_EQ(t, BType::INT);
+}
+
+// --- Power types ---
+
+TEST(BType, PowerTypeKind) {
+  auto t = BType::POW(BType::INT);
+  EXPECT_EQ(t.getKind(), BType::Kind::PowerType);
+}
+
+TEST(BType, PowerTypeContent) {
+  auto t = BType::POW(BType::INT);
+  EXPECT_EQ(t.toPowerType().content, BType::INT);
+}
+
+TEST(BType, PowerTypeEquality) {
+  EXPECT_EQ(BType::POW(BType::INT), BType::POW(BType::INT));
+  EXPECT_NE(BType::POW(BType::INT), BType::POW(BType::BOOL));
+}
+
+TEST(BType, PowerTypeNested) {
+  auto t = BType::POW(BType::POW(BType::INT));
+  EXPECT_EQ(t.getKind(), BType::Kind::PowerType);
+  auto inner = t.toPowerType().content;
+  EXPECT_EQ(inner.getKind(), BType::Kind::PowerType);
+  EXPECT_EQ(inner.toPowerType().content, BType::INT);
+}
+
+TEST(BType, PowerTypeToString) {
+  EXPECT_EQ(BType::POW(BType::INT).to_string(), "POW(INT)");
+  EXPECT_EQ(BType::POW(BType::POW(BType::BOOL)).to_string(),
+            "POW(POW(BOOL))");
+}
+
+TEST(BType, PrebuiltPowerTypes) {
+  EXPECT_EQ(BType::POW_INT, BType::POW(BType::INT));
+  EXPECT_EQ(BType::POW_BOOL, BType::POW(BType::BOOL));
+  EXPECT_EQ(BType::POW_FLOAT, BType::POW(BType::FLOAT));
+  EXPECT_EQ(BType::POW_STRING, BType::POW(BType::STRING));
+  EXPECT_EQ(BType::POW_REAL, BType::POW(BType::REAL));
+}
+
+// --- Product types ---
+
+TEST(BType, ProductTypeKind) {
+  auto t = BType::PROD(BType::INT, BType::BOOL);
+  EXPECT_EQ(t.getKind(), BType::Kind::ProductType);
+}
+
+TEST(BType, ProductTypeComponents) {
+  auto t = BType::PROD(BType::INT, BType::BOOL);
+  EXPECT_EQ(t.toProductType().lhs, BType::INT);
+  EXPECT_EQ(t.toProductType().rhs, BType::BOOL);
+}
+
+TEST(BType, ProductTypeEquality) {
+  EXPECT_EQ(BType::PROD(BType::INT, BType::BOOL),
+            BType::PROD(BType::INT, BType::BOOL));
+  EXPECT_NE(BType::PROD(BType::INT, BType::BOOL),
+            BType::PROD(BType::BOOL, BType::INT));
+}
+
+TEST(BType, ProductTypeToString) {
+  EXPECT_EQ(BType::PROD(BType::INT, BType::BOOL).to_string(),
+            "PROD(INT, BOOL)");
+}
+
+TEST(BType, RelationInteger) {
+  EXPECT_EQ(BType::RELATION_INTEGER, BType::POW(BType::PROD(BType::INT, BType::INT)));
+}
+
+// --- Abstract sets ---
+
+TEST(BType, AbstractSetKind) {
+  auto t = BType::SET("COLORS");
+  EXPECT_EQ(t.getKind(), BType::Kind::AbstractSet);
+}
+
+TEST(BType, AbstractSetName) {
+  auto t = BType::ABSTRACT_SET("COLORS");
+  EXPECT_EQ(t.toAbstractSetType().getName(), "COLORS");
+}
+
+TEST(BType, AbstractSetEquality) {
+  EXPECT_EQ(BType::SET("S"), BType::SET("S"));
+  EXPECT_NE(BType::SET("S"), BType::SET("T"));
+}
+
+TEST(BType, AbstractSetToString) {
+  EXPECT_EQ(BType::SET("COLORS").to_string(), "ASET(COLORS)");
+}
+
+TEST(BType, SetAndAbstractSetEqual) {
+  EXPECT_EQ(BType::SET("X"), BType::ABSTRACT_SET("X"));
+}
+
+// --- Enumerated sets ---
+
+TEST(BType, EnumeratedSetKind) {
+  auto t = BType::ENUMERATED_SET({"COLORS", {"red", "green", "blue"}});
+  EXPECT_EQ(t.getKind(), BType::Kind::EnumeratedSet);
+}
+
+TEST(BType, EnumeratedSetAccessors) {
+  auto t = BType::ENUMERATED_SET({"COLORS", {"red", "green", "blue"}});
+  EXPECT_EQ(t.toEnumeratedSetType().getName(), "COLORS");
+  auto &content = t.toEnumeratedSetType().getContent();
+  ASSERT_EQ(content.size(), 3u);
+  EXPECT_EQ(content[0], "red");
+  EXPECT_EQ(content[1], "green");
+  EXPECT_EQ(content[2], "blue");
+}
+
+TEST(BType, EnumeratedSetToString) {
+  auto t = BType::ENUMERATED_SET({"COLORS", {"red", "green"}});
+  EXPECT_EQ(t.to_string(), "ESET(COLORS)");
+}
+
+// --- Struct types ---
+
+TEST(BType, StructKind) {
+  auto t = BType::STRUCT({{"x", BType::INT}, {"y", BType::BOOL}});
+  EXPECT_EQ(t.getKind(), BType::Kind::Struct);
+}
+
+TEST(BType, StructFieldsSorted) {
+  auto t = BType::STRUCT({{"z", BType::INT}, {"a", BType::BOOL}});
+  auto &fields = t.toRecordType().m_fields;
+  ASSERT_EQ(fields.size(), 2u);
+  EXPECT_EQ(fields[0].first, "a");
+  EXPECT_EQ(fields[1].first, "z");
+}
+
+TEST(BType, StructEquality) {
+  auto t1 = BType::STRUCT({{"x", BType::INT}, {"y", BType::BOOL}});
+  auto t2 = BType::STRUCT({{"y", BType::BOOL}, {"x", BType::INT}});
+  EXPECT_EQ(t1, t2);
+}
+
+TEST(BType, StructInequality) {
+  auto t1 = BType::STRUCT({{"x", BType::INT}});
+  auto t2 = BType::STRUCT({{"x", BType::BOOL}});
+  EXPECT_NE(t1, t2);
+}
+
+TEST(BType, StructToString) {
+  auto t = BType::STRUCT({{"x", BType::INT}, {"y", BType::BOOL}});
+  EXPECT_EQ(t.to_string(), "STRUCT(x : INT, y : BOOL)");
+}
+
+// --- Comparison ---
+
+TEST(BType, CompareReflexive) {
+  EXPECT_EQ(BType::compare(BType::INT, BType::INT), 0);
+}
+
+TEST(BType, CompareTransitive) {
+  // Different kinds have an ordering
+  auto cmp1 = BType::compare(BType::INT, BType::BOOL);
+  auto cmp2 = BType::compare(BType::BOOL, BType::INT);
+  EXPECT_NE(cmp1, 0);
+  EXPECT_EQ(cmp1, -cmp2);
+}
+
+TEST(BType, CompareOperators) {
+  EXPECT_TRUE(BType::INT == BType::INT);
+  EXPECT_TRUE(BType::INT != BType::BOOL);
+  // One of these must be true
+  EXPECT_TRUE(BType::INT < BType::BOOL || BType::INT > BType::BOOL);
+}
+
+// Note: BType::vec_compare is declared but not implemented in the library
+
+// --- Hashing ---
+
+TEST(BType, HashConsistency) {
+  EXPECT_EQ(BType::INT.hash_combine(0), BType::INT.hash_combine(0));
+  EXPECT_EQ(BType::POW(BType::INT).hash_combine(0),
+            BType::POW(BType::INT).hash_combine(0));
+}
+
+TEST(BType, HashEqualObjectsSameHash) {
+  auto t1 = BType::PROD(BType::INT, BType::BOOL);
+  auto t2 = BType::PROD(BType::INT, BType::BOOL);
+  EXPECT_EQ(t1, t2);
+  EXPECT_EQ(t1.hash_combine(0), t2.hash_combine(0));
+}
+
+// --- Visitor ---
+
+class TestVisitor : public BType::Visitor {
+ public:
+  BType::Kind visited = BType::Kind::INTEGER;
+  void visitINTEGER() override { visited = BType::Kind::INTEGER; }
+  void visitBOOLEAN() override { visited = BType::Kind::BOOLEAN; }
+  void visitFLOAT() override { visited = BType::Kind::FLOAT; }
+  void visitREAL() override { visited = BType::Kind::REAL; }
+  void visitSTRING() override { visited = BType::Kind::STRING; }
+  void visitProductType(const BType &, const BType &) override {
+    visited = BType::Kind::ProductType;
+  }
+  void visitPowerType(const BType &) override {
+    visited = BType::Kind::PowerType;
+  }
+  void visitRecordType(
+      const std::vector<std::pair<std::string, BType>> &) override {
+    visited = BType::Kind::Struct;
+  }
+  void visitAbstractSet(const BType::AbstractSet &) override {
+    visited = BType::Kind::AbstractSet;
+  }
+  void visitEnumeratedSet(const BType::EnumeratedSet &) override {
+    visited = BType::Kind::EnumeratedSet;
+  }
+};
+
+TEST(BType, VisitorPrimitive) {
+  TestVisitor v;
+  BType::INT.accept(v);
+  EXPECT_EQ(v.visited, BType::Kind::INTEGER);
+  BType::BOOL.accept(v);
+  EXPECT_EQ(v.visited, BType::Kind::BOOLEAN);
+}
+
+TEST(BType, VisitorPowerType) {
+  TestVisitor v;
+  BType::POW(BType::INT).accept(v);
+  EXPECT_EQ(v.visited, BType::Kind::PowerType);
+}
+
+TEST(BType, VisitorProductType) {
+  TestVisitor v;
+  BType::PROD(BType::INT, BType::BOOL).accept(v);
+  EXPECT_EQ(v.visited, BType::Kind::ProductType);
+}
+
+TEST(BType, VisitorStruct) {
+  TestVisitor v;
+  BType::STRUCT({{"x", BType::INT}}).accept(v);
+  EXPECT_EQ(v.visited, BType::Kind::Struct);
+}
+
+TEST(BType, VisitorAbstractSet) {
+  TestVisitor v;
+  BType::SET("S").accept(v);
+  EXPECT_EQ(v.visited, BType::Kind::AbstractSet);
+}
+
+TEST(BType, VisitorEnumeratedSet) {
+  TestVisitor v;
+  BType::ENUMERATED_SET({"S", {"a", "b"}}).accept(v);
+  EXPECT_EQ(v.visited, BType::Kind::EnumeratedSet);
+}
diff --git a/tests/test_expr.cpp b/tests/test_expr.cpp
new file mode 100644
index 0000000..308513c
--- /dev/null
+++ b/tests/test_expr.cpp
@@ -0,0 +1,536 @@
+#include "expr.h"
+#include "exprDesc.h"
+
+#include <gtest/gtest.h>
+
+#include "pred.h"
+
+// --- Constants ---
+
+TEST(Expr, MaxInt) {
+  auto e = Expr::makeMaxInt();
+  EXPECT_EQ(e.getTag(), Expr::EKind::MaxInt);
+}
+
+TEST(Expr, MinInt) {
+  auto e = Expr::makeMinInt();
+  EXPECT_EQ(e.getTag(), Expr::EKind::MinInt);
+}
+
+TEST(Expr, ConstantINTEGER) {
+  auto e = Expr::makeINTEGER();
+  EXPECT_EQ(e.getTag(), Expr::EKind::INTEGER);
+  EXPECT_TRUE(e.isTypeExpression());
+}
+
+TEST(Expr, ConstantNATURAL) {
+  auto e = Expr::makeNATURAL();
+  EXPECT_EQ(e.getTag(), Expr::EKind::NATURAL);
+}
+
+TEST(Expr, ConstantBOOL) {
+  auto e = Expr::makeBOOL();
+  EXPECT_EQ(e.getTag(), Expr::EKind::BOOL);
+}
+
+TEST(Expr, ConstantTRUE) {
+  auto e = Expr::makeTRUE();
+  EXPECT_EQ(e.getTag(), Expr::EKind::TRUE);
+}
+
+TEST(Expr, ConstantFALSE) {
+  auto e = Expr::makeFALSE();
+  EXPECT_EQ(e.getTag(), Expr::EKind::FALSE);
+}
+
+TEST(Expr, Successor) {
+  auto e = Expr::makeSuccessor();
+  EXPECT_EQ(e.getTag(), Expr::EKind::Successor);
+}
+
+TEST(Expr, Predecessor) {
+  auto e = Expr::makePredecessor();
+  EXPECT_EQ(e.getTag(), Expr::EKind::Predecessor);
+}
+
+// --- Literals ---
+
+TEST(Expr, IntegerLiteral) {
+  auto e = Expr::makeInteger("42");
+  EXPECT_EQ(e.getTag(), Expr::EKind::IntegerLiteral);
+  EXPECT_EQ(e.getIntegerLiteral(), "42");
+}
+
+TEST(Expr, StringLiteral) {
+  auto e = Expr::makeString("hello");
+  EXPECT_EQ(e.getTag(), Expr::EKind::StringLiteral);
+  EXPECT_EQ(e.getStringLiteral(), "hello");
+}
+
+TEST(Expr, RealLiteral) {
+  Expr::Decimal d("3", "14");
+  auto e = Expr::makeReal(d);
+  EXPECT_EQ(e.getTag(), Expr::EKind::RealLiteral);
+  EXPECT_EQ(e.getRealLiteral().integerPart, "3");
+  EXPECT_EQ(e.getRealLiteral().fractionalPart, "14");
+}
+
+// --- Decimal ---
+
+TEST(Decimal, Compare) {
+  Expr::Decimal d1("3", "14");
+  Expr::Decimal d2("3", "14");
+  EXPECT_EQ(d1.compare(d2), 0);
+}
+
+TEST(Decimal, CompareDifferent) {
+  Expr::Decimal d1("3", "14");
+  Expr::Decimal d2("4", "0");
+  EXPECT_NE(d1.compare(d2), 0);
+}
+
+TEST(Decimal, IntegerOnly) {
+  Expr::Decimal d("42");
+  EXPECT_EQ(d.integerPart, "42");
+  EXPECT_EQ(d.fractionalPart, "0");
+}
+
+// --- Identifiers ---
+
+TEST(Expr, Ident) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto e = Expr::makeIdent(x, BType::INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Id);
+  EXPECT_EQ(e.getId(), x);
+  EXPECT_EQ(e.getType(), BType::INT);
+}
+
+// --- EmptySet ---
+
+TEST(Expr, EmptySet) {
+  auto e = Expr::makeEmptySet(BType::POW_INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::EmptySet);
+  EXPECT_EQ(e.getType(), BType::POW_INT);
+}
+
+// --- Binary expressions ---
+
+TEST(Expr, BinaryExpr) {
+  auto lhs = Expr::makeInteger("1");
+  auto rhs = Expr::makeInteger("2");
+  auto e = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition, std::move(lhs),
+                                std::move(rhs), BType::INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::BinaryExpr);
+  EXPECT_EQ(e.getType(), BType::INT);
+  auto &bin = e.toBinaryExpr();
+  EXPECT_EQ(bin.op, Expr::BinaryOp::IAddition);
+}
+
+// --- Unary expressions ---
+
+TEST(Expr, UnaryExpr) {
+  auto inner = Expr::makeIdent(VarName::makeVarWithoutSuffix("s"), BType::POW_INT);
+  auto e =
+      Expr::makeUnaryExpr(Expr::UnaryOp::Cardinality, std::move(inner), BType::INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::UnaryExpr);
+  EXPECT_EQ(e.toUnaryExpr().op, Expr::UnaryOp::Cardinality);
+}
+
+// --- Nary expressions ---
+
+TEST(Expr, NaryExprSet) {
+  std::vector<Expr> elems;
+  elems.push_back(Expr::makeInteger("1"));
+  elems.push_back(Expr::makeInteger("2"));
+  auto e =
+      Expr::makeNaryExpr(Expr::NaryOp::Set, std::move(elems), BType::POW_INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::NaryExpr);
+  EXPECT_EQ(e.toNaryExpr().op, Expr::NaryOp::Set);
+}
+
+TEST(Expr, NaryExprSequence) {
+  std::vector<Expr> elems;
+  elems.push_back(Expr::makeInteger("1"));
+  auto seqType = BType::POW(BType::PROD(BType::INT, BType::INT));
+  auto e =
+      Expr::makeNaryExpr(Expr::NaryOp::Sequence, std::move(elems), seqType);
+  EXPECT_EQ(e.getTag(), Expr::EKind::NaryExpr);
+  EXPECT_EQ(e.toNaryExpr().op, Expr::NaryOp::Sequence);
+}
+
+// --- Ternary expressions ---
+
+TEST(Expr, TernaryExpr) {
+  auto fst = Expr::makeInteger("1");
+  auto snd = Expr::makeInteger("2");
+  auto thd = Expr::makeInteger("3");
+  auto e = Expr::makeTernaryExpr(Expr::TernaryOp::Son, std::move(fst),
+                                 std::move(snd), std::move(thd), BType::INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::TernaryExpr);
+  EXPECT_EQ(e.toTernaryExpr().op, Expr::TernaryOp::Son);
+}
+
+// --- Quantified expressions ---
+
+TEST(Expr, QuantifiedExpr) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto cond = Pred::makeTrue();
+  auto body = Expr::makeIdent(x, BType::INT);
+  auto e = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars,
+                                    std::move(cond), std::move(body),
+                                    BType::POW(BType::PROD(BType::INT, BType::INT)));
+  EXPECT_EQ(e.getTag(), Expr::EKind::QuantifiedExpr);
+}
+
+// --- Quantified set ---
+
+TEST(Expr, QuantifiedSet) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto xExpr = Expr::makeIdent(x, BType::INT);
+  auto cond = Pred::makeExprComparison(Pred::ComparisonOp::Igt,
+                                       std::move(xExpr), Expr::makeInteger("0"));
+  auto e = Expr::makeQuantifiedSet(vars, std::move(cond), BType::POW_INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::QuantifiedSet);
+}
+
+// --- BooleanExpr ---
+
+TEST(Expr, BooleanExpr) {
+  auto p = Pred::makeTrue();
+  auto e = Expr::makeBooleanExpr(std::move(p));
+  EXPECT_EQ(e.getTag(), Expr::EKind::BooleanExpr);
+}
+
+// --- Record / Struct ---
+
+TEST(Expr, RecordExpr) {
+  std::vector<std::pair<std::string, Expr>> fields;
+  fields.push_back({"a", Expr::makeInteger("1")});
+  fields.push_back({"b", Expr::makeInteger("2")});
+  auto recType = BType::STRUCT({{"a", BType::INT}, {"b", BType::INT}});
+  auto e = Expr::makeRecord(std::move(fields), recType);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Record);
+}
+
+TEST(Expr, StructExpr) {
+  std::vector<std::pair<std::string, Expr>> fields;
+  fields.push_back({"a", Expr::makeINTEGER()});
+  auto structType = BType::STRUCT({{"a", BType::POW_INT}});
+  auto e = Expr::makeStruct(std::move(fields), structType);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Struct);
+}
+
+// --- Record field access ---
+
+TEST(Expr, RecordFieldAccess) {
+  auto x = Expr::makeIdent(
+      VarName::makeVarWithoutSuffix("r"),
+      BType::STRUCT({{"a", BType::INT}, {"b", BType::BOOL}}));
+  auto e = Expr::makeRecordFieldAccess(std::move(x), "a", BType::INT);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Record_Field_Access);
+}
+
+// --- Record field update ---
+
+TEST(Expr, RecordFieldUpdate) {
+  auto recType = BType::STRUCT({{"a", BType::INT}});
+  auto rec = Expr::makeIdent(VarName::makeVarWithoutSuffix("r"), recType);
+  auto val = Expr::makeInteger("42");
+  auto e = Expr::makeRecordFieldUpdate(std::move(rec), "a", std::move(val),
+                                       recType);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Record_Field_Update);
+}
+
+// --- Copy ---
+
+TEST(Expr, CopyPreservesTag) {
+  auto e = Expr::makeInteger("42");
+  auto c = e.copy();
+  EXPECT_EQ(c.getTag(), Expr::EKind::IntegerLiteral);
+  EXPECT_EQ(c.getIntegerLiteral(), "42");
+}
+
+TEST(Expr, CopyIndependent) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto e = Expr::makeIdent(x, BType::INT);
+  auto c = e.copy();
+  EXPECT_EQ(Expr::compare(e, c), 0);
+}
+
+// --- Comparison ---
+
+TEST(Expr, CompareEqual) {
+  auto e1 = Expr::makeInteger("42");
+  auto e2 = Expr::makeInteger("42");
+  EXPECT_EQ(Expr::compare(e1, e2), 0);
+}
+
+TEST(Expr, CompareDifferentKind) {
+  auto e1 = Expr::makeInteger("42");
+  auto e2 = Expr::makeString("hello");
+  EXPECT_NE(Expr::compare(e1, e2), 0);
+}
+
+TEST(Expr, CompareBinary) {
+  auto e1 = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                 Expr::makeInteger("1"), Expr::makeInteger("2"),
+                                 BType::INT);
+  auto e2 = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                 Expr::makeInteger("1"), Expr::makeInteger("2"),
+                                 BType::INT);
+  EXPECT_EQ(Expr::compare(e1, e2), 0);
+}
+
+TEST(Expr, CompareBinaryDifferentOp) {
+  auto e1 = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                 Expr::makeInteger("1"), Expr::makeInteger("2"),
+                                 BType::INT);
+  auto e2 = Expr::makeBinaryExpr(Expr::BinaryOp::ISubtraction,
+                                 Expr::makeInteger("1"), Expr::makeInteger("2"),
+                                 BType::INT);
+  EXPECT_NE(Expr::compare(e1, e2), 0);
+}
+
+// --- Alpha equality ---
+
+TEST(Expr, AlphaEqualsIdentical) {
+  auto e1 = Expr::makeInteger("42");
+  auto e2 = Expr::makeInteger("42");
+  EXPECT_TRUE(Expr::alpha_equals(e1, e2));
+}
+
+TEST(Expr, AlphaEqualsDifferent) {
+  auto e1 = Expr::makeInteger("1");
+  auto e2 = Expr::makeInteger("2");
+  EXPECT_FALSE(Expr::alpha_equals(e1, e2));
+}
+
+TEST(Expr, AlphaEqualsQuantified) {
+  // lambda x . x  vs  lambda x$1 . x$1  (same prefix, different suffix)
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto x1 = VarName::makeVar("x", 1);
+  std::vector<TypedVar> vars1 = {TypedVar(x, BType::INT)};
+  std::vector<TypedVar> vars2 = {TypedVar(x1, BType::INT)};
+  auto lambdaType = BType::POW(BType::PROD(BType::INT, BType::INT));
+
+  auto e1 = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars1,
+                                     Pred::makeTrue(),
+                                     Expr::makeIdent(x, BType::INT), lambdaType);
+  auto e2 = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars2,
+                                     Pred::makeTrue(),
+                                     Expr::makeIdent(x1, BType::INT), lambdaType);
+  EXPECT_TRUE(Expr::alpha_equals(e1, e2));
+}
+
+TEST(Expr, AlphaNotEqualsDifferentPrefix) {
+  // lambda x . x  vs  lambda y . y  (different prefix -> not alpha-equal)
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  std::vector<TypedVar> vars1 = {TypedVar(x, BType::INT)};
+  std::vector<TypedVar> vars2 = {TypedVar(y, BType::INT)};
+  auto lambdaType = BType::POW(BType::PROD(BType::INT, BType::INT));
+
+  auto e1 = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars1,
+                                     Pred::makeTrue(),
+                                     Expr::makeIdent(x, BType::INT), lambdaType);
+  auto e2 = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars2,
+                                     Pred::makeTrue(),
+                                     Expr::makeIdent(y, BType::INT), lambdaType);
+  EXPECT_FALSE(Expr::alpha_equals(e1, e2));
+}
+
+// --- Hashing ---
+
+TEST(Expr, HashConsistency) {
+  auto e1 = Expr::makeInteger("42");
+  auto e2 = Expr::makeInteger("42");
+  EXPECT_EQ(e1.hash_combine(0), e2.hash_combine(0));
+}
+
+TEST(Expr, HashEqualImpliesSameHash) {
+  auto e1 = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                 Expr::makeInteger("1"), Expr::makeInteger("2"),
+                                 BType::INT);
+  auto e2 = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                 Expr::makeInteger("1"), Expr::makeInteger("2"),
+                                 BType::INT);
+  EXPECT_EQ(Expr::compare(e1, e2), 0);
+  EXPECT_EQ(e1.hash_combine(0), e2.hash_combine(0));
+}
+
+// --- Free variables ---
+
+TEST(Expr, FreeVarsIdent) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto e = Expr::makeIdent(x, BType::INT);
+  auto fv = e.getFreeVars();
+  EXPECT_EQ(fv.size(), 1u);
+  EXPECT_TRUE(fv.count(x));
+}
+
+TEST(Expr, FreeVarsConstant) {
+  auto e = Expr::makeInteger("42");
+  auto fv = e.getFreeVars();
+  EXPECT_TRUE(fv.empty());
+}
+
+TEST(Expr, FreeVarsBinary) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  auto e = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                Expr::makeIdent(x, BType::INT),
+                                Expr::makeIdent(y, BType::INT), BType::INT);
+  auto fv = e.getFreeVars();
+  EXPECT_EQ(fv.size(), 2u);
+  EXPECT_TRUE(fv.count(x));
+  EXPECT_TRUE(fv.count(y));
+}
+
+TEST(Expr, FreeVarsQuantifiedBound) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto lambdaType = BType::POW(BType::PROD(BType::INT, BType::INT));
+  auto e = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars,
+                                    Pred::makeTrue(),
+                                    Expr::makeIdent(x, BType::INT), lambdaType);
+  auto fv = e.getFreeVars();
+  EXPECT_TRUE(fv.empty());
+}
+
+TEST(Expr, FreeVarsQuantifiedMixed) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto lambdaType = BType::POW(BType::PROD(BType::INT, BType::INT));
+  // lambda x . x + y  =>  y is free
+  auto body = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                   Expr::makeIdent(x, BType::INT),
+                                   Expr::makeIdent(y, BType::INT), BType::INT);
+  auto e = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars,
+                                    Pred::makeTrue(), std::move(body),
+                                    lambdaType);
+  auto fv = e.getFreeVars();
+  EXPECT_EQ(fv.size(), 1u);
+  EXPECT_TRUE(fv.count(y));
+  EXPECT_FALSE(fv.count(x));
+}
+
+// --- getAllVars ---
+
+TEST(Expr, GetAllVarsQuantified) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto lambdaType = BType::POW(BType::PROD(BType::INT, BType::INT));
+  auto body = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                   Expr::makeIdent(x, BType::INT),
+                                   Expr::makeIdent(y, BType::INT), BType::INT);
+  auto e = Expr::makeQuantifiedExpr(Expr::QuantifiedOp::Lambda, vars,
+                                    Pred::makeTrue(), std::move(body),
+                                    lambdaType);
+  auto av = e.getAllVars();
+  EXPECT_EQ(av.size(), 2u);
+  EXPECT_TRUE(av.count(x));
+  EXPECT_TRUE(av.count(y));
+}
+
+// --- Substitution ---
+
+TEST(Expr, SubstIdent) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto e = Expr::makeIdent(x, BType::INT);
+  std::map<VarName, Expr> map;
+  map.insert({x, Expr::makeInteger("42")});
+  e.subst(map);
+  EXPECT_EQ(e.getTag(), Expr::EKind::IntegerLiteral);
+  EXPECT_EQ(e.getIntegerLiteral(), "42");
+}
+
+TEST(Expr, SubstNoMatch) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  auto e = Expr::makeIdent(x, BType::INT);
+  std::map<VarName, Expr> map;
+  map.insert({y, Expr::makeInteger("42")});
+  e.subst(map);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Id);
+  EXPECT_EQ(e.getId(), x);
+}
+
+TEST(Expr, SubstBinary) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto e = Expr::makeBinaryExpr(Expr::BinaryOp::IAddition,
+                                Expr::makeIdent(x, BType::INT),
+                                Expr::makeInteger("1"), BType::INT);
+  std::map<VarName, Expr> map;
+  map.insert({x, Expr::makeInteger("5")});
+  e.subst(map);
+  // After substitution, lhs should be 5
+  auto &bin = e.toBinaryExpr();
+  EXPECT_EQ(bin.lhs.getTag(), Expr::EKind::IntegerLiteral);
+  EXPECT_EQ(bin.lhs.getIntegerLiteral(), "5");
+}
+
+// --- Alpha renaming ---
+
+TEST(Expr, AlphaRename) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  auto e = Expr::makeIdent(x, BType::INT);
+  std::map<VarName, VarName> map;
+  map.insert({x, y});
+  e.alpha(map);
+  EXPECT_EQ(e.getId(), y);
+}
+
+// --- BxmlTag ---
+
+TEST(Expr, BxmlTag) {
+  auto e = Expr::makeInteger("1", {"tag1", "tag2"});
+  auto &tags = e.getBxmlTag();
+  ASSERT_EQ(tags.size(), 2u);
+  EXPECT_EQ(tags[0], "tag1");
+  EXPECT_EQ(tags[1], "tag2");
+}
+
+// --- Default constructor ---
+
+TEST(Expr, DefaultConstructor) {
+  Expr e;
+  EXPECT_EQ(e.getTag(), Expr::EKind::MaxInt);
+}
+
+// --- Vec compare ---
+
+TEST(Expr, VecCompareEqual) {
+  std::vector<Expr> v1;
+  v1.push_back(Expr::makeInteger("1"));
+  v1.push_back(Expr::makeInteger("2"));
+  std::vector<Expr> v2;
+  v2.push_back(Expr::makeInteger("1"));
+  v2.push_back(Expr::makeInteger("2"));
+  EXPECT_EQ(Expr::vec_compare(v1, v2), 0);
+}
+
+TEST(Expr, VecCompareDifferentSize) {
+  std::vector<Expr> v1;
+  v1.push_back(Expr::makeInteger("1"));
+  std::vector<Expr> v2;
+  v2.push_back(Expr::makeInteger("1"));
+  v2.push_back(Expr::makeInteger("2"));
+  EXPECT_LT(Expr::vec_compare(v1, v2), 0);
+}
+
+// --- getFreeTVars ---
+
+TEST(Expr, GetFreeTVars) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto e = Expr::makeIdent(x, BType::INT);
+  auto ftv = e.getFreeTVars();
+  EXPECT_EQ(ftv.size(), 1u);
+  auto it = ftv.begin();
+  EXPECT_EQ(it->name, x);
+  EXPECT_EQ(it->type, BType::INT);
+}
diff --git a/tests/test_hash.cpp b/tests/test_hash.cpp
new file mode 100644
index 0000000..4d822d0
--- /dev/null
+++ b/tests/test_hash.cpp
@@ -0,0 +1,65 @@
+#include "hash.h"
+
+#include <gtest/gtest.h>
+
+TEST(HashUtil, CombineIntDeterministic) {
+  size_t a = hashUtil::hash_combine_int(42, 0);
+  size_t b = hashUtil::hash_combine_int(42, 0);
+  EXPECT_EQ(a, b);
+}
+
+TEST(HashUtil, CombineIntDifferentValues) {
+  size_t a = hashUtil::hash_combine_int(1, 0);
+  size_t b = hashUtil::hash_combine_int(2, 0);
+  EXPECT_NE(a, b);
+}
+
+TEST(HashUtil, CombineIntDifferentSeeds) {
+  size_t a = hashUtil::hash_combine_int(42, 0);
+  size_t b = hashUtil::hash_combine_int(42, 1);
+  EXPECT_NE(a, b);
+}
+
+TEST(HashUtil, CombineStringDeterministic) {
+  size_t a = hashUtil::hash_combine_string("hello", 0);
+  size_t b = hashUtil::hash_combine_string("hello", 0);
+  EXPECT_EQ(a, b);
+}
+
+TEST(HashUtil, CombineStringDifferentValues) {
+  size_t a = hashUtil::hash_combine_string("hello", 0);
+  size_t b = hashUtil::hash_combine_string("world", 0);
+  EXPECT_NE(a, b);
+}
+
+TEST(HashUtil, CombineStringDifferentSeeds) {
+  size_t a = hashUtil::hash_combine_string("hello", 0);
+  size_t b = hashUtil::hash_combine_string("hello", 1);
+  EXPECT_NE(a, b);
+}
+
+TEST(HashUtil, CombineStringEmpty) {
+  size_t a = hashUtil::hash_combine_string("", 0);
+  size_t b = hashUtil::hash_combine_string("x", 0);
+  EXPECT_NE(a, b);
+}
+
+TEST(HashUtil, CombineChaining) {
+  size_t h1 = hashUtil::hash_combine_int(1, 0);
+  h1 = hashUtil::hash_combine_int(2, h1);
+
+  size_t h2 = hashUtil::hash_combine_int(1, 0);
+  h2 = hashUtil::hash_combine_int(2, h2);
+
+  EXPECT_EQ(h1, h2);
+}
+
+TEST(HashUtil, CombineOrderMatters) {
+  size_t h1 = hashUtil::hash_combine_int(1, 0);
+  h1 = hashUtil::hash_combine_int(2, h1);
+
+  size_t h2 = hashUtil::hash_combine_int(2, 0);
+  h2 = hashUtil::hash_combine_int(1, h2);
+
+  EXPECT_NE(h1, h2);
+}
diff --git a/tests/test_pred.cpp b/tests/test_pred.cpp
new file mode 100644
index 0000000..ca70fe3
--- /dev/null
+++ b/tests/test_pred.cpp
@@ -0,0 +1,462 @@
+#include "pred.h"
+#include "predDesc.h"
+
+#include <gtest/gtest.h>
+
+// --- Constants ---
+
+TEST(Pred, True) {
+  auto p = Pred::makeTrue();
+  EXPECT_EQ(p.getTag(), Pred::PKind::True);
+}
+
+TEST(Pred, False) {
+  auto p = Pred::makeFalse();
+  EXPECT_EQ(p.getTag(), Pred::PKind::False);
+}
+
+// --- Implication ---
+
+TEST(Pred, Implication) {
+  auto p = Pred::makeImplication(Pred::makeTrue(), Pred::makeFalse());
+  EXPECT_EQ(p.getTag(), Pred::PKind::Implication);
+  auto &impl = p.toImplication();
+  EXPECT_EQ(impl.lhs.getTag(), Pred::PKind::True);
+  EXPECT_EQ(impl.rhs.getTag(), Pred::PKind::False);
+}
+
+// --- Equivalence ---
+
+TEST(Pred, Equivalence) {
+  auto p = Pred::makeEquivalence(Pred::makeTrue(), Pred::makeTrue());
+  EXPECT_EQ(p.getTag(), Pred::PKind::Equivalence);
+}
+
+// --- Negation ---
+
+TEST(Pred, Negation) {
+  auto p = Pred::makeNegation(Pred::makeTrue());
+  EXPECT_EQ(p.getTag(), Pred::PKind::Negation);
+  auto &neg = p.toNegation();
+  EXPECT_EQ(neg.operand.getTag(), Pred::PKind::True);
+}
+
+// --- Conjunction ---
+
+TEST(Pred, Conjunction) {
+  std::vector<Pred> vec;
+  vec.push_back(Pred::makeTrue());
+  vec.push_back(Pred::makeFalse());
+  auto p = Pred::makeConjunction(std::move(vec));
+  EXPECT_EQ(p.getTag(), Pred::PKind::Conjunction);
+  auto &conj = p.toConjunction();
+  EXPECT_EQ(conj.operands.size(), 2u);
+}
+
+// --- Disjunction ---
+
+TEST(Pred, Disjunction) {
+  std::vector<Pred> vec;
+  vec.push_back(Pred::makeTrue());
+  vec.push_back(Pred::makeFalse());
+  auto p = Pred::makeDisjunction(std::move(vec));
+  EXPECT_EQ(p.getTag(), Pred::PKind::Disjunction);
+  auto &disj = p.toDisjunction();
+  EXPECT_EQ(disj.operands.size(), 2u);
+}
+
+// --- ExprComparison ---
+
+TEST(Pred, ExprComparison) {
+  auto lhs = Expr::makeIdent(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  auto rhs = Expr::makeInteger("0");
+  auto p = Pred::makeExprComparison(Pred::ComparisonOp::Equality,
+                                    std::move(lhs), std::move(rhs));
+  EXPECT_EQ(p.getTag(), Pred::PKind::ExprComparison);
+  auto &cmp = p.toExprComparison();
+  EXPECT_EQ(cmp.op, Pred::ComparisonOp::Equality);
+}
+
+TEST(Pred, ExprComparisonMembership) {
+  auto x = Expr::makeIdent(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  auto s = Expr::makeINTEGER();
+  auto p = Pred::makeExprComparison(Pred::ComparisonOp::Membership,
+                                    std::move(x), std::move(s));
+  EXPECT_EQ(p.getTag(), Pred::PKind::ExprComparison);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Membership);
+}
+
+// --- Forall ---
+
+TEST(Pred, Forall) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto body = Pred::makeTrue();
+  auto p = Pred::makeForall(vars, std::move(body));
+  EXPECT_EQ(p.getTag(), Pred::PKind::Forall);
+  auto &fa = p.toForall();
+  EXPECT_EQ(fa.vars.size(), 1u);
+}
+
+// --- Exists ---
+
+TEST(Pred, Exists) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto body = Pred::makeTrue();
+  auto p = Pred::makeExists(vars, std::move(body));
+  EXPECT_EQ(p.getTag(), Pred::PKind::Exists);
+  auto &ex = p.toExists();
+  EXPECT_EQ(ex.vars.size(), 1u);
+}
+
+// --- GoalTag ---
+
+TEST(Pred, GoalTag) {
+  auto p = Pred::makeTrue("myGoal");
+  EXPECT_EQ(p.getGoalTag(), "myGoal");
+}
+
+TEST(Pred, SetGoalTag) {
+  auto p = Pred::makeTrue();
+  p.setGoalTag("updated");
+  EXPECT_EQ(p.getGoalTag(), "updated");
+}
+
+// --- BxmlTag ---
+
+TEST(Pred, BxmlTag) {
+  Pred::BXmlTags tags = {"t1", "t2"};
+  auto p = Pred::makeTrue("", tags);
+  EXPECT_EQ(p.getBxmlTag().size(), 2u);
+  EXPECT_TRUE(p.getBxmlTag().count("t1"));
+  EXPECT_TRUE(p.getBxmlTag().count("t2"));
+}
+
+// --- Copy ---
+
+TEST(Pred, CopyTrue) {
+  auto p = Pred::makeTrue("goal1");
+  auto c = p.copy();
+  EXPECT_EQ(c.getTag(), Pred::PKind::True);
+  EXPECT_EQ(c.getGoalTag(), "goal1");
+}
+
+TEST(Pred, CopyImplication) {
+  auto p = Pred::makeImplication(Pred::makeTrue(), Pred::makeFalse());
+  auto c = p.copy();
+  EXPECT_EQ(c.getTag(), Pred::PKind::Implication);
+  EXPECT_EQ(Pred::compare(p, c), 0);
+}
+
+// --- Comparison ---
+
+TEST(Pred, CompareEqual) {
+  auto p1 = Pred::makeTrue();
+  auto p2 = Pred::makeTrue();
+  EXPECT_EQ(Pred::compare(p1, p2), 0);
+}
+
+TEST(Pred, CompareDifferent) {
+  auto p1 = Pred::makeTrue();
+  auto p2 = Pred::makeFalse();
+  EXPECT_NE(Pred::compare(p1, p2), 0);
+}
+
+TEST(Pred, CompareImplication) {
+  auto p1 = Pred::makeImplication(Pred::makeTrue(), Pred::makeFalse());
+  auto p2 = Pred::makeImplication(Pred::makeTrue(), Pred::makeFalse());
+  EXPECT_EQ(Pred::compare(p1, p2), 0);
+}
+
+TEST(Pred, VecCompareEqual) {
+  std::vector<Pred> v1;
+  v1.push_back(Pred::makeTrue());
+  v1.push_back(Pred::makeFalse());
+  std::vector<Pred> v2;
+  v2.push_back(Pred::makeTrue());
+  v2.push_back(Pred::makeFalse());
+  EXPECT_EQ(Pred::vec_compare(v1, v2), 0);
+}
+
+TEST(Pred, VecCompareDifferentSize) {
+  std::vector<Pred> v1;
+  v1.push_back(Pred::makeTrue());
+  std::vector<Pred> v2;
+  v2.push_back(Pred::makeTrue());
+  v2.push_back(Pred::makeFalse());
+  EXPECT_LT(Pred::vec_compare(v1, v2), 0);
+}
+
+// --- Hashing ---
+
+TEST(Pred, HashConsistency) {
+  auto p1 = Pred::makeTrue();
+  auto p2 = Pred::makeTrue();
+  EXPECT_EQ(p1.hash_combine(0), p2.hash_combine(0));
+}
+
+TEST(Pred, HashEqualImpliesSameHash) {
+  auto p1 = Pred::makeImplication(Pred::makeTrue(), Pred::makeFalse());
+  auto p2 = Pred::makeImplication(Pred::makeTrue(), Pred::makeFalse());
+  EXPECT_EQ(Pred::compare(p1, p2), 0);
+  EXPECT_EQ(p1.hash_combine(0), p2.hash_combine(0));
+}
+
+TEST(Pred, StdHash) {
+  auto p1 = Pred::makeTrue();
+  auto p2 = Pred::makeTrue();
+  std::hash<Pred> h;
+  EXPECT_EQ(h(p1), h(p2));
+}
+
+// --- Free variables ---
+
+TEST(Pred, FreeVarsTrue) {
+  auto p = Pred::makeTrue();
+  EXPECT_TRUE(p.getFreeVars().empty());
+}
+
+TEST(Pred, FreeVarsComparison) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto p = Pred::makeExprComparison(
+      Pred::ComparisonOp::Equality, Expr::makeIdent(x, BType::INT),
+      Expr::makeInteger("0"));
+  auto fv = p.getFreeVars();
+  EXPECT_EQ(fv.size(), 1u);
+  EXPECT_TRUE(fv.count(x));
+}
+
+TEST(Pred, FreeVarsForallBound) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto body = Pred::makeExprComparison(
+      Pred::ComparisonOp::Igt, Expr::makeIdent(x, BType::INT),
+      Expr::makeInteger("0"));
+  auto p = Pred::makeForall(vars, std::move(body));
+  auto fv = p.getFreeVars();
+  EXPECT_TRUE(fv.empty());
+}
+
+TEST(Pred, FreeVarsForallMixed) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto body = Pred::makeExprComparison(
+      Pred::ComparisonOp::Equality, Expr::makeIdent(x, BType::INT),
+      Expr::makeIdent(y, BType::INT));
+  auto p = Pred::makeForall(vars, std::move(body));
+  auto fv = p.getFreeVars();
+  EXPECT_EQ(fv.size(), 1u);
+  EXPECT_TRUE(fv.count(y));
+}
+
+// --- getAllVars ---
+
+TEST(Pred, GetAllVarsForall) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  std::vector<TypedVar> vars = {TypedVar(x, BType::INT)};
+  auto body = Pred::makeExprComparison(
+      Pred::ComparisonOp::Equality, Expr::makeIdent(x, BType::INT),
+      Expr::makeIdent(y, BType::INT));
+  auto p = Pred::makeForall(vars, std::move(body));
+  auto av = p.getAllVars();
+  EXPECT_EQ(av.size(), 2u);
+  EXPECT_TRUE(av.count(x));
+  EXPECT_TRUE(av.count(y));
+}
+
+// --- getFreeTVars ---
+
+TEST(Pred, GetFreeTVars) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto p = Pred::makeExprComparison(
+      Pred::ComparisonOp::Equality, Expr::makeIdent(x, BType::INT),
+      Expr::makeInteger("0"));
+  auto ftv = p.getFreeTVars();
+  EXPECT_EQ(ftv.size(), 1u);
+  auto it = ftv.begin();
+  EXPECT_EQ(it->name, x);
+  EXPECT_EQ(it->type, BType::INT);
+}
+
+// --- Substitution ---
+
+TEST(Pred, SubstComparison) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto p = Pred::makeExprComparison(
+      Pred::ComparisonOp::Equality, Expr::makeIdent(x, BType::INT),
+      Expr::makeInteger("0"));
+  std::map<VarName, Expr> map;
+  map.insert({x, Expr::makeInteger("5")});
+  p.subst(map);
+  auto &cmp = p.toExprComparison();
+  EXPECT_EQ(cmp.lhs.getTag(), Expr::EKind::IntegerLiteral);
+  EXPECT_EQ(cmp.lhs.getIntegerLiteral(), "5");
+}
+
+// --- Alpha renaming ---
+
+TEST(Pred, AlphaRename) {
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  auto p = Pred::makeExprComparison(
+      Pred::ComparisonOp::Equality, Expr::makeIdent(x, BType::INT),
+      Expr::makeInteger("0"));
+  std::map<VarName, VarName> map;
+  map.insert({x, y});
+  p.alpha(map);
+  auto &cmp = p.toExprComparison();
+  EXPECT_EQ(cmp.lhs.getId(), y);
+}
+
+// --- Alpha equality ---
+
+TEST(Pred, AlphaEqualsTrue) {
+  EXPECT_TRUE(Pred::alpha_equals(Pred::makeTrue(), Pred::makeTrue()));
+}
+
+TEST(Pred, AlphaEqualsDifferent) {
+  EXPECT_FALSE(Pred::alpha_equals(Pred::makeTrue(), Pred::makeFalse()));
+}
+
+TEST(Pred, AlphaEqualsForall) {
+  // forall x . x > 0  vs  forall x$1 . x$1 > 0  (same prefix, diff suffix)
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto x1 = VarName::makeVar("x", 1);
+  std::vector<TypedVar> v1 = {TypedVar(x, BType::INT)};
+  std::vector<TypedVar> v2 = {TypedVar(x1, BType::INT)};
+  auto p1 = Pred::makeForall(
+      v1, Pred::makeExprComparison(Pred::ComparisonOp::Igt,
+                                   Expr::makeIdent(x, BType::INT),
+                                   Expr::makeInteger("0")));
+  auto p2 = Pred::makeForall(
+      v2, Pred::makeExprComparison(Pred::ComparisonOp::Igt,
+                                   Expr::makeIdent(x1, BType::INT),
+                                   Expr::makeInteger("0")));
+  EXPECT_TRUE(Pred::alpha_equals(p1, p2));
+}
+
+TEST(Pred, AlphaNotEqualsForallDifferentPrefix) {
+  // forall x . x > 0  vs  forall y . y > 0  (different prefix -> not equal)
+  auto x = VarName::makeVarWithoutSuffix("x");
+  auto y = VarName::makeVarWithoutSuffix("y");
+  std::vector<TypedVar> v1 = {TypedVar(x, BType::INT)};
+  std::vector<TypedVar> v2 = {TypedVar(y, BType::INT)};
+  auto p1 = Pred::makeForall(
+      v1, Pred::makeExprComparison(Pred::ComparisonOp::Igt,
+                                   Expr::makeIdent(x, BType::INT),
+                                   Expr::makeInteger("0")));
+  auto p2 = Pred::makeForall(
+      v2, Pred::makeExprComparison(Pred::ComparisonOp::Igt,
+                                   Expr::makeIdent(y, BType::INT),
+                                   Expr::makeInteger("0")));
+  EXPECT_FALSE(Pred::alpha_equals(p1, p2));
+}
+
+// --- isPureTypingPredicate ---
+
+TEST(Pred, IsPureTypingMembership) {
+  // x : INTEGER is a pure typing predicate
+  auto x = Expr::makeIdent(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  auto p = Pred::makeExprComparison(Pred::ComparisonOp::Membership,
+                                    std::move(x), Expr::makeINTEGER());
+  EXPECT_TRUE(p.isPureTypingPredicate());
+}
+
+TEST(Pred, IsNotPureTypingEquality) {
+  // x = 3 is not a pure typing predicate
+  auto x = Expr::makeIdent(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  auto p = Pred::makeExprComparison(Pred::ComparisonOp::Equality,
+                                    std::move(x), Expr::makeInteger("3"));
+  EXPECT_FALSE(p.isPureTypingPredicate());
+}
+
+TEST(Pred, IsNotPureTypingTrue) {
+  auto p = Pred::makeTrue();
+  EXPECT_FALSE(p.isPureTypingPredicate());
+}
+
+// --- Visitor ---
+
+class TestPredVisitor : public Pred::Visitor {
+ public:
+  Pred::PKind visited = Pred::PKind::True;
+  void visitImplication(const Pred &, const Pred &) override {
+    visited = Pred::PKind::Implication;
+  }
+  void visitEquivalence(const Pred &, const Pred &) override {
+    visited = Pred::PKind::Equivalence;
+  }
+  void visitExprComparison(Pred::ComparisonOp, const Expr &,
+                           const Expr &) override {
+    visited = Pred::PKind::ExprComparison;
+  }
+  void visitNegation(const Pred &) override {
+    visited = Pred::PKind::Negation;
+  }
+  void visitConjunction(const std::vector<Pred> &) override {
+    visited = Pred::PKind::Conjunction;
+  }
+  void visitDisjunction(const std::vector<Pred> &) override {
+    visited = Pred::PKind::Disjunction;
+  }
+  void visitForall(const std::vector<TypedVar> &, const Pred &) override {
+    visited = Pred::PKind::Forall;
+  }
+  void visitExists(const std::vector<TypedVar> &, const Pred &) override {
+    visited = Pred::PKind::Exists;
+  }
+  void visitTrue() override { visited = Pred::PKind::True; }
+  void visitFalse() override { visited = Pred::PKind::False; }
+};
+
+TEST(Pred, VisitorTrue) {
+  TestPredVisitor v;
+  Pred::makeTrue().accept(v);
+  EXPECT_EQ(v.visited, Pred::PKind::True);
+}
+
+TEST(Pred, VisitorImplication) {
+  TestPredVisitor v;
+  Pred::makeImplication(Pred::makeTrue(), Pred::makeFalse()).accept(v);
+  EXPECT_EQ(v.visited, Pred::PKind::Implication);
+}
+
+TEST(Pred, VisitorNegation) {
+  TestPredVisitor v;
+  Pred::makeNegation(Pred::makeTrue()).accept(v);
+  EXPECT_EQ(v.visited, Pred::PKind::Negation);
+}
+
+TEST(Pred, VisitorConjunction) {
+  TestPredVisitor v;
+  std::vector<Pred> vec;
+  vec.push_back(Pred::makeTrue());
+  Pred::makeConjunction(std::move(vec)).accept(v);
+  EXPECT_EQ(v.visited, Pred::PKind::Conjunction);
+}
+
+TEST(Pred, VisitorExprComparison) {
+  TestPredVisitor v;
+  Pred::makeExprComparison(Pred::ComparisonOp::Equality,
+                           Expr::makeInteger("1"), Expr::makeInteger("1"))
+      .accept(v);
+  EXPECT_EQ(v.visited, Pred::PKind::ExprComparison);
+}
+
+TEST(Pred, VisitorForall) {
+  TestPredVisitor v;
+  std::vector<TypedVar> vars = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  Pred::makeForall(vars, Pred::makeTrue()).accept(v);
+  EXPECT_EQ(v.visited, Pred::PKind::Forall);
+}
+
+// --- ComparisonOp to_string ---
+
+TEST(Pred, ComparisonOpToString) {
+  EXPECT_FALSE(Pred::to_string(Pred::ComparisonOp::Equality).empty());
+  EXPECT_FALSE(Pred::to_string(Pred::ComparisonOp::Membership).empty());
+}
diff --git a/tests/test_readBType.cpp b/tests/test_readBType.cpp
new file mode 100644
index 0000000..a1822bf
--- /dev/null
+++ b/tests/test_readBType.cpp
@@ -0,0 +1,498 @@
+#include <gtest/gtest.h>
+
+#include "btypeReader.h"
+#include "tinyxml2.h"
+
+// ============================================================
+// readTypeInfos tests
+// ============================================================
+
+TEST(ReadTypeInfos, NullDomReturnsEmpty) {
+  std::vector<BType> ti;
+  Xml::readTypeInfos(nullptr, ti);
+  EXPECT_TRUE(ti.empty());
+}
+
+TEST(ReadTypeInfos, PrimitiveINTEGER) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Id value="INTEGER"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::INT);
+}
+
+TEST(ReadTypeInfos, PrimitiveFLOAT) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Id value="FLOAT"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::FLOAT);
+}
+
+TEST(ReadTypeInfos, PrimitiveREAL) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Id value="REAL"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::REAL);
+}
+
+TEST(ReadTypeInfos, PrimitiveSTRING) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Id value="STRING"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::STRING);
+}
+
+TEST(ReadTypeInfos, PrimitiveBOOL) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Id value="BOOL"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::BOOL);
+}
+
+TEST(ReadTypeInfos, MultiplePrimitives) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Id value="INTEGER"/></Type>
+      <Type id="1"><Id value="BOOL"/></Type>
+      <Type id="2"><Id value="STRING"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 3u);
+  EXPECT_EQ(ti[0], BType::INT);
+  EXPECT_EQ(ti[1], BType::BOOL);
+  EXPECT_EQ(ti[2], BType::STRING);
+}
+
+TEST(ReadTypeInfos, PowerType) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Unary_Exp op="POW"><Id value="INTEGER"/></Unary_Exp></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::POW(BType::INT));
+}
+
+TEST(ReadTypeInfos, ProductType) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0">
+        <Binary_Exp op="*">
+          <Id value="INTEGER"/>
+          <Id value="BOOL"/>
+        </Binary_Exp>
+      </Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::PROD(BType::INT, BType::BOOL));
+}
+
+TEST(ReadTypeInfos, StructType) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0">
+        <Struct>
+          <Record_Item label="a"><Id value="INTEGER"/></Record_Item>
+          <Record_Item label="b"><Id value="BOOL"/></Record_Item>
+        </Struct>
+      </Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::STRUCT({{"a", BType::INT}, {"b", BType::BOOL}}));
+}
+
+TEST(ReadTypeInfos, AbstractSetFromSets) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <Sets>
+      <Set>
+        <Id value="COLOR"/>
+      </Set>
+    </Sets>
+    <TypeInfos>
+      <Type id="0"><Id value="COLOR"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::ABSTRACT_SET("COLOR"));
+}
+
+TEST(ReadTypeInfos, EnumeratedSetFromSets) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <Sets>
+      <Set>
+        <Id value="COLOR"/>
+        <Enumerated_Values>
+          <Id value="red"/>
+          <Id value="green"/>
+          <Id value="blue"/>
+        </Enumerated_Values>
+      </Set>
+    </Sets>
+    <TypeInfos>
+      <Type id="0"><Id value="COLOR"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0],
+            BType::ENUMERATED_SET({"COLOR", {"red", "green", "blue"}}));
+}
+
+TEST(ReadTypeInfos, SetFromDefine) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <Define>
+      <Set>
+        <Id value="STATUS"/>
+      </Set>
+    </Define>
+    <TypeInfos>
+      <Type id="0"><Id value="STATUS"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::ABSTRACT_SET("STATUS"));
+}
+
+TEST(ReadTypeInfos, NestedPowerProduct) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0">
+        <Unary_Exp op="POW">
+          <Binary_Exp op="*">
+            <Id value="INTEGER"/>
+            <Id value="INTEGER"/>
+          </Binary_Exp>
+        </Unary_Exp>
+      </Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  Xml::readTypeInfos(tiElem, ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::POW(BType::PROD(BType::INT, BType::INT)));
+}
+
+// --- Error cases ---
+
+TEST(ReadTypeInfos, MissingIdAttributeThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type><Id value="INTEGER"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readTypeInfos(tiElem, ti), Xml::BTypeReaderException);
+}
+
+TEST(ReadTypeInfos, NonSequentialIdThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="1"><Id value="INTEGER"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readTypeInfos(tiElem, ti), Xml::BTypeReaderException);
+}
+
+TEST(ReadTypeInfos, UnknownSetNameThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Id value="UNKNOWN_SET"/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readTypeInfos(tiElem, ti), Xml::BTypeReaderException);
+}
+
+TEST(ReadTypeInfos, UnexpectedTagThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Root>
+    <TypeInfos>
+      <Type id="0"><Bogus/></Type>
+    </TypeInfos>
+  </Root>)");
+  auto *tiElem = doc.RootElement()->FirstChildElement("TypeInfos");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readTypeInfos(tiElem, ti), Xml::BTypeReaderException);
+}
+
+// ============================================================
+// readRichTypesInfo tests
+// ============================================================
+
+TEST(ReadRichTypesInfo, NullDomReturnsEmpty) {
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(nullptr, ti);
+  EXPECT_TRUE(ti.empty());
+}
+
+TEST(ReadRichTypesInfo, PrimitiveINTEGER) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><INTEGER/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::INT);
+}
+
+TEST(ReadRichTypesInfo, PrimitiveBOOL) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><BOOL/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::BOOL);
+}
+
+TEST(ReadRichTypesInfo, PrimitiveREAL) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><REAL/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::REAL);
+}
+
+TEST(ReadRichTypesInfo, PrimitiveFLOAT) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><FLOAT/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::FLOAT);
+}
+
+TEST(ReadRichTypesInfo, PrimitiveSTRING) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><STRING/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::STRING);
+}
+
+TEST(ReadRichTypesInfo, AbstractSet) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><AbstractSet id="COLOR"/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0], BType::ABSTRACT_SET("COLOR"));
+}
+
+TEST(ReadRichTypesInfo, EnumeratedSet) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0">
+      <EnumeratedSet id="COLOR">
+        <EnumeratedValue id="red"/>
+        <EnumeratedValue id="green"/>
+        <EnumeratedValue id="blue"/>
+      </EnumeratedSet>
+    </RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 1u);
+  EXPECT_EQ(ti[0],
+            BType::ENUMERATED_SET({"COLOR", {"red", "green", "blue"}}));
+}
+
+TEST(ReadRichTypesInfo, PowerSetRefPrevious) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><INTEGER/></RichType>
+    <RichType id="1"><PowerSet arg="0"/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 2u);
+  EXPECT_EQ(ti[0], BType::INT);
+  EXPECT_EQ(ti[1], BType::POW(BType::INT));
+}
+
+TEST(ReadRichTypesInfo, MultipleMixed) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><INTEGER/></RichType>
+    <RichType id="1"><BOOL/></RichType>
+    <RichType id="2"><AbstractSet id="S"/></RichType>
+    <RichType id="3"><PowerSet arg="0"/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  Xml::readRichTypesInfo(doc.RootElement(), ti);
+  ASSERT_EQ(ti.size(), 4u);
+  EXPECT_EQ(ti[0], BType::INT);
+  EXPECT_EQ(ti[1], BType::BOOL);
+  EXPECT_EQ(ti[2], BType::ABSTRACT_SET("S"));
+  EXPECT_EQ(ti[3], BType::POW(BType::INT));
+}
+
+// --- Error cases ---
+
+TEST(ReadRichTypesInfo, MissingIdAttributeThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType><INTEGER/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
+
+TEST(ReadRichTypesInfo, NonSequentialIdThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="1"><INTEGER/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
+
+TEST(ReadRichTypesInfo, UnexpectedTagThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><Bogus/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
+
+TEST(ReadRichTypesInfo, AbstractSetMissingIdThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><AbstractSet/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
+
+TEST(ReadRichTypesInfo, EnumeratedSetMissingIdThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><EnumeratedSet/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
+
+TEST(ReadRichTypesInfo, EnumeratedValueMissingIdThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0">
+      <EnumeratedSet id="S">
+        <EnumeratedValue/>
+      </EnumeratedSet>
+    </RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
+
+TEST(ReadRichTypesInfo, PowerSetMissingArgThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><PowerSet/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
+
+TEST(ReadRichTypesInfo, PowerSetOutOfRangeArgThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<RichTypesInfo>
+    <RichType id="0"><PowerSet arg="99"/></RichType>
+  </RichTypesInfo>)");
+  std::vector<BType> ti;
+  EXPECT_THROW(Xml::readRichTypesInfo(doc.RootElement(), ti),
+               Xml::BTypeReaderException);
+}
diff --git a/tests/test_readExpr.cpp b/tests/test_readExpr.cpp
new file mode 100644
index 0000000..f2896f7
--- /dev/null
+++ b/tests/test_readExpr.cpp
@@ -0,0 +1,641 @@
+#include <gtest/gtest.h>
+
+#include "exprReader.h"
+#include "exprDesc.h"
+#include "tinyxml2.h"
+
+// typeInfos: [0]=INT, [1]=POW_INT, [2]=BOOL, [3]=POW_BOOL, [4]=STRING,
+//            [5]=REAL, [6]=POW(PROD(INT,INT)), [7]=STRUCT({a:INT,b:INT})
+static const auto structAB =
+    BType::STRUCT({{"a", BType::INT}, {"b", BType::INT}});
+static const std::vector<BType> TI = {
+    BType::INT,                                // 0
+    BType::POW_INT,                            // 1
+    BType::BOOL,                               // 2
+    BType::POW_BOOL,                           // 3
+    BType::STRING,                             // 4
+    BType::REAL,                               // 5
+    BType::POW(BType::PROD(BType::INT, BType::INT)),  // 6
+    structAB,                                  // 7
+};
+
+// --- Literals ---
+
+TEST(ReadExpr, IntegerLiteral) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Integer_Literal value=\"42\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::IntegerLiteral);
+  EXPECT_EQ(e.getIntegerLiteral(), "42");
+}
+
+TEST(ReadExpr, StringLiteral) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<String_Literal value=\"hello\" typref=\"4\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::StringLiteral);
+  EXPECT_EQ(e.getStringLiteral(), "hello");
+}
+
+TEST(ReadExpr, STRING_Literal) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<STRING_Literal value=\"world\" typref=\"4\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::StringLiteral);
+  EXPECT_EQ(e.getStringLiteral(), "world");
+}
+
+TEST(ReadExpr, RealLiteralWithDecimal) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Real_Literal value=\"3.14\" typref=\"5\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::RealLiteral);
+  EXPECT_EQ(e.getRealLiteral().integerPart, "3");
+  EXPECT_EQ(e.getRealLiteral().fractionalPart, "14");
+}
+
+TEST(ReadExpr, RealLiteralIntegerOnly) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Real_Literal value=\"5\" typref=\"5\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::RealLiteral);
+  EXPECT_EQ(e.getRealLiteral().integerPart, "5");
+}
+
+TEST(ReadExpr, BooleanLiteralTrue) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Boolean_Literal value=\"TRUE\" typref=\"2\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::TRUE);
+}
+
+TEST(ReadExpr, BooleanLiteralFalse) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Boolean_Literal value=\"FALSE\" typref=\"2\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::FALSE);
+}
+
+TEST(ReadExpr, BooleanLiteralCaseInsensitive) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Boolean_Literal value=\"true\" typref=\"2\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::TRUE);
+}
+
+// --- Identifiers ---
+
+TEST(ReadExpr, IdPlain) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"x\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Id);
+  EXPECT_EQ(e.getId(), VarName::makeVarWithoutSuffix("x"));
+  EXPECT_EQ(e.getType(), BType::INT);
+}
+
+TEST(ReadExpr, IdWithSuffix) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"x\" suffix=\"1\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Id);
+  EXPECT_EQ(e.getId(), VarName::makeVar("x", 1));
+}
+
+TEST(ReadExpr, IdWithSuffix0) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"x\" suffix=\"0\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Id);
+  EXPECT_EQ(e.getId(), VarName::makeVarWithoutSuffix("x"));
+}
+
+TEST(ReadExpr, FreshId) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Fresh_Id ref=\"f1\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Id);
+  EXPECT_EQ(e.getId(), VarName::makeFreshId("f1"));
+}
+
+TEST(ReadExpr, IdWithRichtypref) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"y\" richtypref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Id);
+  EXPECT_EQ(e.getType(), BType::INT);
+}
+
+// --- Constants ---
+
+TEST(ReadExpr, ConstMAXINT) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"MAXINT\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::MaxInt);
+}
+
+TEST(ReadExpr, ConstMININT) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"MININT\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::MinInt);
+}
+
+TEST(ReadExpr, ConstINTEGER) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"INTEGER\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::INTEGER);
+}
+
+TEST(ReadExpr, ConstNATURAL) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"NATURAL\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::NATURAL);
+}
+
+TEST(ReadExpr, ConstNATURAL1) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"NATURAL1\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::NATURAL1);
+}
+
+TEST(ReadExpr, ConstINT) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"INT\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::INT);
+}
+
+TEST(ReadExpr, ConstNAT) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"NAT\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::NAT);
+}
+
+TEST(ReadExpr, ConstNAT1) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"NAT1\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::NAT1);
+}
+
+TEST(ReadExpr, ConstSTRING) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"STRING\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::STRING);
+}
+
+TEST(ReadExpr, ConstBOOL) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"BOOL\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::BOOL);
+}
+
+TEST(ReadExpr, ConstREAL) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"REAL\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::REAL);
+}
+
+TEST(ReadExpr, ConstFLOAT) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"FLOAT\" typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::FLOAT);
+}
+
+TEST(ReadExpr, ConstTRUE) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"TRUE\" typref=\"2\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::TRUE);
+}
+
+TEST(ReadExpr, ConstFALSE) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"FALSE\" typref=\"2\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::FALSE);
+}
+
+TEST(ReadExpr, ConstSuccessor) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"succ\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Successor);
+}
+
+TEST(ReadExpr, ConstPredecessor) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"pred\" typref=\"0\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Predecessor);
+}
+
+// --- EmptySet / EmptySeq ---
+
+TEST(ReadExpr, EmptySet) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<EmptySet typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::EmptySet);
+  EXPECT_EQ(e.getType(), TI[1]);
+}
+
+TEST(ReadExpr, EmptySeq) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<EmptySeq typref=\"1\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::EmptySet);
+}
+
+// --- Binary expressions ---
+
+TEST(ReadExpr, BinaryExpAddition) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Binary_Exp op="+i" typref="0">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="2" typref="0"/>
+  </Binary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::BinaryExpr);
+  EXPECT_EQ(e.getType(), BType::INT);
+  auto &bin = e.toBinaryExpr();
+  EXPECT_EQ(bin.op, Expr::BinaryOp::IAddition);
+  EXPECT_EQ(bin.lhs.getIntegerLiteral(), "1");
+  EXPECT_EQ(bin.rhs.getIntegerLiteral(), "2");
+}
+
+TEST(ReadExpr, BinaryExpMapplet) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Binary_Exp op="|->" typref="6">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="2" typref="0"/>
+  </Binary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.toBinaryExpr().op, Expr::BinaryOp::Mapplet);
+}
+
+TEST(ReadExpr, BinaryExpInterval) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Binary_Exp op=".." typref="1">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="10" typref="0"/>
+  </Binary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.toBinaryExpr().op, Expr::BinaryOp::Interval);
+}
+
+// --- Unary expressions ---
+
+TEST(ReadExpr, UnaryExpCard) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Unary_Exp op="card" typref="0">
+    <Id value="s" typref="1"/>
+  </Unary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::UnaryExpr);
+  EXPECT_EQ(e.toUnaryExpr().op, Expr::UnaryOp::Cardinality);
+}
+
+TEST(ReadExpr, UnaryExpDom) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Unary_Exp op="dom" typref="1">
+    <Id value="f" typref="6"/>
+  </Unary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.toUnaryExpr().op, Expr::UnaryOp::Domain);
+}
+
+TEST(ReadExpr, UnaryExpSucc) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Unary_Exp op="succ" typref="0">
+    <Integer_Literal value="5" typref="0"/>
+  </Unary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  // succ is rewritten as Application(successor, arg)
+  EXPECT_EQ(e.getTag(), Expr::EKind::BinaryExpr);
+  EXPECT_EQ(e.toBinaryExpr().op, Expr::BinaryOp::Application);
+  EXPECT_EQ(e.toBinaryExpr().lhs.getTag(), Expr::EKind::Successor);
+}
+
+TEST(ReadExpr, UnaryExpPred) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Unary_Exp op="pred" typref="0">
+    <Integer_Literal value="5" typref="0"/>
+  </Unary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::BinaryExpr);
+  EXPECT_EQ(e.toBinaryExpr().op, Expr::BinaryOp::Application);
+  EXPECT_EQ(e.toBinaryExpr().lhs.getTag(), Expr::EKind::Predecessor);
+}
+
+// --- Nary expressions ---
+
+TEST(ReadExpr, NaryExpSet) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Exp op="{" typref="1">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="2" typref="0"/>
+    <Integer_Literal value="3" typref="0"/>
+  </Nary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::NaryExpr);
+  EXPECT_EQ(e.toNaryExpr().op, Expr::NaryOp::Set);
+  EXPECT_EQ(e.toNaryExpr().vec.size(), 3u);
+}
+
+TEST(ReadExpr, NaryExpSequence) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Exp op="[" typref="6">
+    <Integer_Literal value="10" typref="0"/>
+  </Nary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.toNaryExpr().op, Expr::NaryOp::Sequence);
+}
+
+// --- Ternary expressions ---
+
+TEST(ReadExpr, TernaryExpSon) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Ternary_Exp op="son" typref="0">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="2" typref="0"/>
+    <Integer_Literal value="3" typref="0"/>
+  </Ternary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::TernaryExpr);
+  EXPECT_EQ(e.toTernaryExpr().op, Expr::TernaryOp::Son);
+}
+
+TEST(ReadExpr, TernaryExpBin) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Ternary_Exp op="bin" typref="0">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="2" typref="0"/>
+    <Integer_Literal value="3" typref="0"/>
+  </Ternary_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.toTernaryExpr().op, Expr::TernaryOp::Bin);
+}
+
+// --- Quantified expression ---
+
+TEST(ReadExpr, QuantifiedExprLambda) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Exp type="%" typref="6">
+    <Variables>
+      <Id value="x" typref="0"/>
+    </Variables>
+    <Pred>
+      <Exp_Comparison op=":">
+        <Id value="x" typref="0"/>
+        <Id value="INTEGER" typref="1"/>
+      </Exp_Comparison>
+    </Pred>
+    <Body>
+      <Id value="x" typref="0"/>
+    </Body>
+  </Quantified_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::QuantifiedExpr);
+}
+
+TEST(ReadExpr, QuantifiedExprISigma) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Exp type="iSIGMA" typref="0">
+    <Variables>
+      <Id value="x" typref="0"/>
+    </Variables>
+    <Pred>
+      <Exp_Comparison op=":">
+        <Id value="x" typref="0"/>
+        <Id value="NAT" typref="1"/>
+      </Exp_Comparison>
+    </Pred>
+    <Body>
+      <Id value="x" typref="0"/>
+    </Body>
+  </Quantified_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::QuantifiedExpr);
+}
+
+// --- Quantified set ---
+
+TEST(ReadExpr, QuantifiedSet) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Set typref="1">
+    <Variables>
+      <Id value="x" typref="0"/>
+    </Variables>
+    <Body>
+      <Exp_Comparison op="&gt;i">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Body>
+  </Quantified_Set>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::QuantifiedSet);
+}
+
+// --- Boolean expression ---
+
+TEST(ReadExpr, BooleanExp) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Boolean_Exp typref="2">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Boolean_Exp>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::BooleanExpr);
+}
+
+// --- Struct / Record ---
+
+TEST(ReadExpr, Struct) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Struct typref="7">
+    <Record_Item label="a">
+      <Id value="INTEGER" typref="1"/>
+    </Record_Item>
+    <Record_Item label="b">
+      <Id value="INTEGER" typref="1"/>
+    </Record_Item>
+  </Struct>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Struct);
+}
+
+TEST(ReadExpr, Record) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Record typref="7">
+    <Record_Item label="a">
+      <Integer_Literal value="1" typref="0"/>
+    </Record_Item>
+    <Record_Item label="b">
+      <Integer_Literal value="2" typref="0"/>
+    </Record_Item>
+  </Record>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Record);
+}
+
+// --- Record_Field_Access ---
+
+TEST(ReadExpr, RecordFieldAccess) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Record_Field_Access label="a" typref="0">
+    <Id value="r" typref="7"/>
+  </Record_Field_Access>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Record_Field_Access);
+}
+
+// --- Record_Update ---
+
+TEST(ReadExpr, RecordFieldUpdate) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Record_Update label="a" typref="7">
+    <Id value="r" typref="7"/>
+    <Integer_Literal value="99" typref="0"/>
+  </Record_Update>)");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_EQ(e.getTag(), Expr::EKind::Record_Field_Update);
+}
+
+// --- Tag attribute ---
+
+TEST(ReadExpr, TagAttribute) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Integer_Literal value=\"1\" typref=\"0\" tag=\"foo\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  ASSERT_EQ(e.getBxmlTag().size(), 1u);
+  EXPECT_EQ(e.getBxmlTag()[0], "foo");
+}
+
+TEST(ReadExpr, EmptyTagIgnored) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Integer_Literal value=\"1\" typref=\"0\" tag=\"\"/>");
+  auto e = Xml::readExpression(doc.RootElement(), TI);
+  EXPECT_TRUE(e.getBxmlTag().empty());
+}
+
+// --- Error cases ---
+
+TEST(ReadExpr, NullDomThrows) {
+  EXPECT_THROW(Xml::readExpression(nullptr, TI), Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, UnknownTagThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Bogus typref=\"0\"/>");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, MissingTyprefThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Integer_Literal value=\"1\"/>");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, OutOfRangeTyprefThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Integer_Literal value=\"1\" typref=\"999\"/>");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, UnknownBinaryOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Binary_Exp op="???" typref="0">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="2" typref="0"/>
+  </Binary_Exp>)");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, UnknownUnaryOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Unary_Exp op="???" typref="0">
+    <Integer_Literal value="1" typref="0"/>
+  </Unary_Exp>)");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, UnknownNaryOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Exp op="???" typref="0">
+    <Integer_Literal value="1" typref="0"/>
+  </Nary_Exp>)");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, UnknownTernaryOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Ternary_Exp op="???" typref="0">
+    <Integer_Literal value="1" typref="0"/>
+    <Integer_Literal value="2" typref="0"/>
+    <Integer_Literal value="3" typref="0"/>
+  </Ternary_Exp>)");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, UnknownQuantifiedExprTypeThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Exp type="???" typref="0">
+    <Variables><Id value="x" typref="0"/></Variables>
+    <Pred><Exp_Comparison op=":"><Id value="x" typref="0"/><Id value="INTEGER" typref="1"/></Exp_Comparison></Pred>
+    <Body><Id value="x" typref="0"/></Body>
+  </Quantified_Exp>)");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+TEST(ReadExpr, UnknownBooleanLiteralThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Boolean_Literal value=\"MAYBE\" typref=\"2\"/>");
+  EXPECT_THROW(Xml::readExpression(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
+
+// --- VarNameFromId ---
+
+TEST(ReadExpr, VarNameFromIdPlain) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Id value=\"x\" typref=\"0\"/>");
+  auto tv = Xml::VarNameFromId(doc.RootElement(), TI);
+  EXPECT_EQ(tv.name, VarName::makeVarWithoutSuffix("x"));
+  EXPECT_EQ(tv.type, BType::INT);
+}
+
+TEST(ReadExpr, VarNameFromIdFresh) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Fresh_Id ref=\"f1\" typref=\"0\"/>");
+  auto tv = Xml::VarNameFromId(doc.RootElement(), TI);
+  EXPECT_EQ(tv.name, VarName::makeFreshId("f1"));
+}
+
+TEST(ReadExpr, VarNameFromIdBadTagThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Bogus typref=\"0\"/>");
+  EXPECT_THROW(Xml::VarNameFromId(doc.RootElement(), TI),
+               Xml::ExprReaderException);
+}
diff --git a/tests/test_readPred.cpp b/tests/test_readPred.cpp
new file mode 100644
index 0000000..42f69f7
--- /dev/null
+++ b/tests/test_readPred.cpp
@@ -0,0 +1,379 @@
+#include <gtest/gtest.h>
+
+#include "predReader.h"
+#include "predDesc.h"
+#include "tinyxml2.h"
+
+// typeInfos: [0]=INT, [1]=POW_INT
+static const std::vector<BType> TI = {
+    BType::INT,      // 0
+    BType::POW_INT,  // 1
+};
+
+// --- Exp_Comparison ---
+
+TEST(ReadPred, ComparisonEquality) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="=">
+    <Id value="x" typref="0"/>
+    <Integer_Literal value="0" typref="0"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::ExprComparison);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Equality);
+}
+
+TEST(ReadPred, ComparisonMembership) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op=":">
+    <Id value="x" typref="0"/>
+    <Id value="INTEGER" typref="1"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Membership);
+}
+
+TEST(ReadPred, ComparisonSubset) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="&lt;:">
+    <Id value="s" typref="1"/>
+    <Id value="INTEGER" typref="1"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Subset);
+}
+
+TEST(ReadPred, ComparisonStrictSubset) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="&lt;&lt;:">
+    <Id value="s" typref="1"/>
+    <Id value="INTEGER" typref="1"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Strict_Subset);
+}
+
+TEST(ReadPred, ComparisonIgt) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="&gt;i">
+    <Id value="x" typref="0"/>
+    <Integer_Literal value="0" typref="0"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Igt);
+}
+
+TEST(ReadPred, ComparisonIlt) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="&lt;i">
+    <Id value="x" typref="0"/>
+    <Integer_Literal value="0" typref="0"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Ilt);
+}
+
+TEST(ReadPred, ComparisonIge) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="&gt;=i">
+    <Id value="x" typref="0"/>
+    <Integer_Literal value="0" typref="0"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Ige);
+}
+
+TEST(ReadPred, ComparisonIle) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="&lt;=i">
+    <Id value="x" typref="0"/>
+    <Integer_Literal value="0" typref="0"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Ile);
+}
+
+// --- Negated comparisons ---
+
+TEST(ReadPred, NegatedMembership) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="/:">
+    <Id value="x" typref="0"/>
+    <Id value="INTEGER" typref="1"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Negation);
+  auto &inner = p.toNegation().operand;
+  EXPECT_EQ(inner.getTag(), Pred::PKind::ExprComparison);
+  EXPECT_EQ(inner.toExprComparison().op, Pred::ComparisonOp::Membership);
+}
+
+TEST(ReadPred, NegatedSubset) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="/&lt;:">
+    <Id value="s" typref="1"/>
+    <Id value="INTEGER" typref="1"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Negation);
+  EXPECT_EQ(p.toNegation().operand.toExprComparison().op,
+            Pred::ComparisonOp::Subset);
+}
+
+TEST(ReadPred, NegatedStrictSubset) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="/&lt;&lt;:">
+    <Id value="s" typref="1"/>
+    <Id value="INTEGER" typref="1"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Negation);
+  EXPECT_EQ(p.toNegation().operand.toExprComparison().op,
+            Pred::ComparisonOp::Strict_Subset);
+}
+
+TEST(ReadPred, NegatedEquality) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="/=">
+    <Id value="x" typref="0"/>
+    <Integer_Literal value="0" typref="0"/>
+  </Exp_Comparison>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Negation);
+  EXPECT_EQ(p.toNegation().operand.toExprComparison().op,
+            Pred::ComparisonOp::Equality);
+}
+
+// --- Binary predicates ---
+
+TEST(ReadPred, Implication) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Binary_Pred op="=&gt;">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Binary_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Implication);
+}
+
+TEST(ReadPred, Equivalence) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Binary_Pred op="&lt;=&gt;">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Binary_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Equivalence);
+}
+
+// --- Unary predicate ---
+
+TEST(ReadPred, Negation) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Unary_Pred op="not">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Unary_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Negation);
+}
+
+// --- Nary predicates ---
+
+TEST(ReadPred, Conjunction) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Pred op="&amp;">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="1" typref="0"/>
+    </Exp_Comparison>
+  </Nary_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Conjunction);
+  EXPECT_EQ(p.toConjunction().operands.size(), 2u);
+}
+
+TEST(ReadPred, Disjunction) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Pred op="or">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="1" typref="0"/>
+    </Exp_Comparison>
+  </Nary_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Disjunction);
+  EXPECT_EQ(p.toDisjunction().operands.size(), 2u);
+}
+
+// --- Quantified predicates ---
+
+TEST(ReadPred, Forall) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Pred type="!">
+    <Variables>
+      <Id value="x" typref="0"/>
+    </Variables>
+    <Body>
+      <Exp_Comparison op="&gt;i">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Body>
+  </Quantified_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Forall);
+  EXPECT_EQ(p.toForall().vars.size(), 1u);
+}
+
+TEST(ReadPred, Exists) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Pred type="#">
+    <Variables>
+      <Id value="x" typref="0"/>
+    </Variables>
+    <Body>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="42" typref="0"/>
+      </Exp_Comparison>
+    </Body>
+  </Quantified_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Exists);
+  EXPECT_EQ(p.toExists().vars.size(), 1u);
+}
+
+TEST(ReadPred, ForallMultipleVars) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Pred type="!">
+    <Variables>
+      <Id value="x" typref="0"/>
+      <Id value="y" typref="0"/>
+    </Variables>
+    <Body>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Id value="y" typref="0"/>
+      </Exp_Comparison>
+    </Body>
+  </Quantified_Pred>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::Forall);
+  EXPECT_EQ(p.toForall().vars.size(), 2u);
+}
+
+// --- Tag wrapper ---
+
+TEST(ReadPred, TagWrapper) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Tag>
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Tag>)");
+  auto p = Xml::readPredicate(doc.RootElement(), TI);
+  EXPECT_EQ(p.getTag(), Pred::PKind::ExprComparison);
+  EXPECT_EQ(p.toExprComparison().op, Pred::ComparisonOp::Equality);
+}
+
+// --- Error cases ---
+
+TEST(ReadPred, NullDomThrows) {
+  EXPECT_THROW(Xml::readPredicate(nullptr, TI), Xml::PredReaderException);
+}
+
+TEST(ReadPred, UnknownTagThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Bogus/>");
+  EXPECT_THROW(Xml::readPredicate(doc.RootElement(), TI),
+               Xml::PredReaderException);
+}
+
+TEST(ReadPred, UnknownBinaryPredOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Binary_Pred op="???">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Binary_Pred>)");
+  EXPECT_THROW(Xml::readPredicate(doc.RootElement(), TI),
+               Xml::PredReaderException);
+}
+
+TEST(ReadPred, UnknownComparisonOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Exp_Comparison op="???">
+    <Id value="x" typref="0"/>
+    <Integer_Literal value="0" typref="0"/>
+  </Exp_Comparison>)");
+  EXPECT_THROW(Xml::readPredicate(doc.RootElement(), TI),
+               Xml::PredReaderException);
+}
+
+TEST(ReadPred, UnknownUnaryPredOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Unary_Pred op="???">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Unary_Pred>)");
+  EXPECT_THROW(Xml::readPredicate(doc.RootElement(), TI),
+               Xml::PredReaderException);
+}
+
+TEST(ReadPred, UnknownNaryPredOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Pred op="???">
+    <Exp_Comparison op="=">
+      <Id value="x" typref="0"/>
+      <Integer_Literal value="0" typref="0"/>
+    </Exp_Comparison>
+  </Nary_Pred>)");
+  EXPECT_THROW(Xml::readPredicate(doc.RootElement(), TI),
+               Xml::PredReaderException);
+}
+
+TEST(ReadPred, UnknownQuantifiedPredTypeThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Quantified_Pred type="???">
+    <Variables><Id value="x" typref="0"/></Variables>
+    <Body>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Body>
+  </Quantified_Pred>)");
+  EXPECT_THROW(Xml::readPredicate(doc.RootElement(), TI),
+               Xml::PredReaderException);
+}
diff --git a/tests/test_readSubst.cpp b/tests/test_readSubst.cpp
new file mode 100644
index 0000000..137179f
--- /dev/null
+++ b/tests/test_readSubst.cpp
@@ -0,0 +1,600 @@
+#include <gtest/gtest.h>
+
+#include "substReader.h"
+#include "tinyxml2.h"
+
+// typeInfos: [0]=INT, [1]=POW_INT
+static const std::vector<BType> TI = {BType::INT, BType::POW_INT};
+
+// ============================================================
+// Skip / Block
+// ============================================================
+
+TEST(ReadSubst, Skip) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Skip/>");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Skip);
+}
+
+TEST(ReadSubst, Block) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Bloc_Sub><Skip/></Bloc_Sub>");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Block);
+  EXPECT_EQ(s.toBlock().getTag(), Subst::SKind::Skip);
+}
+
+// ============================================================
+// Assert / PRE
+// ============================================================
+
+TEST(ReadSubst, AssertSub) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Assert_Sub>
+    <Guard>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Guard>
+    <Body><Skip/></Body>
+  </Assert_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Assert);
+  EXPECT_EQ(s.toAssert().condition.getTag(), Pred::PKind::ExprComparison);
+  EXPECT_EQ(s.toAssert().content.getTag(), Subst::SKind::Skip);
+}
+
+TEST(ReadSubst, PreSub) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<PRE_Sub>
+    <Precondition>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Precondition>
+    <Body><Skip/></Body>
+  </PRE_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Assert);
+}
+
+// ============================================================
+// IfThen / IfThenElse
+// ============================================================
+
+TEST(ReadSubst, IfThen) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<If_Sub>
+    <Condition>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Condition>
+    <Then><Skip/></Then>
+  </If_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::IfThen);
+}
+
+TEST(ReadSubst, IfThenElse) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<If_Sub>
+    <Condition>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Condition>
+    <Then><Skip/></Then>
+    <Else><Skip/></Else>
+  </If_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::IfThenElse);
+  EXPECT_EQ(s.toIfThenElse().s_if.getTag(), Subst::SKind::Skip);
+  EXPECT_EQ(s.toIfThenElse().s_else.getTag(), Subst::SKind::Skip);
+}
+
+// ============================================================
+// SimpleAssignment
+// ============================================================
+
+TEST(ReadSubst, SimpleAssignment) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Simple_Assignement_Sub>
+    <Variables>
+      <Id value="x" typref="0"/>
+    </Variables>
+    <Values>
+      <Integer_Literal value="42" typref="0"/>
+    </Values>
+  </Simple_Assignement_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::SimpleAssignment);
+  auto &sa = s.toSimpleAssignment();
+  ASSERT_EQ(sa.vars.size(), 1u);
+  EXPECT_EQ(sa.vars[0].name, VarName::makeVarWithoutSuffix("x"));
+  ASSERT_EQ(sa.exprs.size(), 1u);
+  EXPECT_EQ(sa.exprs[0].getTag(), Expr::EKind::IntegerLiteral);
+}
+
+TEST(ReadSubst, SimpleAssignmentMultiple) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Simple_Assignement_Sub>
+    <Variables>
+      <Id value="x" typref="0"/>
+      <Id value="y" typref="0"/>
+    </Variables>
+    <Values>
+      <Integer_Literal value="1" typref="0"/>
+      <Integer_Literal value="2" typref="0"/>
+    </Values>
+  </Simple_Assignement_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.toSimpleAssignment().vars.size(), 2u);
+  EXPECT_EQ(s.toSimpleAssignment().exprs.size(), 2u);
+}
+
+// ============================================================
+// Select / SelectElse
+// ============================================================
+
+TEST(ReadSubst, Select) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Select>
+    <When_Clauses>
+      <When>
+        <Condition>
+          <Exp_Comparison op="=">
+            <Id value="x" typref="0"/>
+            <Integer_Literal value="0" typref="0"/>
+          </Exp_Comparison>
+        </Condition>
+        <Then><Skip/></Then>
+      </When>
+    </When_Clauses>
+  </Select>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Select);
+  EXPECT_EQ(s.toSelect().clauses.size(), 1u);
+}
+
+TEST(ReadSubst, SelectElse) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Select>
+    <When_Clauses>
+      <When>
+        <Condition>
+          <Exp_Comparison op="=">
+            <Id value="x" typref="0"/>
+            <Integer_Literal value="0" typref="0"/>
+          </Exp_Comparison>
+        </Condition>
+        <Then><Skip/></Then>
+      </When>
+    </When_Clauses>
+    <Else><Skip/></Else>
+  </Select>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::SelectElse);
+}
+
+// ============================================================
+// Case / CaseElse
+// ============================================================
+
+TEST(ReadSubst, Case) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Case_Sub>
+    <Value><Id value="x" typref="0"/></Value>
+    <Choices>
+      <Choice>
+        <Value><Integer_Literal value="1" typref="0"/></Value>
+        <Then><Skip/></Then>
+      </Choice>
+      <Choice>
+        <Value><Integer_Literal value="2" typref="0"/></Value>
+        <Then><Skip/></Then>
+      </Choice>
+    </Choices>
+  </Case_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Case);
+  EXPECT_EQ(s.toCase().m_cases.size(), 2u);
+}
+
+TEST(ReadSubst, CaseElse) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Case_Sub>
+    <Value><Id value="x" typref="0"/></Value>
+    <Choices>
+      <Choice>
+        <Value><Integer_Literal value="1" typref="0"/></Value>
+        <Then><Skip/></Then>
+      </Choice>
+    </Choices>
+    <Else><Skip/></Else>
+  </Case_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::CaseElse);
+}
+
+// ============================================================
+// Any
+// ============================================================
+
+TEST(ReadSubst, Any) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<ANY_Sub>
+    <Variables>
+      <Id value="x" typref="0"/>
+    </Variables>
+    <Pred>
+      <Exp_Comparison op=":">
+        <Id value="x" typref="0"/>
+        <Id value="INTEGER" typref="1"/>
+      </Exp_Comparison>
+    </Pred>
+    <Then><Skip/></Then>
+  </ANY_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Any);
+  EXPECT_EQ(s.toAny().vars.size(), 1u);
+  EXPECT_EQ(s.toAny().body.getTag(), Subst::SKind::Skip);
+}
+
+// ============================================================
+// While
+// ============================================================
+
+TEST(ReadSubst, While) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<While>
+    <Condition>
+      <Exp_Comparison op="&gt;i">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Condition>
+    <Body>
+      <Simple_Assignement_Sub>
+        <Variables><Id value="x" typref="0"/></Variables>
+        <Values>
+          <Binary_Exp op="-i" typref="0">
+            <Id value="x" typref="0"/>
+            <Integer_Literal value="1" typref="0"/>
+          </Binary_Exp>
+        </Values>
+      </Simple_Assignement_Sub>
+    </Body>
+    <Invariant>
+      <Exp_Comparison op="&gt;=i">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Invariant>
+    <Variant>
+      <Id value="x" typref="0"/>
+    </Variant>
+  </While>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::While);
+  auto &w = s.toWhile();
+  EXPECT_EQ(w.body.getTag(), Subst::SKind::SimpleAssignment);
+}
+
+// ============================================================
+// Nary_Sub: Sequence, Parallel, Choice
+// ============================================================
+
+TEST(ReadSubst, Sequence) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Sub op=";">
+    <Skip/>
+    <Skip/>
+  </Nary_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Sequence);
+  EXPECT_EQ(s.toSequence().size(), 2u);
+}
+
+TEST(ReadSubst, Parallel) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Sub op="||">
+    <Skip/>
+    <Skip/>
+    <Skip/>
+  </Nary_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Parallel);
+  EXPECT_EQ(s.toParallel().size(), 3u);
+}
+
+TEST(ReadSubst, Choice) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Sub op="CHOICE">
+    <Skip/>
+    <Skip/>
+  </Nary_Sub>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Choice);
+  EXPECT_EQ(s.toChoice().size(), 2u);
+}
+
+// ============================================================
+// Witness
+// ============================================================
+
+TEST(ReadSubst, WitnessSingle) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Witness>
+    <Witnesses>
+      <Exp_Comparison op="=">
+        <Id value="w" typref="0"/>
+        <Integer_Literal value="42" typref="0"/>
+      </Exp_Comparison>
+    </Witnesses>
+    <Body><Skip/></Body>
+  </Witness>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Witness);
+  auto &wt = s.toWitness();
+  EXPECT_EQ(wt.witnesses.size(), 1u);
+  EXPECT_TRUE(wt.witnesses.count("w"));
+  EXPECT_EQ(wt.body.getTag(), Subst::SKind::Skip);
+}
+
+TEST(ReadSubst, WitnessMultiple) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Witness>
+    <Witnesses>
+      <Nary_Pred op="&amp;">
+        <Exp_Comparison op="=">
+          <Id value="a" typref="0"/>
+          <Integer_Literal value="1" typref="0"/>
+        </Exp_Comparison>
+        <Exp_Comparison op="=">
+          <Id value="b" typref="0"/>
+          <Integer_Literal value="2" typref="0"/>
+        </Exp_Comparison>
+      </Nary_Pred>
+    </Witnesses>
+    <Body><Skip/></Body>
+  </Witness>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::Witness);
+  EXPECT_EQ(s.toWitness().witnesses.size(), 2u);
+  EXPECT_TRUE(s.toWitness().witnesses.count("a"));
+  EXPECT_TRUE(s.toWitness().witnesses.count("b"));
+}
+
+// ============================================================
+// OperationCall
+// ============================================================
+
+TEST(ReadSubst, OperationCallNoParams) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Operation_Call>
+    <Name><Id value="op1" typref="0"/></Name>
+    <Operation name="op1">
+      <Body><Skip/></Body>
+    </Operation>
+  </Operation_Call>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::OperationCall);
+  EXPECT_EQ(s.toOpCall().name, "op1");
+}
+
+TEST(ReadSubst, OperationCallWithParams) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Operation_Call>
+    <Name><Id value="op2" typref="0"/></Name>
+    <Input_Parameters>
+      <Integer_Literal value="5" typref="0"/>
+    </Input_Parameters>
+    <Output_Parameters>
+      <Id value="r" typref="0"/>
+    </Output_Parameters>
+    <Operation name="op2">
+      <Input_Parameters>
+        <Id value="p" typref="0"/>
+      </Input_Parameters>
+      <Output_Parameters>
+        <Id value="q" typref="0"/>
+      </Output_Parameters>
+      <Body><Skip/></Body>
+    </Operation>
+  </Operation_Call>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.getTag(), Subst::SKind::OperationCall);
+  auto &oc = s.toOpCall();
+  EXPECT_EQ(oc.name, "op2");
+  EXPECT_EQ(oc.input.size(), 1u);
+  EXPECT_EQ(oc.output.size(), 1u);
+  EXPECT_EQ(oc.op_input.size(), 1u);
+  EXPECT_EQ(oc.op_output.size(), 1u);
+}
+
+TEST(ReadSubst, OperationCallWithPrecondition) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Operation_Call>
+    <Name><Id value="op3" typref="0"/></Name>
+    <Operation name="op3">
+      <Precondition>
+        <Exp_Comparison op="=">
+          <Id value="x" typref="0"/>
+          <Integer_Literal value="0" typref="0"/>
+        </Exp_Comparison>
+      </Precondition>
+      <Body><Skip/></Body>
+    </Operation>
+  </Operation_Call>)");
+  auto s = Xml::readSubstitution(doc.RootElement(), TI);
+  EXPECT_EQ(s.toOpCall().op_precondition.getTag(), Pred::PKind::ExprComparison);
+}
+
+// ============================================================
+// Error cases
+// ============================================================
+
+TEST(ReadSubst, NullDomThrows) {
+  EXPECT_THROW(Xml::readSubstitution(nullptr, TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, UnknownTagThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Bogus/>");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, UnknownNaryOpThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Nary_Sub op="???"><Skip/></Nary_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, AssertMissingGuardThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Assert_Sub><Body><Skip/></Body></Assert_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, AssertMissingBodyThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Assert_Sub>
+    <Guard>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Guard>
+  </Assert_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, PreSubMissingPreconditionThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<PRE_Sub><Body><Skip/></Body></PRE_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, IfSubMissingConditionThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<If_Sub><Then><Skip/></Then></If_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, IfSubMissingThenThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<If_Sub>
+    <Condition>
+      <Exp_Comparison op="=">
+        <Id value="x" typref="0"/>
+        <Integer_Literal value="0" typref="0"/>
+      </Exp_Comparison>
+    </Condition>
+  </If_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, SimpleAssignmentMissingVariablesThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Simple_Assignement_Sub>
+    <Values><Integer_Literal value="1" typref="0"/></Values>
+  </Simple_Assignement_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, SimpleAssignmentMissingValuesThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Simple_Assignement_Sub>
+    <Variables><Id value="x" typref="0"/></Variables>
+  </Simple_Assignement_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, SelectMissingWhenClausesThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse("<Select/>");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, AnyMissingVariablesThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<ANY_Sub>
+    <Pred><Exp_Comparison op=":"><Id value="x" typref="0"/><Id value="INTEGER" typref="1"/></Exp_Comparison></Pred>
+    <Then><Skip/></Then>
+  </ANY_Sub>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, WhileMissingConditionThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<While>
+    <Body><Skip/></Body>
+    <Invariant><Exp_Comparison op="="><Id value="x" typref="0"/><Integer_Literal value="0" typref="0"/></Exp_Comparison></Invariant>
+    <Variant><Id value="x" typref="0"/></Variant>
+  </While>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, OperationCallMissingNameThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Operation_Call>
+    <Operation name="op"><Body><Skip/></Body></Operation>
+  </Operation_Call>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, OperationCallParamMismatchThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Operation_Call>
+    <Name><Id value="op" typref="0"/></Name>
+    <Input_Parameters>
+      <Integer_Literal value="1" typref="0"/>
+      <Integer_Literal value="2" typref="0"/>
+    </Input_Parameters>
+    <Operation name="op">
+      <Input_Parameters>
+        <Id value="p" typref="0"/>
+      </Input_Parameters>
+      <Body><Skip/></Body>
+    </Operation>
+  </Operation_Call>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, WitnessMissingWitnessesThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Witness><Body><Skip/></Body></Witness>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
+
+TEST(ReadSubst, WitnessBadChildThrows) {
+  tinyxml2::XMLDocument doc;
+  doc.Parse(R"(<Witness>
+    <Witnesses><Bogus/></Witnesses>
+    <Body><Skip/></Body>
+  </Witness>)");
+  EXPECT_THROW(Xml::readSubstitution(doc.RootElement(), TI),
+               Xml::SubstReaderException);
+}
diff --git a/tests/test_subst.cpp b/tests/test_subst.cpp
new file mode 100644
index 0000000..dba6885
--- /dev/null
+++ b/tests/test_subst.cpp
@@ -0,0 +1,661 @@
+#include "subst.h"
+
+#include <gtest/gtest.h>
+
+// ---------------------------------------------------------------------------
+// Helpers
+// ---------------------------------------------------------------------------
+
+static TypedVar tv(const std::string &name, BType type) {
+  return TypedVar{VarName::makeVarWithoutSuffix(name), std::move(type)};
+}
+
+static Expr ident(const std::string &name, BType type) {
+  return Expr::makeIdent(VarName::makeVarWithoutSuffix(name), std::move(type));
+}
+
+// Build a simple assignment: vars := exprs
+static Subst simpleAssign(const std::string &var, BType ty,
+                           const std::string &rhs) {
+  std::vector<TypedVar> vars;
+  vars.push_back(tv(var, ty));
+  std::vector<Expr> exprs;
+  exprs.push_back(ident(rhs, ty));
+  return Subst::makeSimpleAssignment(vars, std::move(exprs));
+}
+
+// ===========================================================================
+// Default constructor
+// ===========================================================================
+
+TEST(SubstDefault, DefaultIsSkip) {
+  Subst s;
+  EXPECT_EQ(s.getTag(), Subst::SKind::Skip);
+}
+
+// ===========================================================================
+// Construction & getTag
+// ===========================================================================
+
+TEST(SubstConstruction, Skip) {
+  auto s = Subst::makeSkip();
+  EXPECT_EQ(s.getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstConstruction, Block) {
+  auto s = Subst::makeBlock(Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::Block);
+  EXPECT_EQ(s.toBlock().getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstConstruction, Assert) {
+  auto s = Subst::makeAssert(Pred::makeTrue(), Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::Assert);
+  EXPECT_EQ(s.toAssert().content.getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstConstruction, IfThen) {
+  auto s = Subst::makeIfThen(Pred::makeTrue(), Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::IfThen);
+  EXPECT_EQ(s.toIfThen().s_if.getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstConstruction, IfThenElse) {
+  auto s = Subst::makeIfThenElse(Pred::makeTrue(), Subst::makeSkip(),
+                                  Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::IfThenElse);
+  EXPECT_EQ(s.toIfThenElse().s_if.getTag(), Subst::SKind::Skip);
+  EXPECT_EQ(s.toIfThenElse().s_else.getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstConstruction, SimpleAssignment) {
+  std::vector<TypedVar> vars;
+  vars.push_back(tv("x", BType::INT));
+  std::vector<Expr> exprs;
+  exprs.push_back(Expr::makeInteger("1"));
+  auto s = Subst::makeSimpleAssignment(vars, std::move(exprs));
+  EXPECT_EQ(s.getTag(), Subst::SKind::SimpleAssignment);
+  EXPECT_EQ(s.toSimpleAssignment().vars.size(), 1u);
+  EXPECT_EQ(s.toSimpleAssignment().exprs.size(), 1u);
+}
+
+TEST(SubstConstruction, Select) {
+  std::vector<std::pair<Pred, Subst>> clauses;
+  clauses.push_back({Pred::makeTrue(), Subst::makeSkip()});
+  auto s = Subst::makeSelect(std::move(clauses));
+  EXPECT_EQ(s.getTag(), Subst::SKind::Select);
+  EXPECT_EQ(s.toSelect().clauses.size(), 1u);
+}
+
+TEST(SubstConstruction, SelectElse) {
+  std::vector<std::pair<Pred, Subst>> clauses;
+  clauses.push_back({Pred::makeTrue(), Subst::makeSkip()});
+  auto s = Subst::makeSelectElse(std::move(clauses), Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::SelectElse);
+  EXPECT_EQ(s.toSelectElse().clauses.size(), 1u);
+  EXPECT_EQ(s.toSelectElse().s_else.getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstConstruction, Case) {
+  std::vector<Subst::CaseChoice> cases;
+  Subst::CaseChoice ch;
+  ch.values.push_back(Expr::makeInteger("1"));
+  ch.body = Subst::makeSkip();
+  cases.push_back(std::move(ch));
+  auto s = Subst::makeCase(ident("x", BType::INT), std::move(cases));
+  EXPECT_EQ(s.getTag(), Subst::SKind::Case);
+  EXPECT_EQ(s.toCase().m_cases.size(), 1u);
+}
+
+TEST(SubstConstruction, CaseElse) {
+  std::vector<Subst::CaseChoice> cases;
+  Subst::CaseChoice ch;
+  ch.values.push_back(Expr::makeInteger("1"));
+  ch.body = Subst::makeSkip();
+  cases.push_back(std::move(ch));
+  auto s = Subst::makeCaseElse(ident("x", BType::INT), std::move(cases),
+                                Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::CaseElse);
+  EXPECT_EQ(s.toCaseElse().m_cases.size(), 1u);
+  EXPECT_EQ(s.toCaseElse().m_else.getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstConstruction, Any) {
+  std::vector<TypedVar> vars;
+  vars.push_back(tv("x", BType::INT));
+  auto s = Subst::makeAny(vars, Pred::makeTrue(), Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::Any);
+  EXPECT_EQ(s.toAny().vars.size(), 1u);
+}
+
+TEST(SubstConstruction, OpCall) {
+  std::vector<Expr> input;
+  input.push_back(Expr::makeInteger("1"));
+  std::vector<TypedVar> output;
+  output.push_back(tv("r", BType::INT));
+  std::vector<TypedVar> op_input;
+  op_input.push_back(tv("p", BType::INT));
+  std::vector<TypedVar> op_output;
+  op_output.push_back(tv("q", BType::INT));
+  auto s = Subst::makeOpCall("myOp", std::move(input), output, op_input,
+                              op_output, Pred::makeTrue(), Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::OperationCall);
+  EXPECT_EQ(s.toOpCall().name, "myOp");
+  EXPECT_EQ(s.toOpCall().input.size(), 1u);
+  EXPECT_EQ(s.toOpCall().output.size(), 1u);
+}
+
+TEST(SubstConstruction, While) {
+  auto s = Subst::makeWhile(Pred::makeTrue(), Subst::makeSkip(),
+                             Pred::makeTrue(), Expr::makeInteger("0"));
+  EXPECT_EQ(s.getTag(), Subst::SKind::While);
+}
+
+TEST(SubstConstruction, Witness) {
+  std::map<std::string, Expr> witnesses;
+  witnesses.emplace("w", Expr::makeInteger("42"));
+  auto s = Subst::makeWitness(std::move(witnesses), Subst::makeSkip());
+  EXPECT_EQ(s.getTag(), Subst::SKind::Witness);
+  EXPECT_EQ(s.toWitness().witnesses.size(), 1u);
+}
+
+TEST(SubstConstruction, Sequence) {
+  std::vector<Subst> vec;
+  vec.push_back(Subst::makeSkip());
+  vec.push_back(Subst::makeSkip());
+  auto s = Subst::makeSequence(std::move(vec));
+  EXPECT_EQ(s.getTag(), Subst::SKind::Sequence);
+  EXPECT_EQ(s.toSequence().size(), 2u);
+}
+
+TEST(SubstConstruction, Parallel) {
+  std::vector<Subst> vec;
+  vec.push_back(Subst::makeSkip());
+  auto s = Subst::makeParallel(std::move(vec));
+  EXPECT_EQ(s.getTag(), Subst::SKind::Parallel);
+  EXPECT_EQ(s.toParallel().size(), 1u);
+}
+
+TEST(SubstConstruction, Choice) {
+  std::vector<Subst> vec;
+  vec.push_back(Subst::makeSkip());
+  vec.push_back(Subst::makeSkip());
+  vec.push_back(Subst::makeSkip());
+  auto s = Subst::makeChoice(std::move(vec));
+  EXPECT_EQ(s.getTag(), Subst::SKind::Choice);
+  EXPECT_EQ(s.toChoice().size(), 3u);
+}
+
+// ===========================================================================
+// Copy
+// ===========================================================================
+
+TEST(SubstCopy, SkipCopy) {
+  auto s = Subst::makeSkip();
+  auto c = s.copy();
+  EXPECT_EQ(c.getTag(), Subst::SKind::Skip);
+}
+
+TEST(SubstCopy, AssignmentCopy) {
+  auto s = simpleAssign("x", BType::INT, "y");
+  auto c = s.copy();
+  EXPECT_EQ(c.getTag(), Subst::SKind::SimpleAssignment);
+  EXPECT_EQ(c.toSimpleAssignment().vars.size(), 1u);
+  EXPECT_EQ(c.toSimpleAssignment().exprs.size(), 1u);
+}
+
+TEST(SubstCopy, NestedCopy) {
+  auto s = Subst::makeIfThenElse(
+      Pred::makeTrue(), simpleAssign("x", BType::INT, "y"),
+      simpleAssign("x", BType::INT, "z"));
+  auto c = s.copy();
+  EXPECT_EQ(c.getTag(), Subst::SKind::IfThenElse);
+  EXPECT_EQ(c.toIfThenElse().s_if.getTag(), Subst::SKind::SimpleAssignment);
+  EXPECT_EQ(c.toIfThenElse().s_else.getTag(), Subst::SKind::SimpleAssignment);
+}
+
+// ===========================================================================
+// getFreeVars
+// ===========================================================================
+
+TEST(SubstFreeVars, SkipEmpty) {
+  auto fv = Subst::makeSkip().getFreeVars();
+  EXPECT_TRUE(fv.empty());
+}
+
+TEST(SubstFreeVars, AssignmentFreeVars) {
+  // x := y  — both x and y are free (no bound context)
+  // But SimpleAssignmentSubst::getFreeVars adds LHS only if in boundVars,
+  // so with empty boundVars, only RHS contributes.
+  auto s = simpleAssign("x", BType::INT, "y");
+  auto fv = s.getFreeVars();
+  EXPECT_EQ(fv.count(VarName::makeVarWithoutSuffix("y")), 1u);
+  // x is NOT free when called with empty boundVars
+  EXPECT_EQ(fv.count(VarName::makeVarWithoutSuffix("x")), 0u);
+}
+
+TEST(SubstFreeVars, AssignmentLhsFreeWhenBound) {
+  // When x is in boundVars, SimpleAssignment's getFreeVars adds it
+  auto s = simpleAssign("x", BType::INT, "y");
+  std::set<VarName> bound;
+  bound.insert(VarName::makeVarWithoutSuffix("x"));
+  std::set<VarName> accu;
+  s.getFreeVars(bound, accu);
+  EXPECT_EQ(accu.count(VarName::makeVarWithoutSuffix("x")), 1u);
+  EXPECT_EQ(accu.count(VarName::makeVarWithoutSuffix("y")), 1u);
+}
+
+TEST(SubstFreeVars, IfThenUnion) {
+  // IF p(a) THEN x := b END
+  auto cond = Pred::makeExprComparison(Pred::ComparisonOp::Equality,
+                                        ident("a", BType::INT),
+                                        Expr::makeInteger("0"));
+  auto body = simpleAssign("x", BType::INT, "b");
+  auto s = Subst::makeIfThen(std::move(cond), std::move(body));
+  auto fv = s.getFreeVars();
+  EXPECT_EQ(fv.count(VarName::makeVarWithoutSuffix("a")), 1u);
+  EXPECT_EQ(fv.count(VarName::makeVarWithoutSuffix("b")), 1u);
+}
+
+TEST(SubstFreeVars, AnyBindsVars) {
+  // ANY x WHERE x=1 THEN skip END
+  // x is bound, not free
+  std::vector<TypedVar> vars;
+  vars.push_back(tv("x", BType::INT));
+  auto pred = Pred::makeExprComparison(Pred::ComparisonOp::Equality,
+                                        ident("x", BType::INT),
+                                        Expr::makeInteger("1"));
+  auto s = Subst::makeAny(vars, std::move(pred), Subst::makeSkip());
+  auto fv = s.getFreeVars();
+  EXPECT_EQ(fv.count(VarName::makeVarWithoutSuffix("x")), 0u);
+}
+
+// ===========================================================================
+// getAllVars
+// ===========================================================================
+
+TEST(SubstAllVars, SkipEmpty) {
+  auto av = Subst::makeSkip().getAllVars();
+  EXPECT_TRUE(av.empty());
+}
+
+TEST(SubstAllVars, Assignment) {
+  auto s = simpleAssign("x", BType::INT, "y");
+  auto av = s.getAllVars();
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("x")), 1u);
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("y")), 1u);
+}
+
+TEST(SubstAllVars, AnyIncludesBound) {
+  std::vector<TypedVar> vars;
+  vars.push_back(tv("x", BType::INT));
+  auto pred = Pred::makeExprComparison(Pred::ComparisonOp::Equality,
+                                        ident("x", BType::INT),
+                                        ident("y", BType::INT));
+  auto s = Subst::makeAny(vars, std::move(pred), Subst::makeSkip());
+  auto av = s.getAllVars();
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("x")), 1u);
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("y")), 1u);
+}
+
+// ===========================================================================
+// getModifiedVars
+// ===========================================================================
+
+TEST(SubstModifiedVars, SkipEmpty) {
+  auto mv = Subst::makeSkip().getModifiedVars();
+  EXPECT_TRUE(mv.empty());
+}
+
+TEST(SubstModifiedVars, Assignment) {
+  auto s = simpleAssign("x", BType::INT, "y");
+  auto mv = s.getModifiedVars();
+  EXPECT_EQ(mv.size(), 1u);
+  EXPECT_EQ(mv.begin()->name, VarName::makeVarWithoutSuffix("x"));
+}
+
+TEST(SubstModifiedVars, AnyExcludesBound) {
+  // ANY x WHERE TRUE THEN x := 1 END
+  // x is bound by ANY, so not modified from outer perspective
+  std::vector<TypedVar> vars;
+  vars.push_back(tv("x", BType::INT));
+  auto body = simpleAssign("x", BType::INT, "x");
+  auto s = Subst::makeAny(vars, Pred::makeTrue(), std::move(body));
+  auto mv = s.getModifiedVars();
+  EXPECT_TRUE(mv.empty());
+}
+
+// ===========================================================================
+// Hashing
+// ===========================================================================
+
+TEST(SubstHash, Consistency) {
+  auto s1 = Subst::makeSkip();
+  auto s2 = Subst::makeSkip();
+  EXPECT_EQ(s1.hash_combine(0), s2.hash_combine(0));
+}
+
+TEST(SubstHash, SkipDiffersFromBlock) {
+  auto skip = Subst::makeSkip();
+  auto block = Subst::makeBlock(Subst::makeSkip());
+  EXPECT_NE(skip.hash_combine(0), block.hash_combine(0));
+}
+
+TEST(SubstHash, StdHash) {
+  std::hash<Subst> h;
+  auto s1 = Subst::makeSkip();
+  auto s2 = Subst::makeSkip();
+  EXPECT_EQ(h(s1), h(s2));
+}
+
+// ===========================================================================
+// Visitor
+// ===========================================================================
+
+class TestVisitor : public Subst::Visitor {
+ public:
+  Subst::SKind visited = Subst::SKind::Skip;
+  int count = 0;
+
+  void visitSkip() override {
+    visited = Subst::SKind::Skip;
+    count++;
+  }
+  void visitBlock(const Subst &) override {
+    visited = Subst::SKind::Block;
+    count++;
+  }
+  void visitAssert(const Pred &, const Subst &) override {
+    visited = Subst::SKind::Assert;
+    count++;
+  }
+  void visitIfThen(const Pred &, const Subst &) override {
+    visited = Subst::SKind::IfThen;
+    count++;
+  }
+  void visitIfThenElse(const Pred &, const Subst &, const Subst &) override {
+    visited = Subst::SKind::IfThenElse;
+    count++;
+  }
+  void visitSimpleAssignment(const std::vector<TypedVar> &,
+                              const std::vector<Expr> &) override {
+    visited = Subst::SKind::SimpleAssignment;
+    count++;
+  }
+  void visitSelect(
+      const std::vector<std::pair<Pred, Subst>> &) override {
+    visited = Subst::SKind::Select;
+    count++;
+  }
+  void visitSelectElse(const std::vector<std::pair<Pred, Subst>> &,
+                        const Subst &) override {
+    visited = Subst::SKind::SelectElse;
+    count++;
+  }
+  void visitCase(const Expr &,
+                  const std::vector<Subst::CaseChoice> &) override {
+    visited = Subst::SKind::Case;
+    count++;
+  }
+  void visitCaseElse(const Expr &, const std::vector<Subst::CaseChoice> &,
+                      const Subst &) override {
+    visited = Subst::SKind::CaseElse;
+    count++;
+  }
+  void visitAny(const std::vector<TypedVar> &, const Pred &,
+                 const Subst &) override {
+    visited = Subst::SKind::Any;
+    count++;
+  }
+  void visitOpCall(const std::string &, const std::vector<Expr> &,
+                    const std::vector<TypedVar> &,
+                    const std::vector<TypedVar> &,
+                    const std::vector<TypedVar> &, const Pred &,
+                    const Subst &) override {
+    visited = Subst::SKind::OperationCall;
+    count++;
+  }
+  void visitWhile(const Pred &, const Subst &, const Pred &,
+                   const Expr &) override {
+    visited = Subst::SKind::While;
+    count++;
+  }
+  void visitSequence(const std::vector<Subst> &) override {
+    visited = Subst::SKind::Sequence;
+    count++;
+  }
+  void visitParallel(const std::vector<Subst> &) override {
+    visited = Subst::SKind::Parallel;
+    count++;
+  }
+  void visitChoice(const std::vector<Subst> &) override {
+    visited = Subst::SKind::Choice;
+    count++;
+  }
+  void visitWitness(const std::map<std::string, Expr> &,
+                     const Subst &) override {
+    visited = Subst::SKind::Witness;
+    count++;
+  }
+};
+
+static void checkVisitor(Subst &s, Subst::SKind expected) {
+  TestVisitor v;
+  s.accept(v);
+  EXPECT_EQ(v.visited, expected);
+  EXPECT_EQ(v.count, 1);
+}
+
+TEST(SubstVisitor, AllKinds) {
+  auto skip = Subst::makeSkip();
+  checkVisitor(skip, Subst::SKind::Skip);
+
+  auto block = Subst::makeBlock(Subst::makeSkip());
+  checkVisitor(block, Subst::SKind::Block);
+
+  auto assert_ = Subst::makeAssert(Pred::makeTrue(), Subst::makeSkip());
+  checkVisitor(assert_, Subst::SKind::Assert);
+
+  auto ifThen = Subst::makeIfThen(Pred::makeTrue(), Subst::makeSkip());
+  checkVisitor(ifThen, Subst::SKind::IfThen);
+
+  auto ifThenElse = Subst::makeIfThenElse(Pred::makeTrue(), Subst::makeSkip(),
+                                            Subst::makeSkip());
+  checkVisitor(ifThenElse, Subst::SKind::IfThenElse);
+
+  auto assign = simpleAssign("x", BType::INT, "y");
+  checkVisitor(assign, Subst::SKind::SimpleAssignment);
+
+  {
+    std::vector<std::pair<Pred, Subst>> clauses;
+    clauses.push_back({Pred::makeTrue(), Subst::makeSkip()});
+    auto sel = Subst::makeSelect(std::move(clauses));
+    checkVisitor(sel, Subst::SKind::Select);
+  }
+  {
+    std::vector<std::pair<Pred, Subst>> clauses;
+    clauses.push_back({Pred::makeTrue(), Subst::makeSkip()});
+    auto selE = Subst::makeSelectElse(std::move(clauses), Subst::makeSkip());
+    checkVisitor(selE, Subst::SKind::SelectElse);
+  }
+  {
+    std::vector<Subst::CaseChoice> cases;
+    Subst::CaseChoice ch;
+    ch.values.push_back(Expr::makeInteger("1"));
+    ch.body = Subst::makeSkip();
+    cases.push_back(std::move(ch));
+    auto cas = Subst::makeCase(ident("x", BType::INT), std::move(cases));
+    checkVisitor(cas, Subst::SKind::Case);
+  }
+  {
+    std::vector<Subst::CaseChoice> cases;
+    Subst::CaseChoice ch;
+    ch.values.push_back(Expr::makeInteger("1"));
+    ch.body = Subst::makeSkip();
+    cases.push_back(std::move(ch));
+    auto casE = Subst::makeCaseElse(ident("x", BType::INT),
+                                     std::move(cases), Subst::makeSkip());
+    checkVisitor(casE, Subst::SKind::CaseElse);
+  }
+  {
+    std::vector<TypedVar> vars;
+    vars.push_back(tv("x", BType::INT));
+    auto any = Subst::makeAny(vars, Pred::makeTrue(), Subst::makeSkip());
+    checkVisitor(any, Subst::SKind::Any);
+  }
+  {
+    std::vector<Expr> input;
+    input.push_back(Expr::makeInteger("1"));
+    std::vector<TypedVar> output, op_in, op_out;
+    output.push_back(tv("r", BType::INT));
+    op_in.push_back(tv("p", BType::INT));
+    op_out.push_back(tv("q", BType::INT));
+    auto op = Subst::makeOpCall("op", std::move(input), output, op_in, op_out,
+                                 Pred::makeTrue(), Subst::makeSkip());
+    checkVisitor(op, Subst::SKind::OperationCall);
+  }
+  {
+    auto wh = Subst::makeWhile(Pred::makeTrue(), Subst::makeSkip(),
+                                Pred::makeTrue(), Expr::makeInteger("0"));
+    checkVisitor(wh, Subst::SKind::While);
+  }
+  {
+    std::vector<Subst> vec;
+    vec.push_back(Subst::makeSkip());
+    auto seq = Subst::makeSequence(std::move(vec));
+    checkVisitor(seq, Subst::SKind::Sequence);
+  }
+  {
+    std::vector<Subst> vec;
+    vec.push_back(Subst::makeSkip());
+    auto par = Subst::makeParallel(std::move(vec));
+    checkVisitor(par, Subst::SKind::Parallel);
+  }
+  {
+    std::vector<Subst> vec;
+    vec.push_back(Subst::makeSkip());
+    auto cho = Subst::makeChoice(std::move(vec));
+    checkVisitor(cho, Subst::SKind::Choice);
+  }
+  {
+    std::map<std::string, Expr> witnesses;
+    witnesses.emplace("w", Expr::makeInteger("1"));
+    auto wit = Subst::makeWitness(std::move(witnesses), Subst::makeSkip());
+    checkVisitor(wit, Subst::SKind::Witness);
+  }
+}
+
+// ===========================================================================
+// Alpha renaming
+// ===========================================================================
+
+TEST(SubstAlpha, AssignmentRenames) {
+  // x := y, rename x->a, y->b
+  auto s = simpleAssign("x", BType::INT, "y");
+  std::map<VarName, VarName> map;
+  map.emplace(VarName::makeVarWithoutSuffix("x"), VarName::makeVarWithoutSuffix("a"));
+  map.emplace(VarName::makeVarWithoutSuffix("y"), VarName::makeVarWithoutSuffix("b"));
+  s.alpha(map);
+  auto &sa = s.toSimpleAssignment();
+  EXPECT_EQ(sa.vars[0].name, VarName::makeVarWithoutSuffix("a"));
+  // RHS expr should also be renamed
+  auto fv = s.getAllVars();
+  EXPECT_EQ(fv.count(VarName::makeVarWithoutSuffix("b")), 1u);
+}
+
+TEST(SubstAlpha, AnyShadowsBoundVars) {
+  // ANY x WHERE x=y THEN skip END, rename x->a
+  // Since x is bound by ANY, the rename should NOT apply to x
+  std::vector<TypedVar> vars;
+  vars.push_back(tv("x", BType::INT));
+  auto pred = Pred::makeExprComparison(Pred::ComparisonOp::Equality,
+                                        ident("x", BType::INT),
+                                        ident("y", BType::INT));
+  auto s = Subst::makeAny(vars, std::move(pred), Subst::makeSkip());
+  std::map<VarName, VarName> map;
+  map.emplace(VarName::makeVarWithoutSuffix("x"), VarName::makeVarWithoutSuffix("a"));
+  map.emplace(VarName::makeVarWithoutSuffix("y"), VarName::makeVarWithoutSuffix("b"));
+  s.alpha(map);
+  // x should remain x (shadowed), y should become b
+  auto av = s.getAllVars();
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("x")), 1u);
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("b")), 1u);
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("a")), 0u);
+}
+
+TEST(SubstAlpha, NestedPropagates) {
+  // IF TRUE THEN x := y END, rename y->z
+  auto body = simpleAssign("x", BType::INT, "y");
+  auto s = Subst::makeIfThen(Pred::makeTrue(), std::move(body));
+  std::map<VarName, VarName> map;
+  map.emplace(VarName::makeVarWithoutSuffix("y"), VarName::makeVarWithoutSuffix("z"));
+  s.alpha(map);
+  auto av = s.getAllVars();
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("z")), 1u);
+  EXPECT_EQ(av.count(VarName::makeVarWithoutSuffix("y")), 0u);
+}
+
+// ===========================================================================
+// substFreshId
+// ===========================================================================
+
+TEST(SubstSubstFreshId, AssignmentFreshId) {
+  // Assignment with FreshId variable
+  std::vector<TypedVar> vars;
+  vars.push_back(TypedVar{VarName::makeFreshId("tmp"), BType::INT});
+  std::vector<Expr> exprs;
+  exprs.push_back(Expr::makeInteger("1"));
+  auto s = Subst::makeSimpleAssignment(vars, std::move(exprs));
+  s.substFreshId("tmp", VarName::makeVarWithoutSuffix("real_var"));
+  EXPECT_EQ(s.toSimpleAssignment().vars[0].name,
+            VarName::makeVarWithoutSuffix("real_var"));
+}
+
+TEST(SubstSubstFreshId, AnyFreshIdInBoundVars) {
+  std::vector<TypedVar> vars;
+  vars.push_back(TypedVar{VarName::makeFreshId("tmp"), BType::INT});
+  auto s = Subst::makeAny(vars, Pred::makeTrue(), Subst::makeSkip());
+  s.substFreshId("tmp", VarName::makeVarWithoutSuffix("real_var"));
+  EXPECT_EQ(s.toAny().vars[0].name, VarName::makeVarWithoutSuffix("real_var"));
+}
+
+// ===========================================================================
+// getInnerFreeVars
+// ===========================================================================
+
+TEST(SubstInnerFreeVars, SkipEmpty) {
+  std::set<VarName> accu;
+  Subst::makeSkip().getInnerFreeVars(accu);
+  EXPECT_TRUE(accu.empty());
+}
+
+TEST(SubstInnerFreeVars, AssignmentEmpty) {
+  auto s = simpleAssign("x", BType::INT, "y");
+  std::set<VarName> accu;
+  s.getInnerFreeVars(accu);
+  EXPECT_TRUE(accu.empty());
+}
+
+TEST(SubstInnerFreeVars, OpCallExposesInnerFreeVars) {
+  // OpCall with op_body referencing a free var "z" (not in op_input/op_output)
+  std::vector<Expr> input;
+  input.push_back(Expr::makeInteger("1"));
+  std::vector<TypedVar> output;
+  output.push_back(tv("r", BType::INT));
+  std::vector<TypedVar> op_input;
+  op_input.push_back(tv("p", BType::INT));
+  std::vector<TypedVar> op_output;
+  op_output.push_back(tv("q", BType::INT));
+  // op_body: q := z  (z is free in op body, not bound by op_input/op_output)
+  auto op_body = simpleAssign("q", BType::INT, "z");
+  auto s = Subst::makeOpCall("myOp", std::move(input), output, op_input,
+                              op_output, Pred::makeTrue(), std::move(op_body));
+  std::set<VarName> accu;
+  s.getInnerFreeVars(accu);
+  EXPECT_EQ(accu.count(VarName::makeVarWithoutSuffix("z")), 1u);
+  // q appears because SimpleAssignment::getFreeVars adds LHS vars that ARE
+  // in boundVars (referencing a bound op_output variable)
+  EXPECT_EQ(accu.count(VarName::makeVarWithoutSuffix("q")), 1u);
+  // p is not referenced in op_body
+  EXPECT_EQ(accu.count(VarName::makeVarWithoutSuffix("p")), 0u);
+}
diff --git a/tests/test_vars.cpp b/tests/test_vars.cpp
new file mode 100644
index 0000000..5c8af22
--- /dev/null
+++ b/tests/test_vars.cpp
@@ -0,0 +1,326 @@
+#include "vars.h"
+
+#include <gtest/gtest.h>
+
+// --- VarName construction & kinds ---
+
+TEST(VarName, NoSuffix) {
+  auto v = VarName::makeVarWithoutSuffix("x");
+  EXPECT_EQ(v.kind(), VarName::Kind::NoSuffix);
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_EQ(v.suffix(), -1);
+}
+
+TEST(VarName, WithSuffix) {
+  auto v = VarName::makeVar("x", 3);
+  EXPECT_EQ(v.kind(), VarName::Kind::WithSuffix);
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_EQ(v.suffix(), 3);
+}
+
+TEST(VarName, FreshId) {
+  auto v = VarName::makeFreshId("x");
+  EXPECT_EQ(v.kind(), VarName::Kind::FreshId);
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_EQ(v.suffix(), -2);
+}
+
+TEST(VarName, Tmp) {
+  auto v = VarName::makeTmp("x");
+  EXPECT_EQ(v.kind(), VarName::Kind::Tmp);
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_LT(v.suffix(), -2);
+}
+
+TEST(VarName, TmpUnique) {
+  auto v1 = VarName::makeTmp("x");
+  auto v2 = VarName::makeTmp("x");
+  EXPECT_NE(v1, v2);
+}
+
+// --- VarName::show ---
+
+TEST(VarName, ShowNoSuffix) {
+  auto v = VarName::makeVarWithoutSuffix("toto");
+  EXPECT_EQ(v.show(), "toto");
+}
+
+TEST(VarName, ShowWithSuffix) {
+  auto v = VarName::makeVar("toto", 1);
+  EXPECT_EQ(v.show(), "toto$1");
+}
+
+TEST(VarName, ShowFreshId) {
+  auto v = VarName::makeFreshId("toto");
+  EXPECT_EQ(v.show(), "_freshId_toto");
+}
+
+TEST(VarName, ShowTmp) {
+  auto v = VarName::makeTmp("toto");
+  auto s = v.show();
+  EXPECT_TRUE(s.find("_tmpId_toto$") == 0);
+}
+
+// --- VarName comparison ---
+
+TEST(VarName, EqualSame) {
+  auto v1 = VarName::makeVarWithoutSuffix("x");
+  auto v2 = VarName::makeVarWithoutSuffix("x");
+  EXPECT_EQ(v1, v2);
+}
+
+TEST(VarName, NotEqualDifferentPrefix) {
+  auto v1 = VarName::makeVarWithoutSuffix("x");
+  auto v2 = VarName::makeVarWithoutSuffix("y");
+  EXPECT_NE(v1, v2);
+}
+
+TEST(VarName, NotEqualDifferentSuffix) {
+  auto v1 = VarName::makeVarWithoutSuffix("x");
+  auto v2 = VarName::makeVar("x", 1);
+  EXPECT_NE(v1, v2);
+}
+
+TEST(VarName, CompareConsistent) {
+  auto v1 = VarName::makeVarWithoutSuffix("x");
+  auto v2 = VarName::makeVar("x", 1);
+  int c1 = VarName::compare(v1, v2);
+  int c2 = VarName::compare(v2, v1);
+  EXPECT_NE(c1, 0);
+  // opposite signs
+  EXPECT_TRUE((c1 < 0 && c2 > 0) || (c1 > 0 && c2 < 0));
+}
+
+TEST(VarName, OrderingOperators) {
+  auto v1 = VarName::makeVarWithoutSuffix("a");
+  auto v2 = VarName::makeVarWithoutSuffix("a");
+  EXPECT_TRUE(v1 <= v2);
+  EXPECT_TRUE(v1 >= v2);
+  EXPECT_FALSE(v1 < v2);
+  EXPECT_FALSE(v1 > v2);
+}
+
+// --- VarName vec_compare ---
+
+TEST(VarName, VecCompareEqual) {
+  std::vector<VarName> v1 = {VarName::makeVarWithoutSuffix("x"),
+                             VarName::makeVarWithoutSuffix("y")};
+  std::vector<VarName> v2 = {VarName::makeVarWithoutSuffix("x"),
+                             VarName::makeVarWithoutSuffix("y")};
+  EXPECT_EQ(VarName::vec_compare(v1, v2), 0);
+}
+
+TEST(VarName, VecCompareDifferentSize) {
+  std::vector<VarName> v1 = {VarName::makeVarWithoutSuffix("x")};
+  std::vector<VarName> v2 = {VarName::makeVarWithoutSuffix("x"),
+                             VarName::makeVarWithoutSuffix("y")};
+  EXPECT_LT(VarName::vec_compare(v1, v2), 0);
+}
+
+TEST(VarName, VecCompareEmpty) {
+  std::vector<VarName> v1, v2;
+  EXPECT_EQ(VarName::vec_compare(v1, v2), 0);
+}
+
+// --- VarName hashing ---
+
+TEST(VarName, HashConsistency) {
+  auto v1 = VarName::makeVarWithoutSuffix("x");
+  auto v2 = VarName::makeVarWithoutSuffix("x");
+  EXPECT_EQ(v1.hash_combine(0), v2.hash_combine(0));
+}
+
+TEST(VarName, HashDifferent) {
+  auto v1 = VarName::makeVarWithoutSuffix("x");
+  auto v2 = VarName::makeVarWithoutSuffix("y");
+  EXPECT_NE(v1.hash_combine(0), v2.hash_combine(0));
+}
+
+// --- VarName::getFreshVar ---
+
+TEST(VarName, GetFreshVarNotInSet) {
+  std::set<VarName> s;
+  auto v = VarName::getFreshVar("x", s);
+  EXPECT_EQ(v, VarName::makeVarWithoutSuffix("x"));
+}
+
+TEST(VarName, GetFreshVarConflict) {
+  std::set<VarName> s;
+  s.insert(VarName::makeVarWithoutSuffix("x"));
+  auto v = VarName::getFreshVar("x", s);
+  EXPECT_NE(v, VarName::makeVarWithoutSuffix("x"));
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_EQ(s.find(v), s.end());
+}
+
+TEST(VarName, GetFreshVarMultipleConflicts) {
+  std::set<VarName> s;
+  s.insert(VarName::makeVarWithoutSuffix("x"));
+  s.insert(VarName::makeVar("x", 1));
+  s.insert(VarName::makeVar("x", 2));
+  auto v = VarName::getFreshVar("x", s);
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_EQ(v.suffix(), 3);
+}
+
+TEST(VarName, GetFreshVarFromVarName) {
+  std::set<VarName> s;
+  auto orig = VarName::makeVarWithoutSuffix("x");
+  auto v = VarName::getFreshVar(orig, s);
+  EXPECT_EQ(v, orig);
+}
+
+TEST(VarName, GetFreshVarFromVarNameConflict) {
+  std::set<VarName> s;
+  s.insert(VarName::makeVarWithoutSuffix("x"));
+  auto orig = VarName::makeVarWithoutSuffix("x");
+  auto v = VarName::getFreshVar(orig, s);
+  EXPECT_NE(v, orig);
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_EQ(s.find(v), s.end());
+}
+
+TEST(VarName, GetFreshVarFromSuffixed) {
+  std::set<VarName> s;
+  s.insert(VarName::makeVar("x", 1));
+  auto orig = VarName::makeVar("x", 1);
+  auto v = VarName::getFreshVar(orig, s);
+  EXPECT_NE(v, orig);
+  EXPECT_EQ(v.prefix(), "x");
+  EXPECT_GT(v.suffix(), 1);
+}
+
+TEST(VarName, GetFreshVarFromTmp) {
+  std::set<VarName> s;
+  auto orig = VarName::makeTmp("x");
+  s.insert(orig);
+  auto v = VarName::getFreshVar(orig, s);
+  EXPECT_NE(v, orig);
+  EXPECT_EQ(v.kind(), VarName::Kind::Tmp);
+}
+
+// --- TypedVar ---
+
+TEST(TypedVar, Construction) {
+  auto name = VarName::makeVarWithoutSuffix("x");
+  TypedVar tv(name, BType::INT);
+  EXPECT_EQ(tv.name, name);
+  EXPECT_EQ(tv.type, BType::INT);
+}
+
+TEST(TypedVar, EqualSame) {
+  TypedVar tv1(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  TypedVar tv2(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  EXPECT_EQ(tv1, tv2);
+}
+
+TEST(TypedVar, NotEqualDifferentName) {
+  TypedVar tv1(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  TypedVar tv2(VarName::makeVarWithoutSuffix("y"), BType::INT);
+  EXPECT_NE(tv1, tv2);
+}
+
+TEST(TypedVar, NotEqualDifferentType) {
+  TypedVar tv1(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  TypedVar tv2(VarName::makeVarWithoutSuffix("x"), BType::BOOL);
+  EXPECT_NE(tv1, tv2);
+}
+
+TEST(TypedVar, VecCompare) {
+  std::vector<TypedVar> v1 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  std::vector<TypedVar> v2 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  EXPECT_EQ(TypedVar::vec_compare(v1, v2), 0);
+}
+
+TEST(TypedVar, VecCompareDifferentSize) {
+  std::vector<TypedVar> v1;
+  std::vector<TypedVar> v2 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  EXPECT_LT(TypedVar::vec_compare(v1, v2), 0);
+}
+
+TEST(TypedVar, HashConsistency) {
+  TypedVar tv1(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  TypedVar tv2(VarName::makeVarWithoutSuffix("x"), BType::INT);
+  EXPECT_EQ(tv1.hash_combine(0), tv2.hash_combine(0));
+}
+
+// --- Context ---
+
+TEST(Context, PushMatchingVars) {
+  Context ctx;
+  std::vector<TypedVar> v1 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  std::vector<TypedVar> v2 = {
+      TypedVar(VarName::makeVar("x", 1), BType::INT)};
+  EXPECT_TRUE(ctx.push(v1, v2));
+}
+
+TEST(Context, PushDifferentSizes) {
+  Context ctx;
+  std::vector<TypedVar> v1 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  std::vector<TypedVar> v2;
+  EXPECT_FALSE(ctx.push(v1, v2));
+}
+
+TEST(Context, PushDifferentPrefixes) {
+  Context ctx;
+  std::vector<TypedVar> v1 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  std::vector<TypedVar> v2 = {
+      TypedVar(VarName::makeVarWithoutSuffix("y"), BType::INT)};
+  EXPECT_FALSE(ctx.push(v1, v2));
+}
+
+TEST(Context, PushDifferentTypes) {
+  Context ctx;
+  std::vector<TypedVar> v1 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::INT)};
+  std::vector<TypedVar> v2 = {
+      TypedVar(VarName::makeVarWithoutSuffix("x"), BType::BOOL)};
+  EXPECT_FALSE(ctx.push(v1, v2));
+}
+
+TEST(Context, EqualsBoundVars) {
+  Context ctx;
+  auto x1 = VarName::makeVarWithoutSuffix("x");
+  auto x2 = VarName::makeVar("x", 1);
+  std::vector<TypedVar> v1 = {TypedVar(x1, BType::INT)};
+  std::vector<TypedVar> v2 = {TypedVar(x2, BType::INT)};
+  ctx.push(v1, v2);
+  EXPECT_TRUE(ctx.equals(x1, x2));
+}
+
+TEST(Context, EqualsFreeVars) {
+  Context ctx;
+  auto y1 = VarName::makeVarWithoutSuffix("y");
+  auto y2 = VarName::makeVarWithoutSuffix("y");
+  EXPECT_TRUE(ctx.equals(y1, y2));
+}
+
+TEST(Context, NotEqualsMixed) {
+  Context ctx;
+  auto x1 = VarName::makeVarWithoutSuffix("x");
+  auto x2 = VarName::makeVar("x", 1);
+  auto y = VarName::makeVarWithoutSuffix("y");
+  std::vector<TypedVar> v1 = {TypedVar(x1, BType::INT)};
+  std::vector<TypedVar> v2 = {TypedVar(x2, BType::INT)};
+  ctx.push(v1, v2);
+  // x1 is bound, y is free - should not be equal
+  EXPECT_FALSE(ctx.equals(x1, y));
+}
+
+TEST(Context, PopRestores) {
+  Context ctx;
+  auto x1 = VarName::makeVarWithoutSuffix("x");
+  auto x2 = VarName::makeVar("x", 1);
+  std::vector<TypedVar> v1 = {TypedVar(x1, BType::INT)};
+  std::vector<TypedVar> v2 = {TypedVar(x2, BType::INT)};
+  ctx.push(v1, v2);
+  ctx.pop();
+  // After pop, x1 and x2 are treated as free vars again
+  EXPECT_FALSE(ctx.equals(x1, x2));
+}