diff --git a/CLAUDE.md b/CLAUDE.md
new file mode 100644
index 000000000..61898f246
--- /dev/null
+++ b/CLAUDE.md
@@ -0,0 +1,82 @@
+# CLAUDE.md
+
+This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
+
+## Overview
+
+Pumpkin is a constraint programming (CP) solver written in pure Rust, based on the lazy clause generation paradigm. It supports proof logging via DRAT (SAT) and DRCP (CP) certificates.
+
+## Build & Development Commands
+
+```bash
+# Build
+cargo build
+cargo build --release
+
+# Test (standard CI command)
+cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations
+
+# Run a single test
+cargo test --release --features pumpkin-solver/check-propagations <test_name>
+
+# Format (requires nightly)
+cargo +nightly fmt
+cargo +nightly fmt --check  # check only
+
+# Lint (requires nightly)
+cargo +nightly clippy --all-targets -- -Dwarnings
+
+# Docs
+cargo doc --no-deps
+
+# License check
+cargo deny check
+
+# WASM tests (for pumpkin-crates/core)
+wasm-pack test --release --node
+
+# Python tests
+cd pumpkin-solver-py && pytest
+```
+
+Scripts in `scripts/` (`fmt.sh`, `clippy.sh`, `documentation.sh`, `deny.sh`) mirror the CI commands and are also run by the pre-commit hook (`.githooks/pre-commit`).
+
+## Workspace Architecture
+
+The project is a Cargo workspace (edition 2024, resolver 2). Crates are grouped by role:
+
+### Core Engine (`pumpkin-crates/`)
+- **`core`** — The main solver engine. Contains the CDCL loop, propagation engine, nogood learning, branching heuristics, and proof logging infrastructure. This is the heart of the solver.
+- **`checking`** — Shared types used by both `core` and `pumpkin-checker` (avoids circular deps).
+- **`propagators`** — Implementations of CP propagators (arithmetic, cumulative, disjunctive, element, etc.).
+- **`conflict-resolvers`** — Pluggable conflict analysis strategies for nogood derivation.
+- **`constraints`** — High-level constraint API built on top of `core`.
+
+### Interfaces
+- **`pumpkin-solver`** — CLI binary. Accepts CNF, WCNF (MaxSAT), and FlatZinc input formats.
+- **`pumpkin-solver-py`** — Python bindings via PyO3.
+
+### Proof Infrastructure
+- **`drcp-format`** — Reading/writing the DRCP proof certificate format.
+- **`pumpkin-checker`** — Standalone proof verification tool.
+- **`pumpkin-proof-processor`** — Proof transformation/preprocessing utility.
+- **`drcp-debugger`** — Debugging tool for DRCP proofs.
+
+### Parsing & Utilities
+- **`fzn-rs`** / **`fzn-rs-derive`** — FlatZinc parser and derive macros.
+- **`pumpkin-macros`** — Procedural macros used across the workspace.
+- **`minizinc/`** — MiniZinc integration (solver plugin).
+
+## Key Design Concepts
+
+- **Lazy Clause Generation (LCG)**: The solver operates on a hybrid SAT/CP model. CP propagators generate explanations (clauses/nogoods) on demand during conflict analysis.
+- **Proof Logging**: Every inference can be certified. The `core` crate threads proof-logging through propagators via a `Proof` type. The `check-propagations` feature enables runtime validation of propagator explanations during tests.
+- **Propagator Interface**: Custom propagators implement the `Propagator` trait in `pumpkin-crates/core`. They must provide both `propagate` and `explain` methods for proof soundness.
+- **Feature Flags**: `pumpkin-solver/check-propagations` enables expensive correctness assertions — always enable this when running tests.
+
+## Code Style
+
+- **Rust edition 2024**, stable toolchain (see `rust-toolchain.toml`), but formatting/linting requires nightly.
+- Line length: 120 chars for comments (`rustfmt.toml`).
+- Imports: grouped (std / external / crate), single-line style enforced.
+- Workspace-level lints are configured in the root `Cargo.toml` — check there before suppressing warnings locally.
diff --git a/pumpkin-crates/propagators/src/lib.rs b/pumpkin-crates/propagators/src/lib.rs
index b78a60169..6210ef73b 100644
--- a/pumpkin-crates/propagators/src/lib.rs
+++ b/pumpkin-crates/propagators/src/lib.rs
@@ -4,3 +4,29 @@
 //! [`pumpkin_core::propagation`].
 mod propagators;
 pub use propagators::*;
+#[cfg(test)]
+use pumpkin_core::state::State;
+#[cfg(test)]
+use pumpkin_core::variables::DomainId;
+
+/// Utilities that simplify test code using the [`State`].
+#[cfg(test)]
+pub(crate) trait StateExt {
+    /// Assert that the bounds of the given `domain_id` match the provided `lower_bound` and
+    /// `upper_bound`.
+    fn assert_bounds(&self, domain_id: DomainId, lower_bound: i32, upper_bound: i32);
+}
+
+#[cfg(test)]
+impl StateExt for State {
+    fn assert_bounds(&self, domain_id: DomainId, lower_bound: i32, upper_bound: i32) {
+        let actual_lb = self.lower_bound(domain_id);
+        let actual_ub = self.upper_bound(domain_id);
+
+        assert_eq!(
+            (lower_bound, upper_bound),
+            (actual_lb, actual_ub),
+            "The expected bounds [{lower_bound}..{upper_bound}] did not match the actual bounds [{actual_lb}..{actual_ub}]"
+        );
+    }
+}
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs
index 95b6e334a..753384dc1 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs
@@ -205,124 +205,118 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
+    use pumpkin_core::state::State;
 
     use super::*;
+    use crate::StateExt;
 
     #[test]
     fn absolute_bounds_are_propagated_at_initialise() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let signed = solver.new_variable(-3, 4);
-        let absolute = solver.new_variable(-2, 10);
-        let constraint_tag = solver.new_constraint_tag();
+        let signed = state.new_interval_variable(-3, 4, None);
+        let absolute = state.new_interval_variable(-2, 10, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(AbsoluteValueArgs {
-                signed,
-                absolute,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(AbsoluteValueArgs {
+            signed,
+            absolute,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(absolute, 0, 4);
+        state.assert_bounds(absolute, 0, 4);
     }
 
     #[test]
     fn signed_bounds_are_propagated_at_initialise() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let signed = solver.new_variable(-5, 5);
-        let absolute = solver.new_variable(0, 3);
-        let constraint_tag = solver.new_constraint_tag();
+        let signed = state.new_interval_variable(-5, 5, None);
+        let absolute = state.new_interval_variable(0, 3, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(AbsoluteValueArgs {
-                signed,
-                absolute,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(AbsoluteValueArgs {
+            signed,
+            absolute,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(signed, -3, 3);
+        state.assert_bounds(signed, -3, 3);
     }
 
     #[test]
     fn absolute_lower_bound_can_be_strictly_positive() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let signed = solver.new_variable(3, 6);
-        let absolute = solver.new_variable(0, 10);
-        let constraint_tag = solver.new_constraint_tag();
+        let signed = state.new_interval_variable(3, 6, None);
+        let absolute = state.new_interval_variable(0, 10, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(AbsoluteValueArgs {
-                signed,
-                absolute,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(AbsoluteValueArgs {
+            signed,
+            absolute,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(absolute, 3, 6);
+        state.assert_bounds(absolute, 3, 6);
     }
 
     #[test]
     fn strictly_negative_signed_value_can_propagate_lower_bound_on_absolute() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let signed = solver.new_variable(-5, -3);
-        let absolute = solver.new_variable(1, 5);
-        let constraint_tag = solver.new_constraint_tag();
+        let signed = state.new_interval_variable(-5, -3, None);
+        let absolute = state.new_interval_variable(1, 5, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(AbsoluteValueArgs {
-                signed,
-                absolute,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(AbsoluteValueArgs {
+            signed,
+            absolute,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(absolute, 3, 5);
+        state.assert_bounds(absolute, 3, 5);
     }
 
     #[test]
     fn lower_bound_on_absolute_can_propagate_negative_upper_bound_on_signed() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let signed = solver.new_variable(-5, 0);
-        let absolute = solver.new_variable(1, 5);
-        let constraint_tag = solver.new_constraint_tag();
+        let signed = state.new_interval_variable(-5, 0, None);
+        let absolute = state.new_interval_variable(1, 5, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(AbsoluteValueArgs {
-                signed,
-                absolute,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(AbsoluteValueArgs {
+            signed,
+            absolute,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(signed, -5, -1);
+        state.assert_bounds(signed, -5, -1);
     }
 
     #[test]
     fn lower_bound_on_absolute_can_propagate_positive_lower_bound_on_signed() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let signed = solver.new_variable(1, 5);
-        let absolute = solver.new_variable(3, 5);
-        let constraint_tag = solver.new_constraint_tag();
+        let signed = state.new_interval_variable(1, 5, None);
+        let absolute = state.new_interval_variable(3, 5, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(AbsoluteValueArgs {
-                signed,
-                absolute,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(AbsoluteValueArgs {
+            signed,
+            absolute,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(signed, 3, 5);
+        state.assert_bounds(signed, 3, 5);
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs
index 7241fd3ae..40f429ab8 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs
@@ -439,59 +439,60 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
-    use pumpkin_core::propagation::EnqueueDecision;
+    use pumpkin_core::state::State;
 
+    use crate::StateExt;
     use crate::propagators::arithmetic::BinaryEqualsPropagatorArgs;
 
     #[test]
     fn test_propagation_of_bounds() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(0, 5);
-        let b = solver.new_variable(3, 7);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let a = state.new_interval_variable(0, 5, None);
+        let b = state.new_interval_variable(3, 7, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let result = solver.new_propagator(BinaryEqualsPropagatorArgs {
+        let _ = state.add_propagator(BinaryEqualsPropagatorArgs {
             a,
             b,
             constraint_tag,
         });
+        state.propagate_to_fixed_point().expect("no conflict");
 
-        assert!(result.is_ok());
-
-        solver.assert_bounds(a, 3, 5);
-        solver.assert_bounds(b, 3, 5);
+        state.assert_bounds(a, 3, 5);
+        state.assert_bounds(b, 3, 5);
     }
 
     #[test]
     fn test_propagation_of_holes() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_sparse_variable(vec![2, 4, 6, 9]);
-        let b = solver.new_sparse_variable(vec![3, 4, 7, 9]);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let a = state.new_sparse_variable(vec![2, 4, 6, 9], None);
+        let b = state.new_sparse_variable(vec![3, 4, 7, 9], None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let result = solver.new_propagator(BinaryEqualsPropagatorArgs {
+        let _ = state.add_propagator(BinaryEqualsPropagatorArgs {
             a,
             b,
             constraint_tag,
         });
+        state.propagate_to_fixed_point().expect("no conflict");
 
-        assert!(result.is_ok());
-
-        solver.assert_bounds(a, 4, 9);
-        solver.assert_bounds(b, 4, 9);
+        state.assert_bounds(a, 4, 9);
+        state.assert_bounds(b, 4, 9);
 
         for i in 5..=8 {
-            assert!(!solver.contains(a, i));
-            assert!(!solver.contains(b, i));
+            assert!(!state.contains(a, i));
+            assert!(!state.contains(b, i));
         }
     }
 
+    #[allow(deprecated, reason = "Uses TestSolver for EnqueueDecision assertions")]
     #[test]
     fn test_propagation_of_holes_incremental() {
+        use pumpkin_core::TestSolver;
+        use pumpkin_core::propagation::EnqueueDecision;
+
         let mut solver = TestSolver::default();
         let a = solver.new_variable(2, 9);
         let b = solver.new_variable(3, 9);
@@ -527,17 +528,18 @@ mod tests {
 
     #[test]
     fn test_conflict() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(0, 5);
-        let b = solver.new_variable(6, 9);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let a = state.new_interval_variable(0, 5, None);
+        let b = state.new_interval_variable(6, 9, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(BinaryEqualsPropagatorArgs {
-                a,
-                b,
-                constraint_tag,
-            })
-            .expect_err("Expected result to be err");
+        let _ = state.add_propagator(BinaryEqualsPropagatorArgs {
+            a,
+            b,
+            constraint_tag,
+        });
+        let _ = state
+            .propagate_to_fixed_point()
+            .expect_err("expected conflict");
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs
index efe6d8768..f000a7eeb 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs
@@ -206,50 +206,55 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
-    use pumpkin_core::propagation::EnqueueDecision;
+    use pumpkin_core::state::State;
 
+    use crate::StateExt;
     use crate::propagators::arithmetic::BinaryNotEqualsPropagatorArgs;
 
     #[test]
     fn detects_conflict() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(0, 0);
-        let b = solver.new_variable(0, 0);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let a = state.new_interval_variable(0, 0, None);
+        let b = state.new_interval_variable(0, 0, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(BinaryNotEqualsPropagatorArgs {
-                a,
-                b,
-                constraint_tag,
-            })
+        let _ = state.add_propagator(BinaryNotEqualsPropagatorArgs {
+            a,
+            b,
+            constraint_tag,
+        });
+        let _ = state
+            .propagate_to_fixed_point()
             .expect_err("Expected conflict to be detected");
     }
 
     #[test]
     fn propagate_when_one_is_fixed() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(0, 0);
-        let b = solver.new_variable(0, 1);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let a = state.new_interval_variable(0, 0, None);
+        let b = state.new_interval_variable(0, 1, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(BinaryNotEqualsPropagatorArgs {
-                a,
-                b,
-                constraint_tag,
-            })
+        let _ = state.add_propagator(BinaryNotEqualsPropagatorArgs {
+            a,
+            b,
+            constraint_tag,
+        });
+        state
+            .propagate_to_fixed_point()
             .expect("Expected no conflict to be detected");
 
-        solver.assert_bounds(b, 1, 1);
+        state.assert_bounds(b, 1, 1);
     }
 
+    #[allow(deprecated, reason = "Uses TestSolver for EnqueueDecision assertions")]
     #[test]
     fn incremental_propagation() {
+        use pumpkin_core::TestSolver;
+        use pumpkin_core::propagation::EnqueueDecision;
+
         let mut solver = TestSolver::default();
         let a = solver.new_variable(0, 0);
         let b = solver.new_variable(0, 10);
@@ -277,20 +282,21 @@ mod tests {
 
     #[test]
     fn non_overlapping_is_ok() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(0, 5);
-        let b = solver.new_variable(6, 10);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let a = state.new_interval_variable(0, 5, None);
+        let b = state.new_interval_variable(6, 10, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(BinaryNotEqualsPropagatorArgs {
-                a,
-                b,
-                constraint_tag,
-            })
+        let _ = state.add_propagator(BinaryNotEqualsPropagatorArgs {
+            a,
+            b,
+            constraint_tag,
+        });
+        state
+            .propagate_to_fixed_point()
             .expect("Expected no conflict to be detected");
 
-        solver.assert_bounds(a, 0, 5);
-        solver.assert_bounds(b, 6, 10);
+        state.assert_bounds(a, 0, 5);
+        state.assert_bounds(b, 6, 10);
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs
index 526f1511c..e0ba0e6a6 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs
@@ -457,28 +457,27 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
+    use pumpkin_core::state::State;
 
     use super::*;
 
     #[test]
     fn detects_conflicts() {
-        let mut solver = TestSolver::default();
-        let numerator = solver.new_variable(1, 1);
-        let denominator = solver.new_variable(2, 2);
-        let rhs = solver.new_variable(2, 2);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let numerator = state.new_interval_variable(1, 1, None);
+        let denominator = state.new_interval_variable(2, 2, None);
+        let rhs = state.new_interval_variable(2, 2, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let propagator = solver.new_propagator(DivisionArgs {
+        let _ = state.add_propagator(DivisionArgs {
             numerator,
             denominator,
             rhs,
             constraint_tag,
         });
 
-        assert!(propagator.is_err());
+        let _ = state.propagate_to_fixed_point().unwrap_err();
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs
index 79dd4de68..7af7ea417 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs
@@ -417,44 +417,54 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
+    use pumpkin_core::predicate;
+    use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
+    use pumpkin_core::state::State;
 
     use super::*;
+    use crate::StateExt;
 
     #[test]
     fn bounds_of_a_and_b_propagate_bounds_c() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(1, 3);
-        let b = solver.new_variable(0, 4);
-        let c = solver.new_variable(-10, 20);
-
-        let constraint_tag = solver.new_constraint_tag();
-
-        let propagator = solver
-            .new_propagator(IntegerMultiplicationArgs {
-                a,
-                b,
-                c,
-                constraint_tag,
-            })
-            .expect("no empty domains");
-
-        solver.propagate(propagator).expect("no empty domains");
-
-        assert_eq!(1, solver.lower_bound(a));
-        assert_eq!(3, solver.upper_bound(a));
-        assert_eq!(0, solver.lower_bound(b));
-        assert_eq!(4, solver.upper_bound(b));
-        assert_eq!(0, solver.lower_bound(c));
-        assert_eq!(12, solver.upper_bound(c));
-
-        let reason_lb = solver.get_reason_int(predicate![c >= 0]);
+        let mut state = State::default();
+        let a = state.new_interval_variable(1, 3, None);
+        let b = state.new_interval_variable(0, 4, None);
+        let c = state.new_interval_variable(-10, 20, None);
+
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(IntegerMultiplicationArgs {
+            a,
+            b,
+            c,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
+
+        state.assert_bounds(a, 1, 3);
+        state.assert_bounds(b, 0, 4);
+        state.assert_bounds(c, 0, 12);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![c >= 0],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason_lb: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([a >= 0] & [b >= 0]), reason_lb);
 
-        let reason_ub = solver.get_reason_int(predicate![c <= 12]);
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![c <= 12],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason_ub: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
             conjunction!([a >= 0] & [a <= 3] & [b >= 0] & [b <= 4]),
             reason_ub
@@ -463,141 +473,149 @@ mod tests {
 
     #[test]
     fn bounds_of_a_and_c_propagate_bounds_b() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(2, 3);
-        let b = solver.new_variable(0, 12);
-        let c = solver.new_variable(2, 12);
-
-        let constraint_tag = solver.new_constraint_tag();
-
-        let propagator = solver
-            .new_propagator(IntegerMultiplicationArgs {
-                a,
-                b,
-                c,
-                constraint_tag,
-            })
-            .expect("no empty domains");
-
-        solver.propagate(propagator).expect("no empty domains");
-
-        assert_eq!(2, solver.lower_bound(a));
-        assert_eq!(3, solver.upper_bound(a));
-        assert_eq!(1, solver.lower_bound(b));
-        assert_eq!(6, solver.upper_bound(b));
-        assert_eq!(2, solver.lower_bound(c));
-        assert_eq!(12, solver.upper_bound(c));
-
-        let reason_lb = solver.get_reason_int(predicate![b >= 1]);
+        let mut state = State::default();
+        let a = state.new_interval_variable(2, 3, None);
+        let b = state.new_interval_variable(0, 12, None);
+        let c = state.new_interval_variable(2, 12, None);
+
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(IntegerMultiplicationArgs {
+            a,
+            b,
+            c,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
+
+        state.assert_bounds(a, 2, 3);
+        state.assert_bounds(b, 1, 6);
+        state.assert_bounds(c, 2, 12);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![b >= 1],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason_lb: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([a >= 1] & [c >= 1]), reason_lb);
 
-        let reason_ub = solver.get_reason_int(predicate![b <= 6]);
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![b <= 6],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason_ub: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([a >= 2] & [c >= 0] & [c <= 12]), reason_ub);
     }
 
     #[test]
     fn bounds_of_b_and_c_propagate_bounds_a() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(0, 10);
-        let b = solver.new_variable(3, 6);
-        let c = solver.new_variable(2, 12);
-
-        let constraint_tag = solver.new_constraint_tag();
-
-        let propagator = solver
-            .new_propagator(IntegerMultiplicationArgs {
-                a,
-                b,
-                c,
-                constraint_tag,
-            })
-            .expect("no empty domains");
-
-        solver.propagate(propagator).expect("no empty domains");
-
-        assert_eq!(1, solver.lower_bound(a));
-        assert_eq!(4, solver.upper_bound(a));
-        assert_eq!(3, solver.lower_bound(b));
-        assert_eq!(6, solver.upper_bound(b));
-        assert_eq!(3, solver.lower_bound(c));
-        assert_eq!(12, solver.upper_bound(c));
-
-        let reason_lb = solver.get_reason_int(predicate![a >= 1]);
+        let mut state = State::default();
+        let a = state.new_interval_variable(0, 10, None);
+        let b = state.new_interval_variable(3, 6, None);
+        let c = state.new_interval_variable(2, 12, None);
+
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(IntegerMultiplicationArgs {
+            a,
+            b,
+            c,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
+
+        state.assert_bounds(a, 1, 4);
+        state.assert_bounds(b, 3, 6);
+        state.assert_bounds(c, 3, 12);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![a >= 1],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason_lb: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([b >= 1] & [c >= 1]), reason_lb);
 
-        let reason_ub = solver.get_reason_int(predicate![a <= 4]);
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![a <= 4],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason_ub: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([b >= 3] & [c >= 0] & [c <= 12]), reason_ub);
     }
 
     #[test]
     fn b_unbounded_does_not_panic() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(12, 12);
-        let b = solver.new_variable(i32::MIN, i32::MAX);
-        let c = solver.new_variable(144, 144);
-
-        let constraint_tag = solver.new_constraint_tag();
-        let _ = solver
-            .new_propagator(IntegerMultiplicationArgs {
-                a,
-                b,
-                c,
-                constraint_tag,
-            })
-            .expect("No empty domains");
+        let mut state = State::default();
+        let a = state.new_interval_variable(12, 12, None);
+        let b = state.new_interval_variable(i32::MIN, i32::MAX, None);
+        let c = state.new_interval_variable(144, 144, None);
+
+        let constraint_tag = state.new_constraint_tag();
+        let _ = state.add_propagator(IntegerMultiplicationArgs {
+            a,
+            b,
+            c,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("No empty domains");
     }
 
     #[test]
     fn a_unbounded_does_not_panic() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(i32::MIN, i32::MAX);
-        let b = solver.new_variable(12, 12);
-        let c = solver.new_variable(144, 144);
-
-        let constraint_tag = solver.new_constraint_tag();
-        let _ = solver
-            .new_propagator(IntegerMultiplicationArgs {
-                a,
-                b,
-                c,
-                constraint_tag,
-            })
-            .expect("No empty domains");
+        let mut state = State::default();
+        let a = state.new_interval_variable(i32::MIN, i32::MAX, None);
+        let b = state.new_interval_variable(12, 12, None);
+        let c = state.new_interval_variable(144, 144, None);
+
+        let constraint_tag = state.new_constraint_tag();
+        let _ = state.add_propagator(IntegerMultiplicationArgs {
+            a,
+            b,
+            c,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("No empty domains");
     }
 
     #[test]
     fn c_unbounded_does_not_panic() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(12, 12);
-        let b = solver.new_variable(12, 12);
-        let c = solver.new_variable(i32::MIN, i32::MAX);
-
-        let constraint_tag = solver.new_constraint_tag();
-        let _ = solver
-            .new_propagator(IntegerMultiplicationArgs {
-                a,
-                b,
-                c,
-                constraint_tag,
-            })
-            .expect("No empty domains");
+        let mut state = State::default();
+        let a = state.new_interval_variable(12, 12, None);
+        let b = state.new_interval_variable(12, 12, None);
+        let c = state.new_interval_variable(i32::MIN, i32::MAX, None);
+
+        let constraint_tag = state.new_constraint_tag();
+        let _ = state.add_propagator(IntegerMultiplicationArgs {
+            a,
+            b,
+            c,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("No empty domains");
     }
 
     #[test]
     fn all_unbounded_does_not_panic() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(i32::MIN, i32::MAX);
-        let b = solver.new_variable(i32::MIN, i32::MAX);
-        let c = solver.new_variable(i32::MIN, i32::MAX);
-
-        let constraint_tag = solver.new_constraint_tag();
-        let _ = solver
-            .new_propagator(IntegerMultiplicationArgs {
-                a,
-                b,
-                c,
-                constraint_tag,
-            })
-            .expect("No empty domains");
+        let mut state = State::default();
+        let a = state.new_interval_variable(i32::MIN, i32::MAX, None);
+        let b = state.new_interval_variable(i32::MIN, i32::MAX, None);
+        let c = state.new_interval_variable(i32::MIN, i32::MAX, None);
+
+        let constraint_tag = state.new_constraint_tag();
+        let _ = state.add_propagator(IntegerMultiplicationArgs {
+            a,
+            b,
+            c,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("No empty domains");
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs
index e1e616574..7ccb902c1 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs
@@ -324,89 +324,95 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
     use pumpkin_core::conjunction;
+    use pumpkin_core::predicate;
+    use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
+    use pumpkin_core::state::State;
 
     use super::*;
+    use crate::StateExt;
 
     #[test]
     fn test_bounds_are_propagated() {
-        let mut solver = TestSolver::default();
-        let x = solver.new_variable(1, 5);
-        let y = solver.new_variable(0, 10);
+        let mut state = State::default();
+        let x = state.new_interval_variable(1, 5, None);
+        let y = state.new_interval_variable(0, 10, None);
 
-        let constraint_tag = solver.new_constraint_tag();
+        let constraint_tag = state.new_constraint_tag();
 
-        let propagator = solver
-            .new_propagator(LinearLessOrEqualPropagatorArgs {
-                x: [x, y].into(),
-                c: 7,
-                constraint_tag,
-            })
-            .expect("no empty domains");
-
-        solver.propagate(propagator).expect("non-empty domain");
+        let _ = state.add_propagator(LinearLessOrEqualPropagatorArgs {
+            x: [x, y].into(),
+            c: 7,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(x, 1, 5);
-        solver.assert_bounds(y, 0, 6);
+        state.assert_bounds(x, 1, 5);
+        state.assert_bounds(y, 0, 6);
     }
 
     #[test]
     fn test_explanations() {
-        let mut solver = TestSolver::default();
-        let x = solver.new_variable(1, 5);
-        let y = solver.new_variable(0, 10);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let propagator = solver
-            .new_propagator(LinearLessOrEqualPropagatorArgs {
-                x: [x, y].into(),
-                c: 7,
-                constraint_tag,
-            })
-            .expect("no empty domains");
-
-        solver.propagate(propagator).expect("non-empty domain");
-
-        let reason = solver.get_reason_int(predicate![y <= 6]);
+        let mut state = State::default();
+        let x = state.new_interval_variable(1, 5, None);
+        let y = state.new_interval_variable(0, 10, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(LinearLessOrEqualPropagatorArgs {
+            x: [x, y].into(),
+            c: 7,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![y <= 6],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
 
         assert_eq!(conjunction!([x >= 1]), reason);
     }
 
     #[test]
     fn overflow_leads_to_conflict() {
-        let mut solver = TestSolver::default();
-
-        let x = solver.new_variable(i32::MAX, i32::MAX);
-        let y = solver.new_variable(1, 1);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(LinearLessOrEqualPropagatorArgs {
-                x: [x, y].into(),
-                c: i32::MAX,
-                constraint_tag,
-            })
+        let mut state = State::default();
+
+        let x = state.new_interval_variable(i32::MAX, i32::MAX, None);
+        let y = state.new_interval_variable(1, 1, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(LinearLessOrEqualPropagatorArgs {
+            x: [x, y].into(),
+            c: i32::MAX,
+            constraint_tag,
+        });
+        let _ = state
+            .propagate_to_fixed_point()
             .expect_err("Expected overflow to be detected");
     }
 
     #[test]
     fn underflow_leads_to_no_propagation() {
-        let mut solver = TestSolver::default();
-
-        let x = solver.new_variable(i32::MIN, i32::MIN);
-        let y = solver.new_variable(-1, -1);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(LinearLessOrEqualPropagatorArgs {
-                x: [x, y].into(),
-                c: i32::MIN,
-                constraint_tag,
-            })
+        let mut state = State::default();
+
+        let x = state.new_interval_variable(i32::MIN, i32::MIN, None);
+        let y = state.new_interval_variable(-1, -1, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(LinearLessOrEqualPropagatorArgs {
+            x: [x, y].into(),
+            c: i32::MIN,
+            constraint_tag,
+        });
+        state
+            .propagate_to_fixed_point()
             .expect("Expected no error to be detected");
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs
index 31f8a96e3..c91a57c3a 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs
@@ -402,54 +402,54 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
     use pumpkin_core::conjunction;
+    use pumpkin_core::predicate;
+    use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
     use pumpkin_core::state::Conflict;
+    use pumpkin_core::state::State;
     use pumpkin_core::variables::TransformableVariable;
 
     use super::*;
+    use crate::StateExt;
 
     #[test]
     fn test_value_is_removed() {
-        let mut solver = TestSolver::default();
-        let x = solver.new_variable(2, 2);
-        let y = solver.new_variable(1, 5);
+        let mut state = State::default();
+        let x = state.new_interval_variable(2, 2, None);
+        let y = state.new_interval_variable(1, 5, None);
 
-        let constraint_tag = solver.new_constraint_tag();
+        let constraint_tag = state.new_constraint_tag();
 
-        let propagator = solver
-            .new_propagator(LinearNotEqualPropagatorArgs {
-                terms: [x.scaled(1), y.scaled(-1)].into(),
-                rhs: 0,
-                constraint_tag,
-            })
-            .expect("non-empty domain");
-
-        solver.propagate(propagator).expect("non-empty domain");
+        let _ = state.add_propagator(LinearNotEqualPropagatorArgs {
+            terms: [x.scaled(1), y.scaled(-1)].into(),
+            rhs: 0,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("non-empty domain");
 
-        solver.assert_bounds(x, 2, 2);
-        solver.assert_bounds(y, 1, 5);
-        assert!(!solver.contains(y, 2));
+        state.assert_bounds(x, 2, 2);
+        state.assert_bounds(y, 1, 5);
+        assert!(!state.contains(y, 2));
     }
 
     #[test]
     fn test_empty_domain_is_detected() {
-        let mut solver = TestSolver::default();
-        let x = solver.new_variable(2, 2);
-        let y = solver.new_variable(2, 2);
+        let mut state = State::default();
+        let x = state.new_interval_variable(2, 2, None);
+        let y = state.new_interval_variable(2, 2, None);
 
-        let constraint_tag = solver.new_constraint_tag();
+        let constraint_tag = state.new_constraint_tag();
 
-        let err = solver
-            .new_propagator(LinearNotEqualPropagatorArgs {
-                terms: [x.scaled(1), y.scaled(-1)].into(),
-                rhs: 0,
-                constraint_tag,
-            })
-            .expect_err("empty domain");
+        let _ = state.add_propagator(LinearNotEqualPropagatorArgs {
+            terms: [x.scaled(1), y.scaled(-1)].into(),
+            rhs: 0,
+            constraint_tag,
+        });
+        let err = state.propagate_to_fixed_point().expect_err("empty domain");
 
         let expected = conjunction!([x == 2] & [y == 2]);
 
@@ -461,53 +461,52 @@ mod tests {
 
     #[test]
     fn explanation_for_propagation() {
-        let mut solver = TestSolver::default();
-        let x = solver.new_variable(2, 2).scaled(1);
-        let y = solver.new_variable(1, 5).scaled(-1);
-
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let x = state.new_interval_variable(2, 2, None).scaled(1);
+        let y = state.new_interval_variable(1, 5, None).scaled(-1);
 
-        let propagator = solver
-            .new_propagator(LinearNotEqualPropagatorArgs {
-                terms: [x, y].into(),
-                rhs: 0,
-                constraint_tag,
-            })
-            .expect("non-empty domain");
+        let constraint_tag = state.new_constraint_tag();
 
-        solver.propagate(propagator).expect("non-empty domain");
-
-        let reason = solver.get_reason_int(predicate![y != -2]);
+        let _ = state.add_propagator(LinearNotEqualPropagatorArgs {
+            terms: [x, y].into(),
+            rhs: 0,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("non-empty domain");
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![y != -2],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
 
         assert_eq!(conjunction!([x == 2]), reason);
     }
 
     #[test]
     fn satisfied_constraint_does_not_trigger_conflict() {
-        let mut solver = TestSolver::default();
-        let x = solver.new_variable(0, 3);
-        let y = solver.new_variable(0, 3);
+        let mut state = State::default();
+        let x = state.new_interval_variable(0, 3, None);
+        let y = state.new_interval_variable(0, 3, None);
 
-        let constraint_tag = solver.new_constraint_tag();
+        let constraint_tag = state.new_constraint_tag();
 
-        let propagator = solver
-            .new_propagator(LinearNotEqualPropagatorArgs {
-                terms: [x.scaled(1), y.scaled(-1)].into(),
-                rhs: 0,
-                constraint_tag,
-            })
-            .expect("non-empty domain");
-
-        solver.remove(x, 0).expect("non-empty domain");
-        solver.remove(x, 2).expect("non-empty domain");
-        solver.remove(x, 3).expect("non-empty domain");
+        let _ = state.add_propagator(LinearNotEqualPropagatorArgs {
+            terms: [x.scaled(1), y.scaled(-1)].into(),
+            rhs: 0,
+            constraint_tag,
+        });
 
-        solver.remove(y, 0).expect("non-empty domain");
-        solver.remove(y, 1).expect("non-empty domain");
-        solver.remove(y, 2).expect("non-empty domain");
+        let _ = state.post(predicate![x != 0]).unwrap();
+        let _ = state.post(predicate![x != 2]).unwrap();
+        let _ = state.post(predicate![x != 3]).unwrap();
 
-        solver.notify_propagator(propagator);
+        let _ = state.post(predicate![y != 0]).unwrap();
+        let _ = state.post(predicate![y != 1]).unwrap();
+        let _ = state.post(predicate![y != 2]).unwrap();
 
-        solver.propagate(propagator).expect("non-empty domain");
+        state.propagate_to_fixed_point().expect("non-empty domain");
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs
index d1f927697..f59252ba2 100644
--- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs
+++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs
@@ -224,109 +224,128 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
+    use pumpkin_core::predicate;
+    use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
+    use pumpkin_core::state::State;
 
     use super::*;
+    use crate::StateExt;
 
     #[test]
     fn upper_bound_of_rhs_matches_maximum_upper_bound_of_array_at_initialise() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let a = solver.new_variable(1, 3);
-        let b = solver.new_variable(1, 4);
-        let c = solver.new_variable(1, 5);
+        let a = state.new_interval_variable(1, 3, None);
+        let b = state.new_interval_variable(1, 4, None);
+        let c = state.new_interval_variable(1, 5, None);
 
-        let rhs = solver.new_variable(1, 10);
-        let constraint_tag = solver.new_constraint_tag();
+        let rhs = state.new_interval_variable(1, 10, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(MaximumArgs {
-                array: [a, b, c].into(),
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domain");
+        let _ = state.add_propagator(MaximumArgs {
+            array: [a, b, c].into(),
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domain");
 
-        solver.assert_bounds(rhs, 1, 5);
+        state.assert_bounds(rhs, 1, 5);
 
-        let reason = solver.get_reason_int(predicate![rhs <= 5]);
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![rhs <= 5],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([a <= 5] & [b <= 5] & [c <= 5]), reason);
     }
 
     #[test]
     fn lower_bound_of_rhs_is_maximum_of_lower_bounds_in_array() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let a = solver.new_variable(3, 10);
-        let b = solver.new_variable(4, 10);
-        let c = solver.new_variable(5, 10);
+        let a = state.new_interval_variable(3, 10, None);
+        let b = state.new_interval_variable(4, 10, None);
+        let c = state.new_interval_variable(5, 10, None);
 
-        let rhs = solver.new_variable(1, 10);
-        let constraint_tag = solver.new_constraint_tag();
+        let rhs = state.new_interval_variable(1, 10, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(MaximumArgs {
-                array: [a, b, c].into(),
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domain");
+        let _ = state.add_propagator(MaximumArgs {
+            array: [a, b, c].into(),
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domain");
 
-        solver.assert_bounds(rhs, 5, 10);
+        state.assert_bounds(rhs, 5, 10);
 
-        let reason = solver.get_reason_int(predicate![rhs >= 5]);
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![rhs >= 5],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([c >= 5]), reason);
     }
 
     #[test]
     fn upper_bound_of_all_array_elements_at_most_rhs_max_at_initialise() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
         let array = (1..=5)
-            .map(|idx| solver.new_variable(1, 4 + idx))
+            .map(|idx| state.new_interval_variable(1, 4 + idx, None))
             .collect::<Box<_>>();
 
-        let rhs = solver.new_variable(1, 3);
-        let constraint_tag = solver.new_constraint_tag();
+        let rhs = state.new_interval_variable(1, 3, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(MaximumArgs {
-                array: array.clone(),
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domain");
+        let _ = state.add_propagator(MaximumArgs {
+            array: array.clone(),
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domain");
 
         for var in array.iter() {
-            solver.assert_bounds(*var, 1, 3);
-            let reason = solver.get_reason_int(predicate![var <= 3]);
+            state.assert_bounds(*var, 1, 3);
+
+            let mut reason_buffer: Vec<Predicate> = vec![];
+            let _ = state.get_propagation_reason(
+                predicate![var <= 3],
+                &mut reason_buffer,
+                CurrentNogood::empty(),
+            );
+            let reason: PropositionalConjunction = reason_buffer.into();
             assert_eq!(conjunction!([rhs <= 3]), reason);
         }
     }
 
     #[test]
     fn single_variable_propagate() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
         let array = (1..=5)
-            .map(|idx| solver.new_variable(1, 1 + 10 * idx))
+            .map(|idx| state.new_interval_variable(1, 1 + 10 * idx, None))
             .collect::<Box<_>>();
 
-        let rhs = solver.new_variable(45, 60);
-        let constraint_tag = solver.new_constraint_tag();
+        let rhs = state.new_interval_variable(45, 60, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(MaximumArgs {
-                array: array.clone(),
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domain");
+        let _ = state.add_propagator(MaximumArgs {
+            array: array.clone(),
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domain");
 
-        solver.assert_bounds(*array.last().unwrap(), 45, 51);
-        solver.assert_bounds(rhs, 45, 51);
+        state.assert_bounds(*array.last().unwrap(), 45, 51);
+        state.assert_bounds(rhs, 45, 51);
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs
index 07e5b8cb2..ffe3e0b91 100644
--- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs
+++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs
@@ -649,17 +649,24 @@ fn find_overlapping_profile<Var: IntegerVariable + 'static>(
     })
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
+    #[allow(
+        deprecated,
+        reason = "TestSolver is deprecated but still used in these tests"
+    )]
     use pumpkin_core::TestSolver;
     use pumpkin_core::conjunction;
     use pumpkin_core::predicate;
     use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
     use pumpkin_core::propagation::EnqueueDecision;
     use pumpkin_core::state::Conflict;
+    use pumpkin_core::state::State;
     use pumpkin_core::variables::DomainId;
 
+    use crate::StateExt;
     use crate::cumulative::ArgTask;
     use crate::cumulative::options::CumulativePropagatorOptions;
     use crate::cumulative::time_table::CumulativeExplanationType;
@@ -667,188 +674,187 @@ mod tests {
 
     #[test]
     fn propagator_propagates_from_profile() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions::default(),
+                constraint_tag,
+            ),
+        );
 
-        let _ = solver
-            .new_propagator(
-                TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions::default(),
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
+        state.propagate_to_fixed_point().expect("No conflict");
+
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
     }
 
     #[test]
     fn propagator_detects_conflict() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 1);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let result = solver.new_propagator(TimeTableOverIntervalIncrementalPropagator::<
-            DomainId,
-            false,
-        >::new(
-            &[
-                ArgTask {
-                    start_time: s1,
-                    processing_time: 4,
-                    resource_usage: 1,
-                },
-                ArgTask {
-                    start_time: s2,
-                    processing_time: 4,
-                    resource_usage: 1,
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 1, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    ..Default::default()
                 },
-            ]
-            .into_iter()
-            .collect::<Vec<_>>(),
-            1,
-            CumulativePropagatorOptions {
-                explanation_type: CumulativeExplanationType::Naive,
-                ..Default::default()
-            },
-            constraint_tag,
-        ));
-
-        assert!(matches!(result, Err(Conflict::Propagator(_))));
-        assert!(match result {
-            Err(Conflict::Propagator(conflict)) => {
-                let expected = [
-                    predicate!(s1 <= 1),
-                    predicate!(s1 >= 1),
-                    predicate!(s2 >= 1),
-                    predicate!(s2 <= 1),
-                ];
-                expected.iter().all(|y| {
-                    conflict
-                        .conjunction
-                        .iter()
-                        .collect::<Vec<&Predicate>>()
-                        .contains(&y)
-                }) && conflict.conjunction.iter().all(|y| expected.contains(y))
-            }
-            _ => false,
-        });
+                constraint_tag,
+            ),
+        );
+
+        let Conflict::Propagator(conflict) = state.propagate_to_fixed_point().unwrap_err() else {
+            panic!("an explicit conflict should be detected");
+        };
+
+        let expected = [
+            predicate!(s1 <= 1),
+            predicate!(s1 >= 1),
+            predicate!(s2 >= 1),
+            predicate!(s2 <= 1),
+        ];
+
+        assert!(expected.iter().all(|y| {
+            conflict
+                .conjunction
+                .iter()
+                .collect::<Vec<&Predicate>>()
+                .contains(&y)
+        }));
+
+        assert!(conflict.conjunction.iter().all(|y| expected.contains(y)));
     }
 
     #[test]
     fn propagator_propagates_nothing() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(0, 6);
-        let s2 = solver.new_variable(0, 6);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(
-                TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions::default(),
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 6);
-        assert_eq!(solver.lower_bound(s1), 0);
-        assert_eq!(solver.upper_bound(s1), 6);
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(0, 6, None);
+        let s2 = state.new_interval_variable(0, 6, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions::default(),
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 0, 6);
+        state.assert_bounds(s2, 0, 6);
     }
 
     #[test]
     fn propagator_propagates_example_4_3_schutt() {
-        let mut solver = TestSolver::default();
-        let f = solver.new_variable(0, 14);
-        let e = solver.new_variable(2, 4);
-        let d = solver.new_variable(0, 2);
-        let c = solver.new_variable(8, 9);
-        let b = solver.new_variable(2, 3);
-        let a = solver.new_variable(0, 1);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(
-                TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: a,
-                            processing_time: 2,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: b,
-                            processing_time: 6,
-                            resource_usage: 2,
-                        },
-                        ArgTask {
-                            start_time: c,
-                            processing_time: 2,
-                            resource_usage: 4,
-                        },
-                        ArgTask {
-                            start_time: d,
-                            processing_time: 2,
-                            resource_usage: 2,
-                        },
-                        ArgTask {
-                            start_time: e,
-                            processing_time: 5,
-                            resource_usage: 2,
-                        },
-                        ArgTask {
-                            start_time: f,
-                            processing_time: 6,
-                            resource_usage: 2,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    5,
-                    CumulativePropagatorOptions::default(),
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(f), 10);
+        let mut state = State::default();
+        let f = state.new_interval_variable(0, 14, None);
+        let e = state.new_interval_variable(2, 4, None);
+        let d = state.new_interval_variable(0, 2, None);
+        let c = state.new_interval_variable(8, 9, None);
+        let b = state.new_interval_variable(2, 3, None);
+        let a = state.new_interval_variable(0, 1, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: a,
+                        processing_time: 2,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: b,
+                        processing_time: 6,
+                        resource_usage: 2,
+                    },
+                    ArgTask {
+                        start_time: c,
+                        processing_time: 2,
+                        resource_usage: 4,
+                    },
+                    ArgTask {
+                        start_time: d,
+                        processing_time: 2,
+                        resource_usage: 2,
+                    },
+                    ArgTask {
+                        start_time: e,
+                        processing_time: 5,
+                        resource_usage: 2,
+                    },
+                    ArgTask {
+                        start_time: f,
+                        processing_time: 6,
+                        resource_usage: 2,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                5,
+                CumulativePropagatorOptions::default(),
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        assert_eq!(state.lower_bound(f), 10);
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_after_assignment() {
         let mut solver = TestSolver::default();
         let s1 = solver.new_variable(0, 6);
@@ -898,47 +904,54 @@ mod tests {
 
     #[test]
     fn propagator_propagates_end_time() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(6, 6);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(
-                TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        ..Default::default()
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(6, 6, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 1);
-        assert_eq!(solver.upper_bound(s2), 3);
-        assert_eq!(solver.lower_bound(s1), 6);
-        assert_eq!(solver.upper_bound(s1), 6);
-
-        let reason = solver.get_reason_int(predicate!(s2 <= 3));
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 6, 6);
+        state.assert_bounds(s2, 1, 3);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 <= 3),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([s2 <= 8] & [s1 >= 6] & [s1 <= 6]), reason);
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_example_4_3_schutt_after_update() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
@@ -1016,6 +1029,10 @@ mod tests {
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_example_4_3_schutt_multiple_profiles() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
@@ -1098,138 +1115,147 @@ mod tests {
 
     #[test]
     fn propagator_propagates_from_profile_reason() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(
-                TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        ..Default::default()
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
-
-        let reason = solver.get_reason_int(predicate!(s2 >= 5));
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 >= 5),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([s2 >= 1] & [s1 >= 1] & [s1 <= 1]), reason);
     }
 
     #[test]
     fn propagator_propagates_generic_bounds() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(3, 3);
-        let s2 = solver.new_variable(5, 5);
-        let s3 = solver.new_variable(1, 15);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(
-                TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 2,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 2,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s3,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        ..Default::default()
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(3, 3, None);
+        let s2 = state.new_interval_variable(5, 5, None);
+        let s3 = state.new_interval_variable(1, 15, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 2,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s3), 7);
-        assert_eq!(solver.upper_bound(s3), 15);
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 5);
-        assert_eq!(solver.lower_bound(s1), 3);
-        assert_eq!(solver.upper_bound(s1), 3);
-
-        let reason = solver.get_reason_int(predicate!(s3 >= 7));
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 2,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: s3,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 3, 3);
+        state.assert_bounds(s2, 5, 5);
+        state.assert_bounds(s3, 7, 15);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s3 >= 7),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([s2 <= 5] & [s2 >= 5] & [s3 >= 5]), reason);
     }
 
     #[test]
     fn propagator_propagates_with_holes() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(4, 4);
-        let s2 = solver.new_variable(0, 8);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(
-                TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        allow_holes_in_domain: true,
-                        ..Default::default()
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(4, 4, None);
+        let s2 = state.new_interval_variable(0, 8, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTableOverIntervalIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 4);
-        assert_eq!(solver.upper_bound(s1), 4);
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    allow_holes_in_domain: true,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+
+        state.assert_bounds(s1, 4, 4);
+        state.assert_bounds(s2, 0, 8);
 
         for removed in 2..8 {
-            assert!(!solver.contains(s2, removed));
-            let reason = solver.get_reason_int(predicate!(s2 != removed));
+            assert!(!state.contains(s2, removed));
+            let mut reason_buffer: Vec<Predicate> = vec![];
+            let _ = state.get_propagation_reason(
+                predicate!(s2 != removed),
+                &mut reason_buffer,
+                CurrentNogood::empty(),
+            );
+            let reason: PropositionalConjunction = reason_buffer.into();
             assert_eq!(conjunction!([s1 <= 4] & [s1 >= 4]), reason);
         }
     }
diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs
index c5e9e40c9..fca2a5be2 100644
--- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs
+++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs
@@ -160,13 +160,12 @@ fn sort_profile_based_on_id<Var: IntegerVariable + 'static>(profile: &mut Resour
     profile.profile_tasks.sort_by_key(|task| task.id.unpack());
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
     use std::rc::Rc;
 
-    use pumpkin_core::TestSolver;
     use pumpkin_core::propagation::LocalId;
+    use pumpkin_core::state::State;
 
     use super::find_synchronised_conflict;
     use crate::cumulative::CumulativeParameters;
@@ -177,11 +176,11 @@ mod tests {
 
     #[test]
     fn test_correct_conflict_returned() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let x0 = solver.new_variable(0, 10);
-        let x1 = solver.new_variable(0, 10);
-        let x2 = solver.new_variable(0, 10);
+        let x0 = state.new_interval_variable(0, 10, None);
+        let x1 = state.new_interval_variable(0, 10, None);
+        let x2 = state.new_interval_variable(0, 10, None);
 
         let tasks = vec![
             Task {
diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs
index 3ab30639d..955e8d531 100644
--- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs
+++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs
@@ -646,17 +646,24 @@ mod debug {
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
+    #[allow(
+        deprecated,
+        reason = "TestSolver is deprecated but still used in these tests"
+    )]
     use pumpkin_core::TestSolver;
     use pumpkin_core::conjunction;
     use pumpkin_core::predicate;
     use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
     use pumpkin_core::propagation::EnqueueDecision;
     use pumpkin_core::state::Conflict;
+    use pumpkin_core::state::State;
     use pumpkin_core::variables::DomainId;
 
+    use crate::StateExt;
     use crate::cumulative::ArgTask;
     use crate::cumulative::options::CumulativePropagatorOptions;
     use crate::cumulative::time_table::CumulativeExplanationType;
@@ -665,48 +672,45 @@ mod tests {
 
     #[test]
     fn propagator_propagates_from_profile() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(
-                TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions::default(),
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
+        let _ = state.add_propagator(
+            TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions::default(),
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
     }
 
     #[test]
     fn propagator_detects_conflict() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 1);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 1, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let result = solver.new_propagator(
+        let _ = state.add_propagator(
             TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
                 &[
                     ArgTask {
@@ -730,119 +734,121 @@ mod tests {
                 constraint_tag,
             ),
         );
-        assert!(match result {
-            Err(Conflict::Propagator(x)) => {
-                let expected = [
-                    predicate!(s1 <= 1),
-                    predicate!(s1 >= 1),
-                    predicate!(s2 <= 1),
-                    predicate!(s2 >= 1),
-                ];
-                expected.iter().all(|y| {
-                    x.conjunction
-                        .iter()
-                        .collect::<Vec<&Predicate>>()
-                        .contains(&y)
-                }) && x.conjunction.iter().all(|y| expected.contains(y))
-            }
-            _ => false,
-        });
+        let Conflict::Propagator(x) = state.propagate_to_fixed_point().unwrap_err() else {
+            panic!("an explicit conflict should have been detected");
+        };
+
+        let expected = [
+            predicate!(s1 <= 1),
+            predicate!(s1 >= 1),
+            predicate!(s2 <= 1),
+            predicate!(s2 >= 1),
+        ];
+
+        assert!(expected.iter().all(|y| {
+            x.conjunction
+                .iter()
+                .collect::<Vec<&Predicate>>()
+                .contains(&y)
+        }));
+
+        assert!(x.conjunction.iter().all(|y| expected.contains(y)));
     }
 
     #[test]
     fn propagator_propagates_nothing() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(0, 6);
-        let s2 = solver.new_variable(0, 6);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(0, 6, None);
+        let s2 = state.new_interval_variable(0, 6, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(
-                TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions::default(),
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 6);
-        assert_eq!(solver.lower_bound(s1), 0);
-        assert_eq!(solver.upper_bound(s1), 6);
+        let _ = state.add_propagator(
+            TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions::default(),
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 0, 6);
+        state.assert_bounds(s2, 0, 6);
     }
 
     #[test]
     fn propagator_propagates_example_4_3_schutt() {
-        let mut solver = TestSolver::default();
-        let f = solver.new_variable(0, 14);
-        let e = solver.new_variable(2, 4);
-        let d = solver.new_variable(0, 2);
-        let c = solver.new_variable(8, 9);
-        let b = solver.new_variable(2, 3);
-        let a = solver.new_variable(0, 1);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(
-                TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: a,
-                            processing_time: 2,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: b,
-                            processing_time: 6,
-                            resource_usage: 2,
-                        },
-                        ArgTask {
-                            start_time: c,
-                            processing_time: 2,
-                            resource_usage: 4,
-                        },
-                        ArgTask {
-                            start_time: d,
-                            processing_time: 2,
-                            resource_usage: 2,
-                        },
-                        ArgTask {
-                            start_time: e,
-                            processing_time: 5,
-                            resource_usage: 2,
-                        },
-                        ArgTask {
-                            start_time: f,
-                            processing_time: 6,
-                            resource_usage: 2,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    5,
-                    CumulativePropagatorOptions::default(),
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(f), 10);
+        let mut state = State::default();
+        let f = state.new_interval_variable(0, 14, None);
+        let e = state.new_interval_variable(2, 4, None);
+        let d = state.new_interval_variable(0, 2, None);
+        let c = state.new_interval_variable(8, 9, None);
+        let b = state.new_interval_variable(2, 3, None);
+        let a = state.new_interval_variable(0, 1, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(
+            TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: a,
+                        processing_time: 2,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: b,
+                        processing_time: 6,
+                        resource_usage: 2,
+                    },
+                    ArgTask {
+                        start_time: c,
+                        processing_time: 2,
+                        resource_usage: 4,
+                    },
+                    ArgTask {
+                        start_time: d,
+                        processing_time: 2,
+                        resource_usage: 2,
+                    },
+                    ArgTask {
+                        start_time: e,
+                        processing_time: 5,
+                        resource_usage: 2,
+                    },
+                    ArgTask {
+                        start_time: f,
+                        processing_time: 6,
+                        resource_usage: 2,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                5,
+                CumulativePropagatorOptions::default(),
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        assert_eq!(state.lower_bound(f), 10);
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_after_assignment() {
         let mut solver = TestSolver::default();
         let s1 = solver.new_variable(0, 6);
@@ -892,49 +898,54 @@ mod tests {
 
     #[test]
     fn propagator_propagates_end_time() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(6, 6);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(6, 6, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let propagator = solver
-            .new_propagator(
-                TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        ..Default::default()
+        let _ = state.add_propagator(
+            TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        let result = solver.propagate_until_fixed_point(propagator);
-        assert!(result.is_ok());
-        assert_eq!(solver.lower_bound(s2), 1);
-        assert_eq!(solver.upper_bound(s2), 3);
-        assert_eq!(solver.lower_bound(s1), 6);
-        assert_eq!(solver.upper_bound(s1), 6);
-
-        let reason = solver.get_reason_int(predicate!(s2 <= 3));
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 6, 6);
+        state.assert_bounds(s2, 1, 3);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 <= 3),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([s2 <= 5] & [s1 >= 6] & [s1 <= 6]), reason);
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_example_4_3_schutt_after_update() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
@@ -1012,6 +1023,10 @@ mod tests {
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_example_4_3_schutt_multiple_profiles() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
@@ -1094,43 +1109,46 @@ mod tests {
 
     #[test]
     fn propagator_propagates_from_profile_reason() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(
-                TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        ..Default::default()
+        let _ = state.add_propagator(
+            TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
-
-        let reason = solver.get_reason_int(predicate!(s2 >= 5));
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 >= 5),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
             conjunction!([s2 >= 4] & [s1 >= 1] & [s1 <= 1]), /* Note that this not
                                                               * the most general
@@ -1146,51 +1164,53 @@ mod tests {
 
     #[test]
     fn propagator_propagates_generic_bounds() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(3, 3);
-        let s2 = solver.new_variable(5, 5);
-        let s3 = solver.new_variable(1, 15);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(3, 3, None);
+        let s2 = state.new_interval_variable(5, 5, None);
+        let s3 = state.new_interval_variable(1, 15, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(
-                TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 2,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 2,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s3,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        ..Default::default()
+        let _ = state.add_propagator(
+            TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 2,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s3), 7);
-        assert_eq!(solver.upper_bound(s3), 15);
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 5);
-        assert_eq!(solver.lower_bound(s1), 3);
-        assert_eq!(solver.upper_bound(s1), 3);
-
-        let reason = solver.get_reason_int(predicate!(s3 >= 7));
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 2,
+                        resource_usage: 1,
+                    },
+                    ArgTask {
+                        start_time: s3,
+                        processing_time: 4,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 3, 3);
+        state.assert_bounds(s2, 5, 5);
+        state.assert_bounds(s3, 7, 15);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s3 >= 7),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
             conjunction!([s2 <= 5] & [s2 >= 5] & [s3 >= 6]), /* Note that s3 would
                                                               * have been able to
@@ -1203,51 +1223,58 @@ mod tests {
 
     #[test]
     fn propagator_propagates_with_holes() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(4, 4);
-        let s2 = solver.new_variable(0, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(4, 4, None);
+        let s2 = state.new_interval_variable(0, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(
-                TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
-                    &[
-                        ArgTask {
-                            start_time: s1,
-                            processing_time: 4,
-                            resource_usage: 1,
-                        },
-                        ArgTask {
-                            start_time: s2,
-                            processing_time: 3,
-                            resource_usage: 1,
-                        },
-                    ]
-                    .into_iter()
-                    .collect::<Vec<_>>(),
-                    1,
-                    CumulativePropagatorOptions {
-                        explanation_type: CumulativeExplanationType::Naive,
-                        allow_holes_in_domain: true,
-                        ..Default::default()
+        let _ = state.add_propagator(
+            TimeTablePerPointIncrementalPropagator::<DomainId, false>::new(
+                &[
+                    ArgTask {
+                        start_time: s1,
+                        processing_time: 4,
+                        resource_usage: 1,
                     },
-                    constraint_tag,
-                ),
-            )
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 4);
-        assert_eq!(solver.upper_bound(s1), 4);
+                    ArgTask {
+                        start_time: s2,
+                        processing_time: 3,
+                        resource_usage: 1,
+                    },
+                ]
+                .into_iter()
+                .collect::<Vec<_>>(),
+                1,
+                CumulativePropagatorOptions {
+                    explanation_type: CumulativeExplanationType::Naive,
+                    allow_holes_in_domain: true,
+                    ..Default::default()
+                },
+                constraint_tag,
+            ),
+        );
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 4, 4);
+        state.assert_bounds(s2, 0, 8);
 
         for removed in 2..8 {
-            assert!(!solver.contains(s2, removed));
-            let reason = solver.get_reason_int(predicate!(s2 != removed));
+            assert!(!state.contains(s2, removed));
+            let mut reason_buffer: Vec<Predicate> = vec![];
+            let _ = state.get_propagation_reason(
+                predicate!(s2 != removed),
+                &mut reason_buffer,
+                CurrentNogood::empty(),
+            );
+            let reason: PropositionalConjunction = reason_buffer.into();
             assert_eq!(conjunction!([s1 <= 4] & [s1 >= 4]), reason);
         }
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn synchronisation_leads_to_same_conflict_explanation() {
         let mut solver_scratch = TestSolver::default();
         let s1_scratch = solver_scratch.new_variable(5, 5);
@@ -1346,6 +1373,10 @@ mod tests {
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn synchronisation_leads_to_same_conflict_after_propagating() {
         let mut solver_scratch = TestSolver::default();
         let s1_scratch = solver_scratch.new_variable(5, 5);
@@ -1443,6 +1474,10 @@ mod tests {
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn no_synchronisation_leads_to_different_conflict_explanation() {
         let mut solver_scratch = TestSolver::default();
         let s1_scratch = solver_scratch.new_variable(5, 5);
@@ -1538,6 +1573,10 @@ mod tests {
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn synchronisation_leads_to_same_explanation() {
         let mut solver_scratch = TestSolver::default();
         let s1_scratch = solver_scratch.new_variable(1, 6);
@@ -1632,6 +1671,10 @@ mod tests {
         );
     }
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn no_synchronisation_leads_to_different_explanation() {
         let mut solver_scratch = TestSolver::default();
         let s1_scratch = solver_scratch.new_variable(1, 6);
@@ -1729,6 +1772,10 @@ mod tests {
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn synchronisation_leads_to_same_conflict() {
         let mut solver_scratch = TestSolver::default();
         let s0_scratch = solver_scratch.new_variable(1, 11);
diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs
index 3d3640783..9dbf8f62c 100644
--- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs
+++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs
@@ -490,16 +490,23 @@ pub(crate) fn propagate_from_scratch_time_table_interval<Var: IntegerVariable +
     )
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
+    #[allow(
+        deprecated,
+        reason = "TestSolver is deprecated but still used in these tests"
+    )]
     use pumpkin_core::TestSolver;
     use pumpkin_core::conjunction;
     use pumpkin_core::predicate;
     use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
     use pumpkin_core::propagation::EnqueueDecision;
     use pumpkin_core::state::Conflict;
+    use pumpkin_core::state::State;
 
+    use crate::StateExt;
     use crate::cumulative::ArgTask;
     use crate::cumulative::options::CumulativePropagatorOptions;
     use crate::cumulative::time_table::CumulativeExplanationType;
@@ -507,46 +514,43 @@ mod tests {
 
     #[test]
     fn propagator_propagates_from_profile() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTableOverIntervalPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions::default(),
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions::default(),
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
     }
 
     #[test]
     fn propagator_detects_conflict() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 1);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 1, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let result = solver.new_propagator(TimeTableOverIntervalPropagator::new(
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
             &[
                 ArgTask {
                     start_time: s1,
@@ -569,120 +573,117 @@ mod tests {
             constraint_tag,
         ));
 
-        assert!(match result {
-            Err(e) => {
-                match e {
-                    Conflict::EmptyDomain(_) => false,
-                    Conflict::Propagator(x) => {
-                        let expected = [
-                            predicate!(s1 <= 1),
-                            predicate!(s1 >= 1),
-                            predicate!(s2 >= 1),
-                            predicate!(s2 <= 1),
-                        ];
-                        expected.iter().all(|y| {
-                            x.conjunction
-                                .iter()
-                                .collect::<Vec<&Predicate>>()
-                                .contains(&y)
-                        }) && x.conjunction.iter().all(|y| expected.contains(y))
-                    }
-                }
-            }
-            _ => false,
-        });
+        let Conflict::Propagator(x) = state.propagate_to_fixed_point().unwrap_err() else {
+            panic!("an explicit conflict should have been detected");
+        };
+
+        let expected = [
+            predicate!(s1 <= 1),
+            predicate!(s1 >= 1),
+            predicate!(s2 >= 1),
+            predicate!(s2 <= 1),
+        ];
+
+        assert!(expected.iter().all(|y| {
+            x.conjunction
+                .iter()
+                .collect::<Vec<&Predicate>>()
+                .contains(&y)
+        }));
+
+        assert!(x.conjunction.iter().all(|y| expected.contains(y)));
     }
 
     #[test]
     fn propagator_propagates_nothing() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(0, 6);
-        let s2 = solver.new_variable(0, 6);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(0, 6, None);
+        let s2 = state.new_interval_variable(0, 6, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTableOverIntervalPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions::default(),
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 6);
-        assert_eq!(solver.lower_bound(s1), 0);
-        assert_eq!(solver.upper_bound(s1), 6);
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions::default(),
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 0, 6);
+        state.assert_bounds(s2, 0, 6);
     }
 
     #[test]
     fn propagator_propagates_example_4_3_schutt() {
-        let mut solver = TestSolver::default();
-        let f = solver.new_variable(0, 14);
-        let e = solver.new_variable(2, 4);
-        let d = solver.new_variable(0, 2);
-        let c = solver.new_variable(8, 9);
-        let b = solver.new_variable(2, 3);
-        let a = solver.new_variable(0, 1);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(TimeTableOverIntervalPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: a,
-                        processing_time: 2,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: b,
-                        processing_time: 6,
-                        resource_usage: 2,
-                    },
-                    ArgTask {
-                        start_time: c,
-                        processing_time: 2,
-                        resource_usage: 4,
-                    },
-                    ArgTask {
-                        start_time: d,
-                        processing_time: 2,
-                        resource_usage: 2,
-                    },
-                    ArgTask {
-                        start_time: e,
-                        processing_time: 5,
-                        resource_usage: 2,
-                    },
-                    ArgTask {
-                        start_time: f,
-                        processing_time: 6,
-                        resource_usage: 2,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                5,
-                CumulativePropagatorOptions::default(),
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(f), 10);
+        let mut state = State::default();
+        let f = state.new_interval_variable(0, 14, None);
+        let e = state.new_interval_variable(2, 4, None);
+        let d = state.new_interval_variable(0, 2, None);
+        let c = state.new_interval_variable(8, 9, None);
+        let b = state.new_interval_variable(2, 3, None);
+        let a = state.new_interval_variable(0, 1, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
+            &[
+                ArgTask {
+                    start_time: a,
+                    processing_time: 2,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: b,
+                    processing_time: 6,
+                    resource_usage: 2,
+                },
+                ArgTask {
+                    start_time: c,
+                    processing_time: 2,
+                    resource_usage: 4,
+                },
+                ArgTask {
+                    start_time: d,
+                    processing_time: 2,
+                    resource_usage: 2,
+                },
+                ArgTask {
+                    start_time: e,
+                    processing_time: 5,
+                    resource_usage: 2,
+                },
+                ArgTask {
+                    start_time: f,
+                    processing_time: 6,
+                    resource_usage: 2,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            5,
+            CumulativePropagatorOptions::default(),
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        assert_eq!(state.lower_bound(f), 10);
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_after_assignment() {
         let mut solver = TestSolver::default();
         let s1 = solver.new_variable(0, 6);
@@ -710,10 +711,8 @@ mod tests {
                 constraint_tag,
             ))
             .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 6);
-        assert_eq!(solver.upper_bound(s2), 10);
-        assert_eq!(solver.lower_bound(s1), 0);
-        assert_eq!(solver.upper_bound(s1), 6);
+        solver.assert_bounds(s1, 0, 6);
+        solver.assert_bounds(s2, 6, 10);
         let notification_status = solver.increase_lower_bound_and_notify(propagator, 0, s1, 5);
         assert!(match notification_status {
             EnqueueDecision::Enqueue => true,
@@ -722,61 +721,68 @@ mod tests {
 
         let result = solver.propagate(propagator);
         assert!(result.is_ok());
-        assert_eq!(solver.lower_bound(s2), 7);
-        assert_eq!(solver.upper_bound(s2), 10);
-        assert_eq!(solver.lower_bound(s1), 5);
-        assert_eq!(solver.upper_bound(s1), 6);
+        solver.assert_bounds(s1, 5, 6);
+        solver.assert_bounds(s2, 7, 10);
     }
 
     #[test]
     fn propagator_propagates_end_time() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(6, 6);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(6, 6, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTableOverIntervalPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    ..Default::default()
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
                 },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 1);
-        assert_eq!(solver.upper_bound(s2), 3);
-        assert_eq!(solver.lower_bound(s1), 6);
-        assert_eq!(solver.upper_bound(s1), 6);
-
-        let reason = solver.get_reason_int(predicate!(s2 <= 3));
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 6, 6);
+        state.assert_bounds(s2, 1, 3);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 <= 3),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([s2 <= 8] & [s1 >= 6] & [s1 <= 6]), reason);
     }
 
     #[test]
-    fn propagator_propagates_example_4_3_schutt_after_update() {
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
+    fn propagator_propagates_example_4_3_schutt_multiple_profiles() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
         let e = solver.new_variable(0, 4);
         let d = solver.new_variable(0, 2);
         let c = solver.new_variable(8, 9);
-        let b = solver.new_variable(2, 3);
+        let b2 = solver.new_variable(5, 5);
+        let b1 = solver.new_variable(3, 3);
         let a = solver.new_variable(0, 1);
+
         let constraint_tag = solver.new_constraint_tag();
 
         let propagator = solver
@@ -788,8 +794,13 @@ mod tests {
                         resource_usage: 1,
                     },
                     ArgTask {
-                        start_time: b,
-                        processing_time: 6,
+                        start_time: b1,
+                        processing_time: 2,
+                        resource_usage: 2,
+                    },
+                    ArgTask {
+                        start_time: b2,
+                        processing_time: 3,
                         resource_usage: 2,
                     },
                     ArgTask {
@@ -820,20 +831,13 @@ mod tests {
                 constraint_tag,
             ))
             .expect("No conflict");
-        assert_eq!(solver.lower_bound(a), 0);
-        assert_eq!(solver.upper_bound(a), 1);
-        assert_eq!(solver.lower_bound(b), 2);
-        assert_eq!(solver.upper_bound(b), 3);
-        assert_eq!(solver.lower_bound(c), 8);
-        assert_eq!(solver.upper_bound(c), 9);
-        assert_eq!(solver.lower_bound(d), 0);
-        assert_eq!(solver.upper_bound(d), 2);
-        assert_eq!(solver.lower_bound(e), 0);
-        assert_eq!(solver.upper_bound(e), 4);
-        assert_eq!(solver.lower_bound(f), 0);
-        assert_eq!(solver.upper_bound(f), 14);
+        solver.assert_bounds(a, 0, 1);
+        solver.assert_bounds(c, 8, 9);
+        solver.assert_bounds(d, 0, 2);
+        solver.assert_bounds(e, 0, 4);
+        solver.assert_bounds(f, 0, 14);
 
-        let notification_status = solver.increase_lower_bound_and_notify(propagator, 3, e, 3);
+        let notification_status = solver.increase_lower_bound_and_notify(propagator, 4, e, 3);
         assert!(match notification_status {
             EnqueueDecision::Enqueue => true,
             EnqueueDecision::Skip => false,
@@ -844,16 +848,61 @@ mod tests {
     }
 
     #[test]
-    fn propagator_propagates_example_4_3_schutt_multiple_profiles() {
+    fn propagator_propagates_from_profile_reason() {
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 >= 5),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
+        assert_eq!(conjunction!([s2 >= 1] & [s1 >= 1] & [s1 <= 1]), reason);
+    }
+
+    #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
+    fn propagator_propagates_example_4_3_schutt_after_update() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
         let e = solver.new_variable(0, 4);
         let d = solver.new_variable(0, 2);
         let c = solver.new_variable(8, 9);
-        let b2 = solver.new_variable(5, 5);
-        let b1 = solver.new_variable(3, 3);
+        let b = solver.new_variable(2, 3);
         let a = solver.new_variable(0, 1);
-
         let constraint_tag = solver.new_constraint_tag();
 
         let propagator = solver
@@ -865,13 +914,8 @@ mod tests {
                         resource_usage: 1,
                     },
                     ArgTask {
-                        start_time: b1,
-                        processing_time: 2,
-                        resource_usage: 2,
-                    },
-                    ArgTask {
-                        start_time: b2,
-                        processing_time: 3,
+                        start_time: b,
+                        processing_time: 6,
                         resource_usage: 2,
                     },
                     ArgTask {
@@ -902,18 +946,14 @@ mod tests {
                 constraint_tag,
             ))
             .expect("No conflict");
-        assert_eq!(solver.lower_bound(a), 0);
-        assert_eq!(solver.upper_bound(a), 1);
-        assert_eq!(solver.lower_bound(c), 8);
-        assert_eq!(solver.upper_bound(c), 9);
-        assert_eq!(solver.lower_bound(d), 0);
-        assert_eq!(solver.upper_bound(d), 2);
-        assert_eq!(solver.lower_bound(e), 0);
-        assert_eq!(solver.upper_bound(e), 4);
-        assert_eq!(solver.lower_bound(f), 0);
-        assert_eq!(solver.upper_bound(f), 14);
+        solver.assert_bounds(a, 0, 1);
+        solver.assert_bounds(b, 2, 3);
+        solver.assert_bounds(c, 8, 9);
+        solver.assert_bounds(d, 0, 2);
+        solver.assert_bounds(e, 0, 4);
+        solver.assert_bounds(f, 0, 14);
 
-        let notification_status = solver.increase_lower_bound_and_notify(propagator, 4, e, 3);
+        let notification_status = solver.increase_lower_bound_and_notify(propagator, 3, e, 3);
         assert!(match notification_status {
             EnqueueDecision::Enqueue => true,
             EnqueueDecision::Skip => false,
@@ -923,134 +963,99 @@ mod tests {
         assert_eq!(solver.lower_bound(f), 10);
     }
 
-    #[test]
-    fn propagator_propagates_from_profile_reason() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(TimeTableOverIntervalPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    ..Default::default()
-                },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
-
-        let reason = solver.get_reason_int(predicate!(s2 >= 5));
-        assert_eq!(conjunction!([s2 >= 1] & [s1 >= 1] & [s1 <= 1]), reason);
-    }
-
     #[test]
     fn propagator_propagates_generic_bounds() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(3, 3);
-        let s2 = solver.new_variable(5, 5);
-        let s3 = solver.new_variable(1, 15);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(3, 3, None);
+        let s2 = state.new_interval_variable(5, 5, None);
+        let s3 = state.new_interval_variable(1, 15, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTableOverIntervalPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 2,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 2,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s3,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    ..Default::default()
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 2,
+                    resource_usage: 1,
                 },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s3), 7);
-        assert_eq!(solver.upper_bound(s3), 15);
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 5);
-        assert_eq!(solver.lower_bound(s1), 3);
-        assert_eq!(solver.upper_bound(s1), 3);
-
-        let reason = solver.get_reason_int(predicate!(s3 >= 7));
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 2,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: s3,
+                    processing_time: 4,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 3, 3);
+        state.assert_bounds(s2, 5, 5);
+        state.assert_bounds(s3, 7, 15);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s3 >= 7),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([s2 <= 5] & [s2 >= 5] & [s3 >= 5]), reason);
     }
 
     #[test]
     fn propagator_propagates_with_holes() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(4, 4);
-        let s2 = solver.new_variable(0, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(4, 4, None);
+        let s2 = state.new_interval_variable(0, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTableOverIntervalPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    allow_holes_in_domain: true,
-                    ..Default::default()
+        let _ = state.add_propagator(TimeTableOverIntervalPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
                 },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 4);
-        assert_eq!(solver.upper_bound(s1), 4);
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                allow_holes_in_domain: true,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 4, 4);
+        state.assert_bounds(s2, 0, 8);
 
         for removed in 2..8 {
-            assert!(!solver.contains(s2, removed));
-            let reason = solver.get_reason_int(predicate!(s2 != removed));
+            assert!(!state.contains(s2, removed));
+            let mut reason_buffer: Vec<Predicate> = vec![];
+            let _ = state.get_propagation_reason(
+                predicate!(s2 != removed),
+                &mut reason_buffer,
+                CurrentNogood::empty(),
+            );
+            let reason: PropositionalConjunction = reason_buffer.into();
             assert_eq!(conjunction!([s1 <= 4] & [s1 >= 4]), reason);
         }
     }
diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs
index 2b26a43b2..28ee01df4 100644
--- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs
+++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs
@@ -296,16 +296,23 @@ pub(crate) fn propagate_from_scratch_time_table_point<Var: IntegerVariable + 'st
     )
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
+    #[allow(
+        deprecated,
+        reason = "TestSolver is deprecated but still used in these tests"
+    )]
     use pumpkin_core::TestSolver;
     use pumpkin_core::conjunction;
     use pumpkin_core::predicate;
     use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
     use pumpkin_core::propagation::EnqueueDecision;
     use pumpkin_core::state::Conflict;
+    use pumpkin_core::state::State;
 
+    use crate::StateExt;
     use crate::cumulative::ArgTask;
     use crate::cumulative::options::CumulativePropagatorOptions;
     use crate::cumulative::time_table::CumulativeExplanationType;
@@ -313,46 +320,43 @@ mod tests {
 
     #[test]
     fn propagator_propagates_from_profile() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTablePerPointPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions::default(),
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions::default(),
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
     }
 
     #[test]
     fn propagator_detects_conflict() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 1);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 1, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let result = solver.new_propagator(TimeTablePerPointPropagator::new(
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
             &[
                 ArgTask {
                     start_time: s1,
@@ -374,119 +378,114 @@ mod tests {
             },
             constraint_tag,
         ));
-        assert!(match result {
-            Err(e) => match e {
-                Conflict::EmptyDomain(_) => false,
-                Conflict::Propagator(x) => {
-                    let expected = [
-                        predicate!(s1 <= 1),
-                        predicate!(s1 >= 1),
-                        predicate!(s2 <= 1),
-                        predicate!(s2 >= 1),
-                    ];
-                    expected.iter().all(|y| {
-                        x.conjunction
-                            .iter()
-                            .collect::<Vec<&Predicate>>()
-                            .contains(&y)
-                    }) && x.conjunction.iter().all(|y| expected.contains(y))
-                }
-            },
-
-            Ok(_) => false,
-        });
+        let Conflict::Propagator(x) = state.propagate_to_fixed_point().unwrap_err() else {
+            panic!("an explicit conflict should have been detected");
+        };
+        let expected = [
+            predicate!(s1 <= 1),
+            predicate!(s1 >= 1),
+            predicate!(s2 <= 1),
+            predicate!(s2 >= 1),
+        ];
+        assert!(expected.iter().all(|y| {
+            x.conjunction
+                .iter()
+                .collect::<Vec<&Predicate>>()
+                .contains(&y)
+        }));
+        assert!(x.conjunction.iter().all(|y| expected.contains(y)));
     }
 
     #[test]
     fn propagator_propagates_nothing() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(0, 6);
-        let s2 = solver.new_variable(0, 6);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(0, 6, None);
+        let s2 = state.new_interval_variable(0, 6, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTablePerPointPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions::default(),
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 6);
-        assert_eq!(solver.lower_bound(s1), 0);
-        assert_eq!(solver.upper_bound(s1), 6);
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions::default(),
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 0, 6);
+        state.assert_bounds(s2, 0, 6);
     }
 
     #[test]
     fn propagator_propagates_example_4_3_schutt() {
-        let mut solver = TestSolver::default();
-        let f = solver.new_variable(0, 14);
-        let e = solver.new_variable(2, 4);
-        let d = solver.new_variable(0, 2);
-        let c = solver.new_variable(8, 9);
-        let b = solver.new_variable(2, 3);
-        let a = solver.new_variable(0, 1);
-        let constraint_tag = solver.new_constraint_tag();
-
-        let _ = solver
-            .new_propagator(TimeTablePerPointPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: a,
-                        processing_time: 2,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: b,
-                        processing_time: 6,
-                        resource_usage: 2,
-                    },
-                    ArgTask {
-                        start_time: c,
-                        processing_time: 2,
-                        resource_usage: 4,
-                    },
-                    ArgTask {
-                        start_time: d,
-                        processing_time: 2,
-                        resource_usage: 2,
-                    },
-                    ArgTask {
-                        start_time: e,
-                        processing_time: 5,
-                        resource_usage: 2,
-                    },
-                    ArgTask {
-                        start_time: f,
-                        processing_time: 6,
-                        resource_usage: 2,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                5,
-                CumulativePropagatorOptions::default(),
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(f), 10);
+        let mut state = State::default();
+        let f = state.new_interval_variable(0, 14, None);
+        let e = state.new_interval_variable(2, 4, None);
+        let d = state.new_interval_variable(0, 2, None);
+        let c = state.new_interval_variable(8, 9, None);
+        let b = state.new_interval_variable(2, 3, None);
+        let a = state.new_interval_variable(0, 1, None);
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
+            &[
+                ArgTask {
+                    start_time: a,
+                    processing_time: 2,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: b,
+                    processing_time: 6,
+                    resource_usage: 2,
+                },
+                ArgTask {
+                    start_time: c,
+                    processing_time: 2,
+                    resource_usage: 4,
+                },
+                ArgTask {
+                    start_time: d,
+                    processing_time: 2,
+                    resource_usage: 2,
+                },
+                ArgTask {
+                    start_time: e,
+                    processing_time: 5,
+                    resource_usage: 2,
+                },
+                ArgTask {
+                    start_time: f,
+                    processing_time: 6,
+                    resource_usage: 2,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            5,
+            CumulativePropagatorOptions::default(),
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        assert_eq!(state.lower_bound(f), 10);
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_after_assignment() {
         let mut solver = TestSolver::default();
         let s1 = solver.new_variable(0, 6);
@@ -534,47 +533,52 @@ mod tests {
 
     #[test]
     fn propagator_propagates_end_time() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(6, 6);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(6, 6, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let propagator = solver
-            .new_propagator(TimeTablePerPointPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    ..Default::default()
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
                 },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        let result = solver.propagate_until_fixed_point(propagator);
-        assert!(result.is_ok());
-        assert_eq!(solver.lower_bound(s2), 1);
-        assert_eq!(solver.upper_bound(s2), 3);
-        assert_eq!(solver.lower_bound(s1), 6);
-        assert_eq!(solver.upper_bound(s1), 6);
-
-        let reason = solver.get_reason_int(predicate!(s2 <= 3));
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 6, 6);
+        state.assert_bounds(s2, 1, 3);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 <= 3),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(conjunction!([s2 <= 5] & [s1 >= 6] & [s1 <= 6]), reason);
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_example_4_3_schutt_after_update() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
@@ -650,6 +654,10 @@ mod tests {
     }
 
     #[test]
+    #[allow(
+        deprecated,
+        reason = "Uses TestSolver for incremental notification assertions"
+    )]
     fn propagator_propagates_example_4_3_schutt_multiple_profiles() {
         let mut solver = TestSolver::default();
         let f = solver.new_variable(0, 14);
@@ -730,41 +738,44 @@ mod tests {
 
     #[test]
     fn propagator_propagates_from_profile_reason() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(1, 1);
-        let s2 = solver.new_variable(1, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(1, 1, None);
+        let s2 = state.new_interval_variable(1, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTablePerPointPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    ..Default::default()
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
                 },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 1);
-        assert_eq!(solver.upper_bound(s1), 1);
-
-        let reason = solver.get_reason_int(predicate!(s2 >= 5));
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 1, 1);
+        state.assert_bounds(s2, 5, 8);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s2 >= 5),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
             conjunction!([s2 >= 4] & [s1 >= 1] & [s1 <= 1]), /* Note that this not
                                                               * the most general
@@ -780,49 +791,51 @@ mod tests {
 
     #[test]
     fn propagator_propagates_generic_bounds() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(3, 3);
-        let s2 = solver.new_variable(5, 5);
-        let s3 = solver.new_variable(1, 15);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(3, 3, None);
+        let s2 = state.new_interval_variable(5, 5, None);
+        let s3 = state.new_interval_variable(1, 15, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTablePerPointPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 2,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 2,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s3,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    ..Default::default()
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 2,
+                    resource_usage: 1,
                 },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s3), 7);
-        assert_eq!(solver.upper_bound(s3), 15);
-        assert_eq!(solver.lower_bound(s2), 5);
-        assert_eq!(solver.upper_bound(s2), 5);
-        assert_eq!(solver.lower_bound(s1), 3);
-        assert_eq!(solver.upper_bound(s1), 3);
-
-        let reason = solver.get_reason_int(predicate!(s3 >= 7));
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 2,
+                    resource_usage: 1,
+                },
+                ArgTask {
+                    start_time: s3,
+                    processing_time: 4,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 3, 3);
+        state.assert_bounds(s2, 5, 5);
+        state.assert_bounds(s3, 7, 15);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate!(s3 >= 7),
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
             conjunction!([s2 <= 5] & [s2 >= 5] & [s3 >= 6]), /* Note that s3 would
                                                               * have been able to
@@ -835,44 +848,47 @@ mod tests {
 
     #[test]
     fn propagator_propagates_with_holes() {
-        let mut solver = TestSolver::default();
-        let s1 = solver.new_variable(4, 4);
-        let s2 = solver.new_variable(0, 8);
-        let constraint_tag = solver.new_constraint_tag();
+        let mut state = State::default();
+        let s1 = state.new_interval_variable(4, 4, None);
+        let s2 = state.new_interval_variable(0, 8, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(TimeTablePerPointPropagator::new(
-                &[
-                    ArgTask {
-                        start_time: s1,
-                        processing_time: 4,
-                        resource_usage: 1,
-                    },
-                    ArgTask {
-                        start_time: s2,
-                        processing_time: 3,
-                        resource_usage: 1,
-                    },
-                ]
-                .into_iter()
-                .collect::<Vec<_>>(),
-                1,
-                CumulativePropagatorOptions {
-                    explanation_type: CumulativeExplanationType::Naive,
-                    allow_holes_in_domain: true,
-                    ..Default::default()
+        let _ = state.add_propagator(TimeTablePerPointPropagator::new(
+            &[
+                ArgTask {
+                    start_time: s1,
+                    processing_time: 4,
+                    resource_usage: 1,
                 },
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(s2), 0);
-        assert_eq!(solver.upper_bound(s2), 8);
-        assert_eq!(solver.lower_bound(s1), 4);
-        assert_eq!(solver.upper_bound(s1), 4);
+                ArgTask {
+                    start_time: s2,
+                    processing_time: 3,
+                    resource_usage: 1,
+                },
+            ]
+            .into_iter()
+            .collect::<Vec<_>>(),
+            1,
+            CumulativePropagatorOptions {
+                explanation_type: CumulativeExplanationType::Naive,
+                allow_holes_in_domain: true,
+                ..Default::default()
+            },
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        state.assert_bounds(s1, 4, 4);
+        state.assert_bounds(s2, 0, 8);
 
         for removed in 2..8 {
-            assert!(!solver.contains(s2, removed));
-            let reason = solver.get_reason_int(predicate!(s2 != removed));
+            assert!(!state.contains(s2, removed));
+            let mut reason_buffer: Vec<Predicate> = vec![];
+            let _ = state.get_propagation_reason(
+                predicate!(s2 != removed),
+                &mut reason_buffer,
+                CurrentNogood::empty(),
+            );
+            let reason: PropositionalConjunction = reason_buffer.into();
             assert_eq!(conjunction!([s1 <= 4] & [s1 >= 4]), reason);
         }
     }
diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs
index 8799b938c..57c8f6fd7 100644
--- a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs
@@ -417,46 +417,44 @@ fn create_propagation_explanation<'a, Var: IntegerVariable>(
     explanation.into()
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
+    use pumpkin_core::state::State;
 
     use crate::disjunctive::ArgDisjunctiveTask;
     use crate::disjunctive::DisjunctiveConstructor;
 
     #[test]
     fn propagator_propagates_lower_bound() {
-        let mut solver = TestSolver::default();
-        let c = solver.new_variable(4, 26);
-        let d = solver.new_variable(13, 13);
-        let e = solver.new_variable(5, 10);
-        let f = solver.new_variable(5, 10);
-
-        let constraint_tag = solver.new_constraint_tag();
-        let _ = solver
-            .new_propagator(DisjunctiveConstructor::new(
-                [
-                    ArgDisjunctiveTask {
-                        start_time: c,
-                        processing_time: 4,
-                    },
-                    ArgDisjunctiveTask {
-                        start_time: d,
-                        processing_time: 5,
-                    },
-                    ArgDisjunctiveTask {
-                        start_time: e,
-                        processing_time: 3,
-                    },
-                    ArgDisjunctiveTask {
-                        start_time: f,
-                        processing_time: 3,
-                    },
-                ],
-                constraint_tag,
-            ))
-            .expect("No conflict");
-        assert_eq!(solver.lower_bound(c), 18);
+        let mut state = State::default();
+        let c = state.new_interval_variable(4, 26, None);
+        let d = state.new_interval_variable(13, 13, None);
+        let e = state.new_interval_variable(5, 10, None);
+        let f = state.new_interval_variable(5, 10, None);
+
+        let constraint_tag = state.new_constraint_tag();
+        let _ = state.add_propagator(DisjunctiveConstructor::new(
+            [
+                ArgDisjunctiveTask {
+                    start_time: c,
+                    processing_time: 4,
+                },
+                ArgDisjunctiveTask {
+                    start_time: d,
+                    processing_time: 5,
+                },
+                ArgDisjunctiveTask {
+                    start_time: e,
+                    processing_time: 3,
+                },
+                ArgDisjunctiveTask {
+                    start_time: f,
+                    processing_time: 3,
+                },
+            ],
+            constraint_tag,
+        ));
+        state.propagate_to_fixed_point().expect("No conflict");
+        assert_eq!(state.lower_bound(c), 18);
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/theta_lambda_tree.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/theta_lambda_tree.rs
index e8c8e2834..2519a0f8c 100644
--- a/pumpkin-crates/propagators/src/propagators/disjunctive/theta_lambda_tree.rs
+++ b/pumpkin-crates/propagators/src/propagators/disjunctive/theta_lambda_tree.rs
@@ -374,11 +374,10 @@ impl<Var: IntegerVariable> ThetaLambdaTree<Var> {
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
-    use pumpkin_core::TestSolver;
     use pumpkin_core::propagation::LocalId;
+    use pumpkin_core::state::State;
 
     use crate::disjunctive::theta_lambda_tree::DisjunctiveTask;
     use crate::propagators::disjunctive::theta_lambda_tree::Node;
@@ -386,11 +385,11 @@ mod tests {
 
     #[test]
     fn tree_built_correctly() {
-        let mut solver = TestSolver::default();
-        let a = solver.new_variable(0, 0);
-        let b = solver.new_variable(25, 25);
-        let c = solver.new_variable(30, 30);
-        let d = solver.new_variable(32, 32);
+        let mut state = State::default();
+        let a = state.new_interval_variable(0, 0, None);
+        let b = state.new_interval_variable(25, 25, None);
+        let c = state.new_interval_variable(30, 30, None);
+        let d = state.new_interval_variable(32, 32, None);
         let tasks = [
             DisjunctiveTask {
                 start_time: a,
@@ -416,12 +415,12 @@ mod tests {
 
         let mut tree = ThetaLambdaTree::new(&tasks);
 
-        tree.update(solver.state.get_domains());
+        tree.update(state.get_domains());
         for task in tasks.iter() {
-            tree.add_to_theta(task, solver.state.get_domains());
+            tree.add_to_theta(task, state.get_domains());
         }
         tree.remove_from_theta(&tasks[2]);
-        tree.add_to_lambda(&tasks[2], solver.state.get_domains());
+        tree.add_to_lambda(&tasks[2], state.get_domains());
 
         assert_eq!(
             tree.nodes[6],
diff --git a/pumpkin-crates/propagators/src/propagators/element.rs b/pumpkin-crates/propagators/src/propagators/element.rs
index c401eb847..3f9b011d4 100644
--- a/pumpkin-crates/propagators/src/propagators/element.rs
+++ b/pumpkin-crates/propagators/src/propagators/element.rs
@@ -399,154 +399,200 @@ where
     }
 }
 
-#[allow(deprecated, reason = "Will be refactored")]
 #[cfg(test)]
 mod tests {
     use pumpkin_checking::TestAtomic;
     use pumpkin_checking::VariableState;
-    use pumpkin_core::TestSolver;
+    use pumpkin_core::predicate;
+    use pumpkin_core::predicates::Predicate;
+    use pumpkin_core::predicates::PropositionalConjunction;
+    use pumpkin_core::propagation::CurrentNogood;
+    use pumpkin_core::state::State;
 
     use super::*;
+    use crate::StateExt;
 
     #[test]
     fn elements_from_array_with_disjoint_domains_to_rhs_are_filtered_from_index() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let x_0 = solver.new_variable(4, 6);
-        let x_1 = solver.new_variable(2, 3);
-        let x_2 = solver.new_variable(7, 9);
-        let x_3 = solver.new_variable(14, 15);
+        let x_0 = state.new_interval_variable(4, 6, None);
+        let x_1 = state.new_interval_variable(2, 3, None);
+        let x_2 = state.new_interval_variable(7, 9, None);
+        let x_3 = state.new_interval_variable(14, 15, None);
 
-        let index = solver.new_variable(0, 3);
-        let rhs = solver.new_variable(6, 9);
-        let constraint_tag = solver.new_constraint_tag();
+        let index = state.new_interval_variable(0, 3, None);
+        let rhs = state.new_interval_variable(6, 9, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(ElementArgs {
-                array: vec![x_0, x_1, x_2, x_3].into(),
-                index,
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(ElementArgs {
+            array: vec![x_0, x_1, x_2, x_3].into(),
+            index,
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(index, 0, 2);
+        state.assert_bounds(index, 0, 2);
 
-        assert_eq!(
-            solver.get_reason_int(predicate![index != 3]),
-            conjunction!([x_3 >= 10] & [rhs <= 9])
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![index != 3],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
         );
-
-        assert_eq!(
-            solver.get_reason_int(predicate![index != 1]),
-            conjunction!([x_1 <= 5] & [rhs >= 6])
+        let reason: PropositionalConjunction = reason_buffer.into();
+        assert_eq!(conjunction!([x_3 >= 10] & [rhs <= 9]), reason);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![index != 1],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
         );
+        let reason: PropositionalConjunction = reason_buffer.into();
+        assert_eq!(conjunction!([x_1 <= 5] & [rhs >= 6]), reason);
     }
 
     #[test]
     fn bounds_of_rhs_are_min_and_max_of_lower_and_upper_in_array() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let x_0 = solver.new_variable(3, 10);
-        let x_1 = solver.new_variable(2, 3);
-        let x_2 = solver.new_variable(7, 9);
-        let x_3 = solver.new_variable(14, 15);
+        let x_0 = state.new_interval_variable(3, 10, None);
+        let x_1 = state.new_interval_variable(2, 3, None);
+        let x_2 = state.new_interval_variable(7, 9, None);
+        let x_3 = state.new_interval_variable(14, 15, None);
 
-        let index = solver.new_variable(0, 3);
-        let rhs = solver.new_variable(0, 20);
-        let constraint_tag = solver.new_constraint_tag();
+        let index = state.new_interval_variable(0, 3, None);
+        let rhs = state.new_interval_variable(0, 20, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let _ = solver
-            .new_propagator(ElementArgs {
-                array: vec![x_0, x_1, x_2, x_3].into(),
-                index,
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(ElementArgs {
+            array: vec![x_0, x_1, x_2, x_3].into(),
+            index,
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(rhs, 2, 15);
+        state.assert_bounds(rhs, 2, 15);
 
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![rhs >= 2],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
-            solver.get_reason_int(predicate![rhs >= 2]),
-            conjunction!([x_0 >= 2] & [x_1 >= 2] & [x_2 >= 2] & [x_3 >= 2])
+            conjunction!([x_0 >= 2] & [x_1 >= 2] & [x_2 >= 2] & [x_3 >= 2]),
+            reason
         );
 
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![rhs <= 15],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
-            solver.get_reason_int(predicate![rhs <= 15]),
-            conjunction!([x_0 <= 15] & [x_1 <= 15] & [x_2 <= 15] & [x_3 <= 15])
+            conjunction!([x_0 <= 15] & [x_1 <= 15] & [x_2 <= 15] & [x_3 <= 15]),
+            reason
         );
     }
 
     #[test]
     fn fixed_index_propagates_bounds_on_element() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let x_0 = solver.new_variable(3, 10);
-        let x_1 = solver.new_variable(0, 15);
-        let x_2 = solver.new_variable(7, 9);
-        let x_3 = solver.new_variable(14, 15);
-        let constraint_tag = solver.new_constraint_tag();
+        let x_0 = state.new_interval_variable(3, 10, None);
+        let x_1 = state.new_interval_variable(0, 15, None);
+        let x_2 = state.new_interval_variable(7, 9, None);
+        let x_3 = state.new_interval_variable(14, 15, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let index = solver.new_variable(1, 1);
-        let rhs = solver.new_variable(6, 9);
+        let index = state.new_interval_variable(1, 1, None);
+        let rhs = state.new_interval_variable(6, 9, None);
 
-        let _ = solver
-            .new_propagator(ElementArgs {
-                array: vec![x_0, x_1, x_2, x_3].into(),
-                index,
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(ElementArgs {
+            array: vec![x_0, x_1, x_2, x_3].into(),
+            index,
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(x_1, 6, 9);
+        state.assert_bounds(x_1, 6, 9);
 
-        assert_eq!(
-            solver.get_reason_int(predicate![x_1 >= 6]),
-            conjunction!([index == 1] & [rhs >= 6])
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![x_1 >= 6],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
         );
-
-        assert_eq!(
-            solver.get_reason_int(predicate![x_1 <= 9]),
-            conjunction!([index == 1] & [rhs <= 9])
+        let reason: PropositionalConjunction = reason_buffer.into();
+        assert_eq!(conjunction!([index == 1] & [rhs >= 6]), reason);
+
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![x_1 <= 9],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
         );
+        let reason: PropositionalConjunction = reason_buffer.into();
+        assert_eq!(conjunction!([index == 1] & [rhs <= 9]), reason);
     }
 
     #[test]
     fn index_hole_propagates_bounds_on_rhs() {
-        let mut solver = TestSolver::default();
+        let mut state = State::default();
 
-        let x_0 = solver.new_variable(3, 10);
-        let x_1 = solver.new_variable(0, 15);
-        let x_2 = solver.new_variable(7, 9);
-        let x_3 = solver.new_variable(14, 15);
-        let constraint_tag = solver.new_constraint_tag();
+        let x_0 = state.new_interval_variable(3, 10, None);
+        let x_1 = state.new_interval_variable(0, 15, None);
+        let x_2 = state.new_interval_variable(7, 9, None);
+        let x_3 = state.new_interval_variable(14, 15, None);
+        let constraint_tag = state.new_constraint_tag();
 
-        let index = solver.new_variable(0, 3);
-        solver.remove(index, 1).expect("Value can be removed");
+        let index = state.new_interval_variable(0, 3, None);
+        let _ = state
+            .post(predicate![index != 1])
+            .expect("Value can be removed");
 
-        let rhs = solver.new_variable(-10, 30);
+        let rhs = state.new_interval_variable(-10, 30, None);
 
-        let _ = solver
-            .new_propagator(ElementArgs {
-                array: vec![x_0, x_1, x_2, x_3].into(),
-                index,
-                rhs,
-                constraint_tag,
-            })
-            .expect("no empty domains");
+        let _ = state.add_propagator(ElementArgs {
+            array: vec![x_0, x_1, x_2, x_3].into(),
+            index,
+            rhs,
+            constraint_tag,
+        });
+        state.propagate_to_fixed_point().expect("no empty domains");
 
-        solver.assert_bounds(rhs, 3, 15);
+        state.assert_bounds(rhs, 3, 15);
 
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![rhs >= 3],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
-            solver.get_reason_int(predicate![rhs >= 3]),
-            conjunction!([x_0 >= 3] & [x_2 >= 3] & [x_3 >= 3] & [index != 1])
+            conjunction!([x_0 >= 3] & [x_2 >= 3] & [x_3 >= 3] & [index != 1]),
+            reason
         );
 
+        let mut reason_buffer: Vec<Predicate> = vec![];
+        let _ = state.get_propagation_reason(
+            predicate![rhs <= 15],
+            &mut reason_buffer,
+            CurrentNogood::empty(),
+        );
+        let reason: PropositionalConjunction = reason_buffer.into();
         assert_eq!(
-            solver.get_reason_int(predicate![rhs <= 15]),
-            conjunction!([x_0 <= 15] & [x_2 <= 15] & [x_3 <= 15] & [index != 1])
+            conjunction!([x_0 <= 15] & [x_2 <= 15] & [x_3 <= 15] & [index != 1]),
+            reason
         );
     }