diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs
index 0775a84f87..28077edacb 100644
--- a/crates/pindakaas-derive/src/lib.rs
+++ b/crates/pindakaas-derive/src/lib.rs
@@ -147,6 +147,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 			None => quote! { self.prop },
 		};
 		quote! {
+			#[cfg(feature = "ipasir-up")]
 			pub(crate) struct #prop_ident {
 				/// Rust Propagator Storage
 				prop: Box<crate::solver::libloading::IpasirPropStore>,
@@ -154,12 +155,14 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 				wrapper: *mut std::ffi::c_void,
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl Drop for #prop_ident {
 				fn drop(&mut self) {
 					unsafe { #krate::ipasir_prop_release(self.wrapper) };
 				}
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl #prop_ident {
 				pub(crate) fn new(prop: Box<dyn crate::solver::Propagator>, slv: *mut dyn crate::solver::SolvingActions) -> Self {
 					// Construct wrapping structures
@@ -182,6 +185,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 				}
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl crate::solver::PropagatingSolver for #ident {
 				fn set_external_propagator(
 					&mut self,
@@ -220,6 +224,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 				}
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl crate::solver::SolvingActions for #ident {
 				fn new_var(&mut self) -> crate::Var {
 					<#ident as crate::ClauseDatabase>::new_var(self)
@@ -266,7 +271,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 
 		impl #ident {
 			/// Return the next [`size`] variables that can be stored as an inclusive range.
-			pub fn new_var_range(&mut self, size: usize) -> std::ops::RangeInclusive<crate::Var> {
+			pub fn new_var_range(&mut self, size: usize) -> crate::helpers::VarRange {
 				self.vars.new_var_range(size).expect("variable pool exhaused")
 			}
 		}
diff --git a/crates/pindakaas/Cargo.toml b/crates/pindakaas/Cargo.toml
index 07c42760ba..33cd9214cd 100644
--- a/crates/pindakaas/Cargo.toml
+++ b/crates/pindakaas/Cargo.toml
@@ -14,7 +14,6 @@ edition = "2021"
 cached = "0.46"
 iset = "0.2"
 itertools = "0.12.0"
-pindakaas-derive = { path = "../pindakaas-derive" }
 rustc-hash = "1.1"
 # Dynamically load solver libraries (through IPASIR interfaces)
 libloading = "0.8"
@@ -24,6 +23,7 @@ tracing = { version = "0.1", optional = true }
 
 # Optional Solver Interfaces
 pindakaas-cadical = { path = "../pindakaas-cadical", optional = true }
+pindakaas-derive = { path = "../pindakaas-derive", optional = true }
 pindakaas-intel-sat = { path = "../pindakaas-intel-sat", optional = true }
 pindakaas-kissat = { path = "../pindakaas-kissat", optional = true }
 splr = { version = "0.17", optional = true }
@@ -33,8 +33,9 @@ splr = { version = "0.17", features = ["incremental_solver"] }
 traced_test = { path = "../traced_test" }
 
 [features]
-cadical = ["pindakaas-cadical"]
-intel-sat = ["pindakaas-intel-sat"]
-kissat = ["pindakaas-kissat"]
+cadical = ["pindakaas-cadical", "pindakaas-derive"]
+intel-sat = ["pindakaas-intel-sat", "pindakaas-derive"]
+kissat = ["pindakaas-kissat", "pindakaas-derive"]
 trace = ["tracing"]
 default = ["cadical"]
+ipasir-up = ["cadical"]
diff --git a/crates/pindakaas/src/helpers.rs b/crates/pindakaas/src/helpers.rs
index 1f75af88c7..f2dbef6c63 100644
--- a/crates/pindakaas/src/helpers.rs
+++ b/crates/pindakaas/src/helpers.rs
@@ -1,10 +1,15 @@
-use std::collections::HashSet;
+use std::{
+	cmp::max,
+	collections::HashSet,
+	iter::FusedIterator,
+	ops::{Bound, RangeBounds, RangeInclusive},
+};
 
 use itertools::Itertools;
 
 use crate::{
 	int::IntVar, linear::PosCoeff, trace::emit_clause, CheckError, Checker, ClauseDatabase, Coeff,
-	Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation,
+	Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation, Var,
 };
 
 #[allow(unused_macros)]
@@ -196,6 +201,74 @@ impl<'a> Checker for XorConstraint<'a> {
 	}
 }
 
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct VarRange {
+	start: Var,
+	end: Var,
+}
+
+impl VarRange {
+	pub fn new(start: Var, end: Var) -> Self {
+		Self { start, end }
+	}
+}
+
+impl Iterator for VarRange {
+	type Item = Var;
+
+	fn next(&mut self) -> Option<Self::Item> {
+		if self.start <= self.end {
+			let item = self.start;
+			self.start = self.start.next_var().unwrap();
+			Some(item)
+		} else {
+			None
+		}
+	}
+	fn size_hint(&self) -> (usize, Option<usize>) {
+		let size = max(self.end.0.get() - self.start.0.get(), 0) as usize;
+		(size, Some(size))
+	}
+	fn count(self) -> usize {
+		let (lower, upper) = self.size_hint();
+		debug_assert_eq!(upper, Some(lower));
+		lower
+	}
+}
+impl FusedIterator for VarRange {}
+impl ExactSizeIterator for VarRange {
+	fn len(&self) -> usize {
+		let (lower, upper) = self.size_hint();
+		debug_assert_eq!(upper, Some(lower));
+		lower
+	}
+}
+impl DoubleEndedIterator for VarRange {
+	fn next_back(&mut self) -> Option<Self::Item> {
+		if self.start <= self.end {
+			let item = self.end;
+			self.end = self.end.prev_var().unwrap();
+			Some(item)
+		} else {
+			None
+		}
+	}
+}
+impl RangeBounds<Var> for VarRange {
+	fn start_bound(&self) -> Bound<&Var> {
+		Bound::Included(&self.start)
+	}
+
+	fn end_bound(&self) -> Bound<&Var> {
+		Bound::Included(&self.end)
+	}
+}
+impl From<RangeInclusive<Var>> for VarRange {
+	fn from(value: RangeInclusive<Var>) -> Self {
+		VarRange::new(*value.start(), *value.end())
+	}
+}
+
 #[cfg(test)]
 pub mod tests {
 	use std::{
diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs
index 62bc7c888d..e63de33f40 100755
--- a/crates/pindakaas/src/lib.rs
+++ b/crates/pindakaas/src/lib.rs
@@ -48,11 +48,24 @@ pub struct Var(pub(crate) NonZeroI32);
 
 impl Var {
 	fn next_var(&self) -> Option<Var> {
-		self.checked_add(NonZeroI32::new(1).unwrap())
+		const ONE: NonZeroI32 = unsafe { NonZeroI32::new_unchecked(1) };
+		self.checked_add(ONE)
+	}
+
+	fn prev_var(&self) -> Option<Var> {
+		let prev = self.0.get() - 1;
+		if prev >= 0 {
+			Some(Var(NonZeroI32::new(prev).unwrap()))
+		} else {
+			None
+		}
 	}
 
 	fn checked_add(&self, b: NonZeroI32) -> Option<Var> {
-		self.0.get().checked_add(b.get()).map(|v| Var(NonZeroI32::new(v).unwrap()))
+		self.0
+			.get()
+			.checked_add(b.get())
+			.map(|v| Var(NonZeroI32::new(v).unwrap()))
 	}
 }
 
diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs
index 60c94fd179..4fcb32b3c9 100644
--- a/crates/pindakaas/src/solver.rs
+++ b/crates/pindakaas/src/solver.rs
@@ -1,6 +1,6 @@
-use std::{num::NonZeroI32, ops::RangeInclusive};
+use std::num::NonZeroI32;
 
-use crate::{ClauseDatabase, Lit, Valuation, Var};
+use crate::{helpers::VarRange, ClauseDatabase, Lit, Valuation, Var};
 
 pub mod libloading;
 
@@ -74,6 +74,7 @@ pub trait TermCallback: Solver {
 	fn set_terminate_callback<F: FnMut() -> SlvTermSignal>(&mut self, cb: Option<F>);
 }
 
+#[cfg(feature = "ipasir-up")]
 pub trait PropagatingSolver: Solver {
 	/// Set Propagator implementation which allows to learn, propagate and
 	/// backtrack based on external constraints.
@@ -96,6 +97,7 @@ pub trait PropagatingSolver: Solver {
 	fn reset_observed_vars(&mut self);
 }
 
+#[cfg(feature = "ipasir-up")]
 pub trait Propagator {
 	/// This method is called checked only when the propagator is connected. When
 	/// a Propagator is marked as lazy, it is only asked to check complete
@@ -108,14 +110,20 @@ pub trait Propagator {
 	/// variables. The notification is not necessarily eager. It usually happens
 	/// before the call of propagator callbacks and when a driving clause is
 	/// leading to an assignment.
-	fn notify_assignment(&mut self, _lit: Lit, _is_fixed: bool) {}
+	fn notify_assignment(&mut self, lit: Lit, is_fixed: bool) {
+		let _ = lit;
+		let _ = is_fixed;
+	}
 	fn notify_new_decision_level(&mut self) {}
-	fn notify_backtrack(&mut self, _new_level: usize) {}
+	fn notify_backtrack(&mut self, new_level: usize) {
+		let _ = new_level;
+	}
 
 	/// Method called to check the found complete solution (after solution
 	/// reconstruction). If it returns false, the propagator must provide an
 	/// external clause during the next callback.
-	fn check_model(&mut self, _value: &dyn Valuation) -> bool {
+	fn check_model(&mut self, value: &dyn Valuation) -> bool {
+		let _ = value;
 		true
 	}
 
@@ -129,14 +137,16 @@ pub trait Propagator {
 	/// current assignment. It returns queue of literals to be propagated in order,
 	/// if an empty queue is returned it indicates that there is no propagation
 	/// under the current assignment.
-	fn propagate(&mut self, _slv: &mut dyn SolvingActions) -> Vec<Lit> {
+	fn propagate(&mut self, slv: &mut dyn SolvingActions) -> Vec<Lit> {
+		let _ = slv;
 		Vec::new()
 	}
 
 	/// Ask the external propagator for the reason clause of a previous external
 	/// propagation step (done by [`Propagator::propagate`]). The clause must
 	/// contain the propagated literal.
-	fn add_reason_clause(&mut self, _propagated_lit: Lit) -> Vec<Lit> {
+	fn add_reason_clause(&mut self, propagated_lit: Lit) -> Vec<Lit> {
+		let _ = propagated_lit;
 		Vec::new()
 	}
 
@@ -146,6 +156,7 @@ pub trait Propagator {
 	}
 }
 
+#[cfg(feature = "ipasir-up")]
 pub trait SolvingActions {
 	fn new_var(&mut self) -> Var;
 	fn add_observed_var(&mut self, var: Var);
@@ -174,18 +185,23 @@ impl VarFactory {
 	}
 
 	/// Return the next [`size`] variables that can be stored as an inclusive range.
-	pub fn new_var_range(&mut self, size: usize) -> Option<RangeInclusive<Var>> {
+	pub fn new_var_range(&mut self, size: usize) -> Option<VarRange> {
 		let Some(start) = self.next_var else {
 			return None;
 		};
 		match size {
-			0 => Some(Var(NonZeroI32::new(2).unwrap())..=Var(NonZeroI32::new(1).unwrap())),
+			0 => Some(VarRange::new(
+				Var(NonZeroI32::new(2).unwrap()),
+				Var(NonZeroI32::new(1).unwrap()),
+			)),
 			_ if size > NonZeroI32::MAX.get() as usize => None,
 			_ => {
-				let size = NonZeroI32::new(size as i32).unwrap();
+				// Size is reduced by 1 since it includes self.next_var
+				let size = NonZeroI32::new((size - 1) as i32).unwrap();
 				if let Some(end) = start.checked_add(size) {
-					self.next_var = end.checked_add(NonZeroI32::new(1).unwrap());
-					Some(start..=end)
+					// Set self.next_var to one after end
+					self.next_var = end.next_var();
+					Some(VarRange::new(start, end))
 				} else {
 					None
 				}
diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs
index df327037e9..1168545c28 100644
--- a/crates/pindakaas/src/solver/cadical.rs
+++ b/crates/pindakaas/src/solver/cadical.rs
@@ -8,6 +8,7 @@ use crate::Lit;
 pub struct Cadical {
 	ptr: *mut std::ffi::c_void,
 	vars: VarFactory,
+	#[cfg(feature = "ipasir-up")]
 	prop: Option<Box<CadicalProp>>,
 }
 
@@ -16,6 +17,7 @@ impl Default for Cadical {
 		Self {
 			ptr: unsafe { pindakaas_cadical::ipasir_init() },
 			vars: VarFactory::default(),
+			#[cfg(feature = "ipasir-up")]
 			prop: None,
 		}
 	}
@@ -39,7 +41,7 @@ mod tests {
 	use super::*;
 	use crate::{
 		linear::LimitComp,
-		solver::{PropagatingSolver, Propagator, SolveResult, Solver},
+		solver::{SolveResult, Solver},
 		CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder,
 	};
 
@@ -67,4 +69,89 @@ mod tests {
 		});
 		assert_eq!(res, SolveResult::Sat);
 	}
+
+	#[cfg(feature = "ipasir-up")]
+	#[test]
+	fn test_ipasir_up() {
+		use itertools::Itertools;
+
+		use crate::{
+			helpers::tests::lits,
+			solver::{PropagatingSolver, Propagator, VarRange},
+		};
+
+		let mut slv = Cadical::default();
+
+		let vars = slv.new_var_range(5);
+
+		struct Dist2 {
+			vars: VarRange,
+			tmp: Vec<Vec<Lit>>,
+		}
+		impl Propagator for Dist2 {
+			fn is_lazy(&self) -> bool {
+				true
+			}
+			fn check_model(&mut self, value: &dyn crate::Valuation) -> bool {
+				let mut vars = self.vars.clone();
+				while let Some(v) = vars.next() {
+					if value(v.into()).unwrap_or(true) {
+						let next_2 = vars.clone().take(2);
+						for o in next_2 {
+							if value(o.into()).unwrap_or(true) {
+								self.tmp.push(vec![!v, !o]);
+							}
+						}
+					}
+				}
+				self.tmp.is_empty()
+			}
+			fn add_external_clause(&mut self) -> Option<Vec<Lit>> {
+				self.tmp.pop()
+			}
+		}
+
+		let p = Box::new(Dist2 {
+			vars: vars.clone(),
+			tmp: Vec::new(),
+		});
+		slv.set_external_propagator(Some(p));
+		slv.add_clause(vars.clone().map_into()).unwrap();
+		for v in vars.clone() {
+			slv.add_observed_var(v)
+		}
+
+		let mut solns = Vec::new();
+		while slv.solve(|value| {
+			let sol: Vec<Lit> = vars
+				.clone()
+				.map(|v| {
+					if value(v.into()).unwrap() {
+						v.into()
+					} else {
+						!v
+					}
+				})
+				.collect_vec();
+			solns.push(sol);
+		}) == SolveResult::Sat
+		{
+			slv.add_clause(solns.last().unwrap().iter().map(|l| !l))
+				.unwrap()
+		}
+		solns.sort();
+		assert_eq!(
+			solns,
+			vec![
+				lits![1, -2, -3, 4, -5],
+				lits![1, -2, -3, -4, 5],
+				lits![1, -2, -3, -4, -5],
+				lits![-1, 2, -3, -4, 5],
+				lits![-1, 2, -3, -4, -5],
+				lits![-1, -2, 3, -4, -5],
+				lits![-1, -2, -3, 4, -5],
+				lits![-1, -2, -3, -4, 5],
+			]
+		);
+	}
 }
diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs
index c5ffdc8ef4..12d1f870d0 100644
--- a/crates/pindakaas/src/solver/libloading.rs
+++ b/crates/pindakaas/src/solver/libloading.rs
@@ -1,5 +1,6 @@
+#[cfg(feature = "ipasir-up")]
+use std::collections::VecDeque;
 use std::{
-	collections::VecDeque,
 	ffi::{c_char, c_int, c_void, CStr},
 	num::NonZeroI32,
 	ptr,
@@ -8,9 +9,11 @@ use std::{
 use libloading::{Library, Symbol};
 
 use super::{
-	FailFn, LearnCallback, Propagator, SlvTermSignal, SolveAssuming, SolveResult, Solver,
-	SolvingActions, TermCallback, VarFactory,
+	FailFn, LearnCallback, SlvTermSignal, SolveAssuming, SolveResult, Solver, TermCallback,
+	VarFactory,
 };
+#[cfg(feature = "ipasir-up")]
+use super::{Propagator, SolvingActions};
 use crate::{ClauseDatabase, Lit, Result, Valuation, Var};
 
 pub struct IpasirLibrary {
@@ -295,10 +298,14 @@ impl Iterator for ExplIter {
 	}
 }
 
+#[cfg(feature = "ipasir-up")]
 #[derive(Debug, Clone, Copy)]
 pub(crate) struct NoProp;
+
+#[cfg(feature = "ipasir-up")]
 impl Propagator for NoProp {}
 
+#[cfg(feature = "ipasir-up")]
 pub(crate) struct IpasirPropStore {
 	/// Rust Propagator
 	pub(crate) prop: Box<dyn Propagator>,
@@ -313,6 +320,7 @@ pub(crate) struct IpasirPropStore {
 	pub(crate) cqueue: Option<VecDeque<crate::Lit>>,
 }
 
+#[cfg(feature = "ipasir-up")]
 impl IpasirPropStore {
 	pub(crate) fn new(prop: Box<dyn Propagator>, slv: *mut dyn SolvingActions) -> Self {
 		Self {
@@ -328,6 +336,7 @@ impl IpasirPropStore {
 
 // --- Callback functions for C propagator interface ---
 
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb(
 	state: *mut c_void,
 	lit: i32,
@@ -337,10 +346,12 @@ pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb(
 	let lit = crate::Lit(std::num::NonZeroI32::new(lit).unwrap());
 	prop.prop.notify_assignment(lit, is_fixed)
 }
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) {
 	let prop = &mut *(state as *mut IpasirPropStore);
 	prop.prop.notify_new_decision_level()
 }
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, level: usize) {
 	let prop = &mut *(state as *mut IpasirPropStore);
 	prop.pqueue.clear();
@@ -349,6 +360,7 @@ pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, l
 	prop.cqueue = None;
 	prop.prop.notify_backtrack(level);
 }
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_check_model_cb(
 	state: *mut c_void,
 	len: usize,
@@ -369,6 +381,7 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb(
 	};
 	prop.prop.check_model(&value)
 }
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 {
 	let prop = &mut *(state as *mut IpasirPropStore);
 	if let Some(l) = prop.prop.decide() {
@@ -377,6 +390,7 @@ pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 {
 		0
 	}
 }
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 {
 	let prop = &mut *(state as *mut IpasirPropStore);
 	if prop.pqueue.is_empty() {
@@ -389,6 +403,7 @@ pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 {
 		0 // No propagation
 	}
 }
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb(
 	state: *mut c_void,
 	propagated_lit: i32,
@@ -409,12 +424,13 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb(
 		0
 	}
 }
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb(state: *mut c_void) -> bool {
 	let prop = &mut *(state as *mut IpasirPropStore);
 	prop.cqueue = prop.prop.add_external_clause().map(Vec::into);
 	prop.cqueue.is_some()
 }
-
+#[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb(state: *mut c_void) -> i32 {
 	let prop = &mut *(state as *mut IpasirPropStore);
 	if prop.cqueue.is_none() {