diff --git a/solver/src/model/lang.rs b/solver/src/model/lang.rs
index 0c961893..64bc4dd8 100644
--- a/solver/src/model/lang.rs
+++ b/solver/src/model/lang.rs
@@ -7,6 +7,7 @@ mod fixed;
 mod int;
 pub mod linear;
 pub mod max;
+pub mod mul;
 pub mod reification;
 mod sym;
 mod validity_scope;
diff --git a/solver/src/model/lang/max.rs b/solver/src/model/lang/max.rs
index c5d21504..a296ab4e 100644
--- a/solver/src/model/lang/max.rs
+++ b/solver/src/model/lang/max.rs
@@ -5,7 +5,7 @@ use crate::reif::ReifExpr;
 use itertools::Itertools;
 use std::fmt::{Debug, Formatter};
 
-/// Constraint equivalent to `lhs = max { e | e \in rhs }
+/// Constraint equivalent to `lhs = max { e | e \in rhs }`
 pub struct EqMax {
     lhs: IAtom,
     rhs: Vec<IAtom>,
@@ -20,7 +20,7 @@ impl EqMax {
     }
 }
 
-/// Constraint equivalent to `lhs = min { e | e \in rhs }
+/// Constraint equivalent to `lhs = min { e | e \in rhs }`
 pub struct EqMin {
     lhs: IAtom,
     rhs: Vec<IAtom>,
diff --git a/solver/src/model/lang/mul.rs b/solver/src/model/lang/mul.rs
new file mode 100644
index 00000000..4784f7ad
--- /dev/null
+++ b/solver/src/model/lang/mul.rs
@@ -0,0 +1,15 @@
+use crate::core::{Lit, VarRef};
+use std::fmt::{Debug, Formatter};
+
+#[derive(Eq, PartialEq, Hash, Clone)]
+pub struct NFEqVarMulLit {
+    pub lhs: VarRef,
+    pub rhs: VarRef,
+    pub lit: Lit,
+}
+
+impl Debug for NFEqVarMulLit {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?} = {:?} * {:?}", self.lhs, self.lit, self.rhs)
+    }
+}
diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs
index fac8e4bf..2a5eeb25 100644
--- a/solver/src/reasoners/cp/mod.rs
+++ b/solver/src/reasoners/cp/mod.rs
@@ -12,8 +12,10 @@ use crate::core::{IntCst, Lit, SignedVar, VarRef, INT_CST_MAX, INT_CST_MIN};
 use crate::create_ref_type;
 use crate::model::extensions::AssignmentExt;
 use crate::model::lang::linear::NFLinearLeq;
+use crate::model::lang::mul::NFEqVarMulLit;
 use crate::reasoners::{Contradiction, ReasonerId, Theory};
 use anyhow::Context;
+use mul::VarEqVarMulLit;
 
 use crate::reasoners::cp::linear::{LinearSumLeq, SumElem};
 use crate::reasoners::cp::max::AtLeastOneGeq;
@@ -121,6 +123,15 @@ impl Cp {
         self.add_propagator(propagator);
     }
 
+    pub fn add_eq_var_mul_lit_constraint(&mut self, mul: &NFEqVarMulLit) {
+        let propagator = VarEqVarMulLit {
+            reified: mul.lhs,
+            original: mul.rhs,
+            lit: mul.lit,
+        };
+        self.add_propagator(propagator);
+    }
+
     pub fn add_propagator(&mut self, propagator: impl Into<DynPropagator>) {
         // TODO: handle validity scopes
         let propagator = propagator.into();
diff --git a/solver/src/reif/mod.rs b/solver/src/reif/mod.rs
index 41ba5017..e442d12f 100644
--- a/solver/src/reif/mod.rs
+++ b/solver/src/reif/mod.rs
@@ -4,6 +4,7 @@ use crate::core::{IntCst, Lit, SignedVar, VarRef};
 use crate::model::lang::alternative::NFAlternative;
 use crate::model::lang::linear::NFLinearLeq;
 use crate::model::lang::max::NFEqMax;
+use crate::model::lang::mul::NFEqVarMulLit;
 use crate::model::lang::ValidityScope;
 use crate::model::{Label, Model};
 use std::fmt::{Debug, Formatter};
@@ -32,6 +33,7 @@ pub enum ReifExpr {
     Linear(NFLinearLeq),
     Alternative(NFAlternative),
     EqMax(NFEqMax),
+    EqVarMulLit(NFEqVarMulLit),
 }
 
 impl std::fmt::Display for ReifExpr {
@@ -48,6 +50,7 @@ impl std::fmt::Display for ReifExpr {
             ReifExpr::Linear(l) => write!(f, "{l}"),
             ReifExpr::EqMax(em) => write!(f, "{em:?}"),
             ReifExpr::Alternative(alt) => write!(f, "{alt:?}"),
+            ReifExpr::EqVarMulLit(em) => write!(f, "{em:?}"),
         }
     }
 }
@@ -75,6 +78,7 @@ impl ReifExpr {
             ReifExpr::Linear(lin) => lin.validity_scope(presence),
             ReifExpr::Alternative(alt) => ValidityScope::new([presence(alt.main)], []),
             ReifExpr::EqMax(eq_max) => ValidityScope::new([presence(eq_max.lhs.variable())], []),
+            ReifExpr::EqVarMulLit(em) => ValidityScope::new([presence(em.lhs)], []),
         }
     }
 
@@ -89,6 +93,7 @@ impl ReifExpr {
             OptDomain::Present(lb, ub) if lb == ub => lb,
             _ => panic!(),
         };
+        let lvalue = |lit: Lit| assignment.value(lit).unwrap();
         let sprez = |svar: SignedVar| prez(svar.variable());
         let svalue = |svar: SignedVar| {
             if svar.is_plus() {
@@ -202,6 +207,13 @@ impl ReifExpr {
                     Some(true)
                 }
             }
+            ReifExpr::EqVarMulLit(NFEqVarMulLit { lhs, rhs, lit }) => {
+                if prez(*lhs) && prez(*rhs) {
+                    Some(value(*lhs) == (lvalue(*lit) as i32) * value(*rhs))
+                } else {
+                    None
+                }
+            }
         }
     }
 }
@@ -254,6 +266,7 @@ impl Not for ReifExpr {
             ReifExpr::Linear(lin) => ReifExpr::Linear(!lin),
             ReifExpr::Alternative(_) => panic!("Alternative is a constraint and cannot be negated"),
             ReifExpr::EqMax(_) => panic!("EqMax is a constraint and cannot be negated"),
+            ReifExpr::EqVarMulLit(_) => panic!("EqVarMulLit is a constraint and cannot be negated"),
         }
     }
 }
diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs
index 7d1af33d..11dd7eed 100644
--- a/solver/src/solver/solver_impl.rs
+++ b/solver/src/solver/solver_impl.rs
@@ -403,6 +403,10 @@ impl<Lbl: Label> Solver<Lbl> {
 
                 Ok(())
             }
+            ReifExpr::EqVarMulLit(mul) => {
+                self.reasoners.cp.add_eq_var_mul_lit_constraint(mul);
+                Ok(())
+            }
         }
     }