diff --git a/crates/lean_compiler/src/a_simplify_lang.rs b/crates/lean_compiler/src/a_simplify_lang.rs
index 2abedf59..cbaf087d 100644
--- a/crates/lean_compiler/src/a_simplify_lang.rs
+++ b/crates/lean_compiler/src/a_simplify_lang.rs
@@ -2,8 +2,8 @@ use crate::{
     Counter, F,
     ir::HighLevelOperation,
     lang::{
-        AssignmentTarget, AssumeBoolean, Condition, ConstExpression, ConstMallocLabel, ConstantValue, Context,
-        Expression, Function, Line, Program, Scope, SimpleExpr, Var,
+        AssignmentTarget, Condition, ConstExpression, ConstMallocLabel, Context, Expression, Function, Line, MathExpr,
+        Program, Scope, SimpleExpr, Var,
     },
     parser::ConstArrayValue,
 };
@@ -529,7 +529,7 @@ fn check_boolean_scoping(boolean: &BooleanExpr<Expression>, ctx: &Context) {
 
 fn check_condition_scoping(condition: &Condition, ctx: &Context) {
     match condition {
-        Condition::Expression(expr, _) => {
+        Condition::AssumeBoolean(expr) => {
             check_expr_scoping(expr, ctx);
         }
         Condition::Comparison(boolean) => {
@@ -723,11 +723,10 @@ fn simplify_lines(
                                         if let (SimpleExpr::Constant(left_cst), SimpleExpr::Constant(right_cst)) =
                                             (&left, &right)
                                         {
-                                            let result = ConstExpression::Binary {
-                                                left: Box::new(left_cst.clone()),
-                                                operation: *operation,
-                                                right: Box::new(right_cst.clone()),
-                                            }
+                                            let result = ConstExpression::MathExpr(
+                                                MathExpr::Binary(*operation),
+                                                vec![left_cst.clone(), right_cst.clone()],
+                                            )
                                             .try_naive_simplification();
                                             res.push(SimpleLine::equality(var.clone(), SimpleExpr::Constant(result)));
                                         } else {
@@ -855,28 +854,8 @@ fn simplify_lines(
                         });
                         (diff_var.into(), then_branch, else_branch)
                     }
-                    Condition::Expression(condition, assume_boolean) => {
+                    Condition::AssumeBoolean(condition) => {
                         let condition_simplified = simplify_expr(ctx, state, const_malloc, condition, &mut res);
-
-                        match assume_boolean {
-                            AssumeBoolean::AssumeBoolean => {}
-                            AssumeBoolean::DoNotAssumeBoolean => {
-                                // Check condition_simplified is boolean
-                                let one_minus_condition_var = state.counters.aux_var();
-                                res.push(SimpleLine::Assignment {
-                                    var: one_minus_condition_var.clone().into(),
-                                    operation: HighLevelOperation::Sub,
-                                    arg0: SimpleExpr::Constant(ConstExpression::Value(ConstantValue::Scalar(1))),
-                                    arg1: condition_simplified.clone(),
-                                });
-                                res.push(SimpleLine::AssertZero {
-                                    operation: HighLevelOperation::Mul,
-                                    arg0: condition_simplified.clone(),
-                                    arg1: one_minus_condition_var.into(),
-                                });
-                            }
-                        }
-
                         (condition_simplified, then_branch, else_branch)
                     }
                 };
@@ -1194,11 +1173,10 @@ fn simplify_expr(
             let right_var = simplify_expr(ctx, state, const_malloc, right, lines);
 
             if let (SimpleExpr::Constant(left_cst), SimpleExpr::Constant(right_cst)) = (&left_var, &right_var) {
-                return SimpleExpr::Constant(ConstExpression::Binary {
-                    left: Box::new(left_cst.clone()),
-                    operation: *operation,
-                    right: Box::new(right_cst.clone()),
-                });
+                return SimpleExpr::Constant(ConstExpression::MathExpr(
+                    MathExpr::Binary(*operation),
+                    vec![left_cst.clone(), right_cst.clone()],
+                ));
             }
 
             let aux_var = state.counters.aux_var();
@@ -1275,7 +1253,7 @@ pub fn find_variable_usage(
                 on_new_expr(&comp.left, internal_vars, external_vars);
                 on_new_expr(&comp.right, internal_vars, external_vars);
             }
-            Condition::Expression(expr, _assume_boolean) => {
+            Condition::AssumeBoolean(expr) => {
                 on_new_expr(expr, internal_vars, external_vars);
             }
         };
@@ -1444,7 +1422,7 @@ fn inline_lines(
 
     let inline_condition = |condition: &mut Condition| match condition {
         Condition::Comparison(comparison) => inline_comparison(comparison),
-        Condition::Expression(expr, _assume_boolean) => inline_expr(expr, args, inlining_count),
+        Condition::AssumeBoolean(expr) => inline_expr(expr, args, inlining_count),
     };
 
     let inline_internal_var = |var: &mut Var| {
@@ -1883,7 +1861,7 @@ fn replace_vars_for_unroll(
                             internal_vars,
                         );
                     }
-                    Condition::Expression(expr, _assume_bool) => {
+                    Condition::AssumeBoolean(expr) => {
                         replace_vars_for_unroll_in_expr(expr, iterator, unroll_index, iterator_value, internal_vars);
                     }
                 }
@@ -2142,9 +2120,9 @@ fn extract_inlined_calls_from_condition(
     inlined_var_counter: &mut Counter,
 ) -> (Condition, Vec<Line>) {
     match condition {
-        Condition::Expression(expr, assume_boolean) => {
+        Condition::AssumeBoolean(expr) => {
             let (expr, expr_lines) = extract_inlined_calls_from_expr(expr, inlined_functions, inlined_var_counter);
-            (Condition::Expression(expr, *assume_boolean), expr_lines)
+            (Condition::AssumeBoolean(expr), expr_lines)
         }
         Condition::Comparison(boolean) => {
             let (boolean, boolean_lines) =
@@ -2719,7 +2697,7 @@ fn replace_vars_by_const_in_lines(lines: &mut [Line], map: &BTreeMap<Var, F>) {
                         replace_vars_by_const_in_expr(&mut cond.left, map);
                         replace_vars_by_const_in_expr(&mut cond.right, map);
                     }
-                    Condition::Expression(expr, _assume_boolean) => {
+                    Condition::AssumeBoolean(expr) => {
                         replace_vars_by_const_in_expr(expr, map);
                     }
                 }
diff --git a/crates/lean_compiler/src/b_compile_intermediate.rs b/crates/lean_compiler/src/b_compile_intermediate.rs
index f6a4f86f..ddc1cc53 100644
--- a/crates/lean_compiler/src/b_compile_intermediate.rs
+++ b/crates/lean_compiler/src/b_compile_intermediate.rs
@@ -51,11 +51,10 @@ impl Compiler {
             VarOrConstMallocAccess::ConstMallocAccess { malloc_label, offset } => {
                 for scope in self.stack_frame_layout.scopes.iter().rev() {
                     if let Some(base) = scope.const_mallocs.get(malloc_label) {
-                        return ConstExpression::Binary {
-                            left: Box::new((*base).into()),
-                            operation: HighLevelOperation::Add,
-                            right: Box::new((*offset).clone()),
-                        };
+                        return ConstExpression::MathExpr(
+                            MathExpr::Binary(HighLevelOperation::Add),
+                            vec![(*base).into(), offset.clone()],
+                        );
                     }
                 }
                 panic!("Const malloc {malloc_label} not in scope");
@@ -518,7 +517,7 @@ fn compile_lines(
                 });
             }
             SimpleLine::ConstMalloc { var, size, label } => {
-                let size = size.naive_eval().unwrap().to_usize(); // TODO not very good;
+                let size = size.naive_eval().unwrap().to_usize();
                 if !compiler.is_in_scope(var) {
                     let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
                     current_scope_layout
diff --git a/crates/lean_compiler/src/grammar.pest b/crates/lean_compiler/src/grammar.pest
index 9a1f57f2..bc2905a6 100644
--- a/crates/lean_compiler/src/grammar.pest
+++ b/crates/lean_compiler/src/grammar.pest
@@ -29,11 +29,8 @@ statement = {
     return_statement |
     break_statement |
     continue_statement |
-    assert_eq_statement |
-    assert_not_eq_statement  |
-    debug_assert_eq_statement |
-    debug_assert_not_eq_statement |
-    debug_assert_lt_statement |
+    assert_statement |
+    debug_assert_statement |
     assignment
 }
 
@@ -51,10 +48,14 @@ assignment_target = { array_access_expr | identifier }
 
 if_statement = { "if" ~ condition ~ "{" ~ statement* ~ "}" ~ else_if_clause* ~ else_clause? }
 
-condition = { expression | assumed_bool_expr }
+condition = { assumed_bool_expr | comparison }
 
 assumed_bool_expr = { "!!assume_bool" ~ "(" ~ expression ~ ")" }
 
+// Comparisons (shared between conditions and assertions)
+comparison = { add_expr ~ comparison_op ~ add_expr }
+comparison_op = { "==" | "!=" | "<" }
+
 else_if_clause = { "else" ~ "if" ~ condition ~ "{" ~ statement* ~ "}" }
 
 else_clause = { "else" ~ "{" ~ statement* ~ "}" }
@@ -67,18 +68,12 @@ match_statement = { "match" ~ expression ~ "{" ~ match_arm* ~ "}" }
 match_arm = { pattern ~ "=>" ~ "{" ~ statement* ~ "}" }
 pattern = { constant_value }
 
-assert_eq_statement = { "assert" ~ add_expr ~ "==" ~ add_expr ~ ";" }
-assert_not_eq_statement = { "assert" ~ add_expr ~ "!=" ~ add_expr ~ ";" }
-
-debug_assert_eq_statement = { "debug_assert" ~ add_expr ~ "==" ~ add_expr ~ ";" }
-debug_assert_not_eq_statement = { "debug_assert" ~ add_expr ~ "!=" ~ add_expr ~ ";" }
-debug_assert_lt_statement = { "debug_assert" ~ add_expr ~ "<" ~ add_expr ~ ";" }
+assert_statement = { "assert" ~ comparison ~ ";" }
+debug_assert_statement = { "debug_assert" ~ comparison ~ ";" }
 
 // Expressions
 tuple_expression = { expression ~ ("," ~ expression)* }
-expression = { neq_expr }
-neq_expr = { eq_expr ~ ("!=" ~ eq_expr)* }
-eq_expr = { add_expr ~ ("==" ~ add_expr)* }
+expression = { add_expr }
 add_expr = { sub_expr ~ ("+" ~ sub_expr)* }
 sub_expr = { mul_expr ~ ("-" ~ mul_expr)* }
 mul_expr = { mod_expr ~ ("*" ~ mod_expr)* }
diff --git a/crates/lean_compiler/src/ir/instruction.rs b/crates/lean_compiler/src/ir/instruction.rs
index 8e633b35..5fc66446 100644
--- a/crates/lean_compiler/src/ir/instruction.rs
+++ b/crates/lean_compiler/src/ir/instruction.rs
@@ -94,10 +94,7 @@ impl IntermediateInstruction {
                 arg_c,
                 res: arg_a,
             },
-            HighLevelOperation::Exp
-            | HighLevelOperation::Mod
-            | HighLevelOperation::Equal
-            | HighLevelOperation::NotEqual => unreachable!(),
+            HighLevelOperation::Exp | HighLevelOperation::Mod => unreachable!(),
         }
     }
 
diff --git a/crates/lean_compiler/src/ir/operation.rs b/crates/lean_compiler/src/ir/operation.rs
index da8660b6..59a5107a 100644
--- a/crates/lean_compiler/src/ir/operation.rs
+++ b/crates/lean_compiler/src/ir/operation.rs
@@ -4,10 +4,6 @@ use multilinear_toolkit::prelude::*;
 use std::fmt::{Display, Formatter};
 use utils::ToUsize;
 
-/// High-level operations that can be performed in the IR.
-///
-/// These operations represent the semantic intent of computations
-/// and may be lowered to different VM operations depending on context.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum HighLevelOperation {
     /// Addition operation.
@@ -22,29 +18,11 @@ pub enum HighLevelOperation {
     Exp,
     /// Modulo operation (only for constant expressions).
     Mod,
-    /// Equality comparison
-    Equal,
-    /// Non-equality comparison
-    NotEqual,
 }
 
 impl HighLevelOperation {
     pub fn eval(&self, a: F, b: F) -> F {
         match self {
-            Self::Equal => {
-                if a == b {
-                    F::ONE
-                } else {
-                    F::ZERO
-                }
-            }
-            Self::NotEqual => {
-                if a != b {
-                    F::ONE
-                } else {
-                    F::ZERO
-                }
-            }
             Self::Add => a + b,
             Self::Mul => a * b,
             Self::Sub => a - b,
@@ -58,8 +36,6 @@ impl HighLevelOperation {
 impl Display for HighLevelOperation {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         match self {
-            Self::Equal => write!(f, "=="),
-            Self::NotEqual => write!(f, "!="),
             Self::Add => write!(f, "+"),
             Self::Mul => write!(f, "*"),
             Self::Sub => write!(f, "-"),
diff --git a/crates/lean_compiler/src/lang.rs b/crates/lean_compiler/src/lang.rs
index 3a421853..de35994a 100644
--- a/crates/lean_compiler/src/lang.rs
+++ b/crates/lean_compiler/src/lang.rs
@@ -115,11 +115,6 @@ pub enum ConstantValue {
 #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum ConstExpression {
     Value(ConstantValue),
-    Binary {
-        left: Box<Self>,
-        operation: HighLevelOperation,
-        right: Box<Self>,
-    },
     MathExpr(MathExpr, Vec<Self>),
 }
 
@@ -140,11 +135,7 @@ impl TryFrom<Expression> for ConstExpression {
             Expression::Binary { left, operation, right } => {
                 let left_expr = Self::try_from(*left)?;
                 let right_expr = Self::try_from(*right)?;
-                Ok(Self::Binary {
-                    left: Box::new(left_expr),
-                    operation,
-                    right: Box::new(right_expr),
-                })
+                Ok(Self::MathExpr(MathExpr::Binary(operation), vec![left_expr, right_expr]))
             }
             Expression::MathExpr(math_expr, args) => {
                 let mut const_args = Vec::new();
@@ -185,9 +176,6 @@ impl ConstExpression {
     {
         match self {
             Self::Value(value) => func(value),
-            Self::Binary { left, operation, right } => {
-                Some(operation.eval(left.eval_with(func)?, right.eval_with(func)?))
-            }
             Self::MathExpr(math_expr, args) => {
                 let mut eval_args = Vec::new();
                 for arg in args {
@@ -220,25 +208,16 @@ impl From<ConstantValue> for ConstExpression {
     }
 }
 
-#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum AssumeBoolean {
-    AssumeBoolean,
-    DoNotAssumeBoolean,
-}
-
 #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum Condition {
-    Expression(Expression, AssumeBoolean),
+    AssumeBoolean(Expression),
     Comparison(BooleanExpr<Expression>),
 }
 
 impl Display for Condition {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         match self {
-            Self::Expression(expr, AssumeBoolean::AssumeBoolean) => {
-                write!(f, "!assume_bool({expr})")
-            }
-            Self::Expression(expr, AssumeBoolean::DoNotAssumeBoolean) => write!(f, "{expr}"),
+            Self::AssumeBoolean(expr) => write!(f, "{expr}"),
             Self::Comparison(cmp) => write!(f, "{cmp}"),
         }
     }
@@ -270,6 +249,7 @@ pub enum Expression {
 /// For arbitrary compile-time computations
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum MathExpr {
+    Binary(HighLevelOperation),
     Log2Ceil,
     NextMultipleOf,
     SaturatingSub,
@@ -278,6 +258,7 @@ pub enum MathExpr {
 impl Display for MathExpr {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         match self {
+            Self::Binary(op) => write!(f, "{op}"),
             Self::Log2Ceil => write!(f, "log2_ceil"),
             Self::NextMultipleOf => write!(f, "next_multiple_of"),
             Self::SaturatingSub => write!(f, "saturating_sub"),
@@ -288,6 +269,7 @@ impl Display for MathExpr {
 impl MathExpr {
     pub fn num_args(&self) -> usize {
         match self {
+            Self::Binary(_) => 2,
             Self::Log2Ceil => 1,
             Self::NextMultipleOf => 2,
             Self::SaturatingSub => 2,
@@ -295,6 +277,10 @@ impl MathExpr {
     }
     pub fn eval(&self, args: &[F]) -> F {
         match self {
+            Self::Binary(op) => {
+                assert_eq!(args.len(), 2);
+                op.eval(args[0], args[1])
+            }
             Self::Log2Ceil => {
                 assert_eq!(args.len(), 1);
                 let value = args[0];
@@ -722,9 +708,6 @@ impl Display for ConstExpression {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         match self {
             Self::Value(value) => write!(f, "{value}"),
-            Self::Binary { left, operation, right } => {
-                write!(f, "({left} {operation} {right})")
-            }
             Self::MathExpr(math_expr, args) => {
                 let args_str = args.iter().map(|arg| format!("{arg}")).collect::<Vec<_>>().join(", ");
                 write!(f, "{math_expr}({args_str})")
diff --git a/crates/lean_compiler/src/parser/parsers/expression.rs b/crates/lean_compiler/src/parser/parsers/expression.rs
index 98991af6..4a696ae0 100644
--- a/crates/lean_compiler/src/parser/parsers/expression.rs
+++ b/crates/lean_compiler/src/parser/parsers/expression.rs
@@ -5,12 +5,11 @@ use crate::{
     ir::HighLevelOperation,
     lang::{ConstExpression, ConstantValue, Expression, SimpleExpr},
     parser::{
-        error::{ParseError, ParseResult, SemanticError},
+        error::{ParseResult, SemanticError},
         grammar::{ParsePair, Rule},
     },
 };
 
-/// Parser for all expression types.
 pub struct ExpressionParser;
 
 impl Parse<Expression> for ExpressionParser {
@@ -20,8 +19,6 @@ impl Parse<Expression> for ExpressionParser {
                 let inner = next_inner_pair(&mut pair.into_inner(), "expression body")?;
                 Self.parse(inner, ctx)
             }
-            Rule::neq_expr => BinaryExpressionParser::parse_with_op(pair, ctx, HighLevelOperation::NotEqual),
-            Rule::eq_expr => BinaryExpressionParser::parse_with_op(pair, ctx, HighLevelOperation::Equal),
             Rule::add_expr => BinaryExpressionParser::parse_with_op(pair, ctx, HighLevelOperation::Add),
             Rule::sub_expr => BinaryExpressionParser::parse_with_op(pair, ctx, HighLevelOperation::Sub),
             Rule::mul_expr => BinaryExpressionParser::parse_with_op(pair, ctx, HighLevelOperation::Mul),
@@ -29,14 +26,11 @@ impl Parse<Expression> for ExpressionParser {
             Rule::div_expr => BinaryExpressionParser::parse_with_op(pair, ctx, HighLevelOperation::Div),
             Rule::exp_expr => BinaryExpressionParser::parse_with_op(pair, ctx, HighLevelOperation::Exp),
             Rule::primary => PrimaryExpressionParser.parse(pair, ctx),
-            other_rule => Err(ParseError::SemanticError(SemanticError::new(format!(
-                "ExpressionParser: Unexpected rule {other_rule:?}"
-            )))),
+            other_rule => Err(SemanticError::new(format!("ExpressionParser: Unexpected rule {other_rule:?}")).into()),
         }
     }
 }
 
-/// Parser for binary arithmetic operations.
 pub struct BinaryExpressionParser;
 
 impl BinaryExpressionParser {
diff --git a/crates/lean_compiler/src/parser/parsers/statement.rs b/crates/lean_compiler/src/parser/parsers/statement.rs
index 915b8f27..0052a25e 100644
--- a/crates/lean_compiler/src/parser/parsers/statement.rs
+++ b/crates/lean_compiler/src/parser/parsers/statement.rs
@@ -6,8 +6,7 @@ use super::literal::ConstExprParser;
 use super::{Parse, ParseContext, next_inner_pair};
 use crate::{
     SourceLineNumber,
-    ir::HighLevelOperation,
-    lang::{AssumeBoolean, Condition, Expression, Line, SourceLocation},
+    lang::{Condition, Expression, Line, SourceLocation},
     parser::{
         error::{ParseResult, SemanticError},
         grammar::{ParsePair, Rule},
@@ -28,11 +27,8 @@ impl Parse<Line> for StatementParser {
             Rule::for_statement => ForStatementParser.parse(inner, ctx),
             Rule::match_statement => MatchStatementParser.parse(inner, ctx),
             Rule::return_statement => ReturnStatementParser.parse(inner, ctx),
-            Rule::assert_eq_statement => AssertEqParser::<false>.parse(inner, ctx),
-            Rule::assert_not_eq_statement => AssertNotEqParser::<false>.parse(inner, ctx),
-            Rule::debug_assert_eq_statement => AssertEqParser::<true>.parse(inner, ctx),
-            Rule::debug_assert_not_eq_statement => AssertNotEqParser::<true>.parse(inner, ctx),
-            Rule::debug_assert_lt_statement => AssertLtParser::<true>.parse(inner, ctx),
+            Rule::assert_statement => AssertParser::<false>.parse(inner, ctx),
+            Rule::debug_assert_statement => AssertParser::<true>.parse(inner, ctx),
             Rule::break_statement => Ok(Line::Break),
             Rule::continue_statement => Err(SemanticError::new("Continue statement not implemented yet").into()),
             _ => Err(SemanticError::new("Unknown statement").into()),
@@ -145,38 +141,40 @@ pub struct ConditionParser;
 impl Parse<Condition> for ConditionParser {
     fn parse(&self, pair: ParsePair<'_>, ctx: &mut ParseContext) -> ParseResult<Condition> {
         let inner_pair = next_inner_pair(&mut pair.into_inner(), "inner expression")?;
-        if inner_pair.as_rule() == Rule::assumed_bool_expr {
-            ExpressionParser
+        match inner_pair.as_rule() {
+            Rule::assumed_bool_expr => ExpressionParser
                 .parse(next_inner_pair(&mut inner_pair.into_inner(), "inner expression")?, ctx)
-                .map(|e| Condition::Expression(e, AssumeBoolean::AssumeBoolean))
-        } else {
-            let expr_result = ExpressionParser.parse(inner_pair, ctx);
-            match expr_result {
-                Err(e) => Err(e),
-                Ok(Expression::Binary {
-                    left,
-                    operation: HighLevelOperation::Equal,
-                    right,
-                }) => Ok(Condition::Comparison(BooleanExpr {
-                    left: *left,
-                    right: *right,
-                    kind: Boolean::Equal,
-                })),
-                Ok(Expression::Binary {
-                    left,
-                    operation: HighLevelOperation::NotEqual,
-                    right,
-                }) => Ok(Condition::Comparison(BooleanExpr {
-                    left: *left,
-                    right: *right,
-                    kind: Boolean::Different,
-                })),
-                Ok(expr) => Ok(Condition::Expression(expr, AssumeBoolean::DoNotAssumeBoolean)),
+                .map(Condition::AssumeBoolean),
+            Rule::comparison => {
+                let boolean = ComparisonParser::parse(inner_pair, ctx)?;
+                Ok(Condition::Comparison(boolean))
             }
+            _ => Err(SemanticError::new("Invalid condition").into()),
         }
     }
 }
 
+/// Parser for comparison expressions (shared between conditions and assertions).
+pub struct ComparisonParser;
+
+impl ComparisonParser {
+    pub fn parse(pair: ParsePair<'_>, ctx: &mut ParseContext) -> ParseResult<BooleanExpr<Expression>> {
+        let mut inner = pair.into_inner();
+        let left = ExpressionParser.parse(next_inner_pair(&mut inner, "left side")?, ctx)?;
+        let op = next_inner_pair(&mut inner, "comparison operator")?;
+        let right = ExpressionParser.parse(next_inner_pair(&mut inner, "right side")?, ctx)?;
+
+        let kind = match op.as_str() {
+            "==" => Boolean::Equal,
+            "!=" => Boolean::Different,
+            "<" => Boolean::LessThan,
+            _ => unreachable!(),
+        };
+
+        Ok(BooleanExpr { left, right, kind })
+    }
+}
+
 /// Parser for for-loop statements.
 pub struct ForStatementParser;
 
@@ -315,66 +313,18 @@ impl Parse<Line> for ReturnStatementParser {
     }
 }
 
-/// Parser for equality assertions.
-pub struct AssertEqParser<const DEBUG: bool>;
+/// Parser for assert statements.
+pub struct AssertParser<const DEBUG: bool>;
 
-impl<const DEBUG: bool> Parse<Line> for AssertEqParser<DEBUG> {
+impl<const DEBUG: bool> Parse<Line> for AssertParser<DEBUG> {
     fn parse(&self, pair: ParsePair<'_>, ctx: &mut ParseContext) -> ParseResult<Line> {
         let line_number = pair.line_col().0;
-        let mut inner = pair.into_inner();
-        let left = ExpressionParser.parse(next_inner_pair(&mut inner, "left assertion")?, ctx)?;
-        let right = ExpressionParser.parse(next_inner_pair(&mut inner, "right assertion")?, ctx)?;
+        let comparison = next_inner_pair(&mut pair.into_inner(), "comparison")?;
+        let boolean = ComparisonParser::parse(comparison, ctx)?;
 
         Ok(Line::Assert {
             debug: DEBUG,
-            boolean: BooleanExpr {
-                left,
-                right,
-                kind: Boolean::Equal,
-            },
-            line_number,
-        })
-    }
-}
-
-/// Parser for inequality assertions.
-pub struct AssertNotEqParser<const DEBUG: bool>;
-
-impl<const DEBUG: bool> Parse<Line> for AssertNotEqParser<DEBUG> {
-    fn parse(&self, pair: ParsePair<'_>, ctx: &mut ParseContext) -> ParseResult<Line> {
-        let line_number = pair.line_col().0;
-        let mut inner = pair.into_inner();
-        let left = ExpressionParser.parse(next_inner_pair(&mut inner, "left assertion")?, ctx)?;
-        let right = ExpressionParser.parse(next_inner_pair(&mut inner, "right assertion")?, ctx)?;
-
-        Ok(Line::Assert {
-            debug: DEBUG,
-            boolean: BooleanExpr {
-                left,
-                right,
-                kind: Boolean::Different,
-            },
-            line_number,
-        })
-    }
-}
-
-pub struct AssertLtParser<const DEBUG: bool>;
-
-impl<const DEBUG: bool> Parse<Line> for AssertLtParser<DEBUG> {
-    fn parse(&self, pair: ParsePair<'_>, ctx: &mut ParseContext) -> ParseResult<Line> {
-        let line_number = pair.line_col().0;
-        let mut inner = pair.into_inner();
-        let left = ExpressionParser.parse(next_inner_pair(&mut inner, "left assertion")?, ctx)?;
-        let right = ExpressionParser.parse(next_inner_pair(&mut inner, "right assertion")?, ctx)?;
-
-        Ok(Line::Assert {
-            debug: DEBUG,
-            boolean: BooleanExpr {
-                left,
-                right,
-                kind: Boolean::LessThan,
-            },
+            boolean,
             line_number,
         })
     }
diff --git a/crates/lean_compiler/tests/test_compiler.rs b/crates/lean_compiler/tests/test_compiler.rs
index 759040d7..5fcc7037 100644
--- a/crates/lean_compiler/tests/test_compiler.rs
+++ b/crates/lean_compiler/tests/test_compiler.rs
@@ -370,7 +370,7 @@ fn test_mini_program_2() {
             for j in i..10 {
                 for k in j..10 {
                     sum, prod = compute_sum_and_product(i, j, k);
-                    if (sum == 10) {
+                    if sum == 10 {
                         print(i, j, k, prod);
                     }
                 }
@@ -548,7 +548,7 @@ fn test_inlined_2() {
     }
 
     fn is_one() inline -> 1 {
-        if 1 {
+        if !!assume_bool(1) {
             return 1;
         } else {
             return 0;