diff --git a/executor/src/witgen/affine_expression.rs b/executor/src/witgen/affine_expression.rs
index 16de7bf2b..c8c52a53a 100644
--- a/executor/src/witgen/affine_expression.rs
+++ b/executor/src/witgen/affine_expression.rs
@@ -66,7 +66,12 @@ where
             .iter()
             .filter_map(|(i, c)| (!c.is_zero()).then_some((*i, c)))
     }
+}
 
+impl<'x, K> AffineExpression<K>
+where
+    K: Copy + Ord + Display + 'x,
+{
     /// If the affine expression has only a single variable (with nonzero coefficient),
     /// returns the index of the variable and the assignment that evaluates the
     /// affine expression to zero.
@@ -115,7 +120,7 @@ where
         // Try to solve directly.
         match self.solve() {
             Ok(value) if value.is_complete() => return Ok(value),
-            Err(()) => return Err(ConstraintUnsatisfiable(String::new())),
+            Err(()) => return Err(ConstraintUnsatisfiable(self.to_string())),
             Ok(value) => {
                 // sanity check that we are not ignoring anything useful here
                 assert!(value.constraints.is_empty());
diff --git a/executor/src/witgen/eval_result.rs b/executor/src/witgen/eval_result.rs
index 6b8c349fa..12ac6bb6c 100644
--- a/executor/src/witgen/eval_result.rs
+++ b/executor/src/witgen/eval_result.rs
@@ -181,7 +181,7 @@ impl fmt::Display for EvalError {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
             EvalError::ConstraintUnsatisfiable(e) => {
-                write!(f, "Linear constraint is not satisfiable: {e}",)
+                write!(f, "Linear constraint is not satisfiable: {e} != 0",)
             }
             EvalError::Multiple(errors) => {
                 for e in errors {
diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs
index aa1ab8990..0c1762587 100644
--- a/executor/src/witgen/generator.rs
+++ b/executor/src/witgen/generator.rs
@@ -104,7 +104,14 @@ where
                     kind => {
                         unimplemented!("Identity of kind {kind:?} is not supported in the executor")
                     }
-                };
+                }
+                .map_err(|err| {
+                    format!(
+                        "No progress on {identity}:\n{}",
+                        indent(&format!("{err}"), "    ")
+                    )
+                    .into()
+                });
 
                 if result.is_err() {
                     identity_failed = true;
diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs
index 0a1a9562d..62d43ff89 100644
--- a/executor/src/witgen/machines/block_machine.rs
+++ b/executor/src/witgen/machines/block_machine.rs
@@ -406,13 +406,7 @@ impl BlockMachine {
         };
         evaluated.solve_with_bit_constraints(self).map_err(|e| {
             let formatted = evaluated.to_string();
-            if let EvalError::ConstraintUnsatisfiable(_) = e {
-                EvalError::ConstraintUnsatisfiable(format!(
-                    "Constraint is invalid ({formatted} != 0)."
-                ))
-            } else {
-                format!("Could not solve expression {formatted} = 0: {e}").into()
-            }
+            format!("Could not solve expression {formatted} = 0: {e}").into()
         })
     }