diff --git a/crates/diagnostics/src/lib.rs b/crates/diagnostics/src/lib.rs
index 2b8e9f7..119f071 100644
--- a/crates/diagnostics/src/lib.rs
+++ b/crates/diagnostics/src/lib.rs
@@ -20,7 +20,7 @@ pub enum ErrorType {
     Parser,
     Semantics,
     Type,
-    Functional,
+    Verification,
 }
 
 impl Display for ErrorType {
@@ -31,7 +31,7 @@ impl Display for ErrorType {
             ErrorType::Parser => word("Parser error"),
             ErrorType::Semantics => word("Semantic error"),
             ErrorType::Type => word("Type error"),
-            ErrorType::Functional => word("Functional error"),
+            ErrorType::Verification => word("Verification error"),
         }
     }
 }
@@ -64,6 +64,8 @@ pub struct Report {
     pub level: Level,
     /// Message of an error
     pub message: String,
+
+    pub additional_info: Vec<Report>,
 }
 
 impl Report {
@@ -74,6 +76,7 @@ impl Report {
             error_type: ErrorType::Lexer,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -84,6 +87,7 @@ impl Report {
             error_type: ErrorType::Parser,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -94,6 +98,7 @@ impl Report {
             error_type: ErrorType::Semantics,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -104,6 +109,7 @@ impl Report {
             error_type: ErrorType::Semantics,
             level: Level::Warning,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -114,16 +120,28 @@ impl Report {
             error_type: ErrorType::Type,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
-    /// Build a report from the functional error.
-    pub fn func_error(loc: Span, message: String) -> Self {
+    /// Build a report from the verification error.
+    pub fn ver_error(loc: Span, message: String) -> Self {
+        Self {
+            loc,
+            error_type: ErrorType::Verification,
+            level: Level::Error,
+            message,
+            additional_info: vec![],
+        }
+    }
+    /// Build a report from the verification error with additional info.
+    pub fn ver_error_with_extra(loc: Span, message: String, errs: Vec<Report>) -> Self {
         Self {
             loc,
-            error_type: ErrorType::Functional,
+            error_type: ErrorType::Verification,
             level: Level::Error,
             message,
+            additional_info: errs,
         }
     }
 }
diff --git a/crates/semantics/src/expression/eval.rs b/crates/semantics/src/expression/eval.rs
index 445b971..c7e9762 100644
--- a/crates/semantics/src/expression/eval.rs
+++ b/crates/semantics/src/expression/eval.rs
@@ -586,7 +586,7 @@ where
     let a = TryGetValue::<T>::try_get(u.left.as_ref())?;
     let b = TryGetValue::<T>::try_get(u.right.as_ref())?;
     let result = func(a, b).ok_or_else(|| {
-        contract.diagnostics.push(Report::func_error(
+        contract.diagnostics.push(Report::semantic_error(
             loc.clone(),
             String::from("The operation is invalid. Probably resulted from the division by 0 or overflow/underflow."),
         ));
diff --git a/crates/verifier/src/ast.rs b/crates/verifier/src/ast.rs
index 049ab32..bff0cba 100644
--- a/crates/verifier/src/ast.rs
+++ b/crates/verifier/src/ast.rs
@@ -6,6 +6,7 @@ use folidity_semantics::{
 };
 use z3::{
     ast::{
+        Ast,
         Bool,
         Dynamic,
         Int,
@@ -72,72 +73,23 @@ impl<'ctx> ConstraintBlock<'ctx> {
     }
 }
 
-pub struct Variable<'ctx> {
-    /// Location of the expression
-    pub loc: Span,
-    /// Element of the expression.
-    pub element: Dynamic<'ctx>,
-}
-
-/// A list of Z3 concrete expression.
-/// Translated from the semantics AST?
-pub enum Z3Expression<'ctx> {
-    Variable(Z3UnaryExpression<usize>),
-
-    // Literals
-    Int(Z3UnaryExpression<Int<'ctx>>),
-    Real(Z3UnaryExpression<Real<'ctx>>),
-    Boolean(Z3UnaryExpression<Bool<'ctx>>),
-    String(Z3UnaryExpression<String<'ctx>>),
-
-    // Maths operations.
-    Multiply(Z3BinaryExpression),
-    Divide(Z3BinaryExpression),
-    Modulo(Z3BinaryExpression),
-    Add(Z3BinaryExpression),
-    Subtract(Z3BinaryExpression),
-
-    // Boolean relations.
-    Equal(Z3BinaryExpression),
-    NotEqual(Z3BinaryExpression),
-    Greater(Z3BinaryExpression),
-    Less(Z3BinaryExpression),
-    GreaterEq(Z3BinaryExpression),
-    LessEq(Z3BinaryExpression),
-    In(Z3BinaryExpression),
-    Not(Z3UnaryExpression<Box<Expression>>),
-
-    // Boolean operations.
-    Or(Z3BinaryExpression),
-    And(Z3BinaryExpression),
-
-    List(Z3UnaryExpression<Vec<Expression>>),
-}
-
 /// Represents unary style expression.
 ///
 /// # Example
 /// `false`
 #[derive(Clone, Debug, PartialEq)]
-pub struct Z3UnaryExpression<T> {
+pub struct Z3Expression<'ctx> {
     /// Location of the expression
     pub loc: Span,
     /// Element of the expression.
-    pub element: T,
+    pub element: Dynamic<'ctx>,
 }
 
-/// Represents binary-style expression.
-///
-/// # Example
-///
-/// - `10 + 2`
-/// - `a > b`
-#[derive(Clone, Debug, PartialEq)]
-pub struct Z3BinaryExpression {
-    /// Location of the parent expression.
-    pub loc: Span,
-    /// Left expression.
-    pub left: Box<Expression>,
-    /// Right expression
-    pub right: Box<Expression>,
+impl<'ctx> Z3Expression<'ctx> {
+    pub fn new(loc: &Span, e: &impl Ast<'ctx>) -> Self {
+        Self {
+            loc: loc.clone(),
+            element: Dynamic::from_ast(e),
+        }
+    }
 }
diff --git a/crates/verifier/src/resolver.rs b/crates/verifier/src/resolver.rs
index 54bef08..7202392 100644
--- a/crates/verifier/src/resolver.rs
+++ b/crates/verifier/src/resolver.rs
@@ -1,3 +1,5 @@
+use std::ops::Mul;
+
 use folidity_diagnostics::{
     Report,
     Span,
@@ -7,11 +9,12 @@ use num_bigint::BigInt;
 use num_rational::BigRational;
 use z3::{
     ast::{
+        Ast,
         Bool,
         Dynamic,
         Int,
         Real,
-        String,
+        String as Z3String,
     },
     Context,
 };
@@ -19,45 +22,49 @@ use z3::{
 use crate::{
     ast::{
         Constraint,
-        Z3BinaryExpression,
         Z3Expression,
-        Z3UnaryExpression,
     },
     executor::SymbolicExecutor,
 };
 
 /// Transforms [`folidity_semantics::ast::Expression`] into [`crate::ast::Z3Expression`]
 /// in some given context [`z3::Context`].
-pub fn transform_expr<'ctx>(expr: &Expression, ctx: &'ctx Context) -> Z3Expression<'ctx> {
+pub fn transform_expr<'ctx>(
+    expr: &Expression,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
     match expr {
         // literals
-        Expression::Int(u) => int(&u.element, &u.loc, ctx),
-        Expression::UInt(u) => int(&u.element.clone().into(), &u.loc, ctx),
-        Expression::Float(u) => real(&u.element, &u.loc, ctx),
-        Expression::Boolean(u) => bool(u.element, &u.loc, ctx),
-        Expression::String(u) => string(u.element.as_str(), &u.loc, ctx),
-        Expression::Char(u) => char(u.element, &u.loc, ctx),
-        Expression::Hex(u) => string(hex::encode(&u.element).as_str(), &u.loc, ctx),
-        Expression::Address(u) => string(u.element.to_string().as_str(), &u.loc, ctx),
-        Expression::Enum(u) => enum_(u.element, &u.loc, ctx),
+        Expression::Int(u) => Ok(int(&u.element, &u.loc, ctx)),
+        Expression::UInt(u) => Ok(int(&u.element.clone().into(), &u.loc, ctx)),
+        Expression::Float(u) => Ok(real(&u.element, &u.loc, ctx)),
+        Expression::Boolean(u) => Ok(bool(u.element, &u.loc, ctx)),
+        Expression::String(u) => Ok(string(u.element.as_str(), &u.loc, ctx)),
+        Expression::Char(u) => Ok(char(u.element, &u.loc, ctx)),
+        Expression::Hex(u) => Ok(string(hex::encode(&u.element).as_str(), &u.loc, ctx)),
+        Expression::Address(u) => Ok(string(u.element.to_string().as_str(), &u.loc, ctx)),
+        Expression::Enum(u) => Ok(enum_(u.element, &u.loc, ctx)),
 
         // binary operations
-        Expression::Multiply(_) => todo!(),
-        Expression::Divide(_) => todo!(),
-        Expression::Modulo(_) => todo!(),
-        Expression::Add(_) => todo!(),
-        Expression::Subtract(_) => todo!(),
-        Expression::Equal(_) => todo!(),
-        Expression::NotEqual(_) => todo!(),
-        Expression::Greater(_) => todo!(),
-        Expression::Less(_) => todo!(),
-        Expression::GreaterEq(_) => todo!(),
-        Expression::LessEq(_) => todo!(),
-        Expression::Not(_) => todo!(),
-        Expression::Or(_) => todo!(),
-        Expression::And(_) => todo!(),
-        Expression::In(_) => todo!(),
+        Expression::Add(_)
+        | Expression::Subtract(_)
+        | Expression::Multiply(_)
+        | Expression::Divide(_)
+        | Expression::Less(_)
+        | Expression::LessEq(_)
+        | Expression::Greater(_)
+        | Expression::GreaterEq(_) => int_real_op(expr, ctx, executor),
+
+        Expression::Modulo(b) => modulo(&b.left, &b.right, &b.loc, ctx, executor),
+        Expression::Equal(b) => equality(&b.left, &b.right, &b.loc, ctx, executor),
+        Expression::NotEqual(b) => inequality(&b.left, &b.right, &b.loc, ctx, executor),
+        Expression::Not(u) => not(&u.element, &u.loc, ctx, executor),
 
+        Expression::Or(b) => or(&b.left, &b.right, &b.loc, ctx, executor),
+        Expression::And(b) => and(&b.left, &b.right, &b.loc, ctx, executor),
+
+        Expression::In(_) => todo!(),
         Expression::MemberAccess(_) => todo!(),
         Expression::List(_) => todo!(),
         Expression::Variable(_) => todo!(),
@@ -71,51 +78,281 @@ pub fn transform_expr<'ctx>(expr: &Expression, ctx: &'ctx Context) -> Z3Expressi
     }
 }
 
+fn int_real_op<'ctx>(
+    e: &Expression,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
+    let (Expression::Multiply(b)
+    | Expression::Divide(b)
+    | Expression::Add(b)
+    | Expression::Subtract(b)
+    | Expression::Less(b)
+    | Expression::LessEq(b)
+    | Expression::Greater(b)
+    | Expression::GreaterEq(b)) = e
+    else {
+        unreachable!("Only [*, /, +, -, >, <, ≥, ≤] ops are allowed to be passed.");
+    };
+    let e1 = transform_expr(&b.left, ctx, executor)?;
+    let e2 = transform_expr(&b.right, ctx, executor)?;
+    let mut reports = Vec::new();
+    let int1 = to_z3_int(&e1, &mut reports);
+    let int2 = to_z3_int(&e2, &mut reports);
+    let real1 = to_z3_real(&e1, &mut reports);
+    let real2 = to_z3_real(&e2, &mut reports);
+    let res = match (int1, int2, real1, real2) {
+        (Ok(n1), Ok(n2), _, _) => {
+            match e {
+                Expression::Add(_) => Dynamic::from_ast(&(n1 + n2)),
+                Expression::Subtract(_) => Dynamic::from_ast(&(n1 - n2)),
+                Expression::Multiply(_) => Dynamic::from_ast(&(n1 * n2)),
+                Expression::Divide(_) => Dynamic::from_ast(&(n1 / n2)),
+                Expression::Less(_) => Dynamic::from_ast(&n1.lt(&n1)),
+                Expression::LessEq(_) => Dynamic::from_ast(&n1.le(&n1)),
+                Expression::Greater(_) => Dynamic::from_ast(&n1.gt(&n1)),
+                Expression::GreaterEq(_) => Dynamic::from_ast(&n1.ge(&n1)),
+                _ => unreachable!(),
+            }
+        }
+        (_, _, Ok(n1), Ok(n2)) => {
+            match e {
+                Expression::Add(_) => Dynamic::from_ast(&(n1 + n2)),
+                Expression::Subtract(_) => Dynamic::from_ast(&(n1 - n2)),
+                Expression::Multiply(_) => Dynamic::from_ast(&(n1 * n2)),
+                Expression::Divide(_) => Dynamic::from_ast(&(n1 / n2)),
+                Expression::Less(_) => Dynamic::from_ast(&n1.lt(&n1)),
+                Expression::LessEq(_) => Dynamic::from_ast(&n1.le(&n1)),
+                Expression::Greater(_) => Dynamic::from_ast(&n1.gt(&n1)),
+                Expression::GreaterEq(_) => Dynamic::from_ast(&n1.ge(&n1)),
+                _ => unreachable!(),
+            }
+        }
+        _ => {
+            executor.diagnostics.push(Report::ver_error_with_extra(
+                b.loc.clone(),
+                String::from("Can not apply arithmetic operation on these data ."),
+                reports,
+            ));
+            return Err(());
+        }
+    };
+    Ok(Z3Expression {
+        loc: b.loc.clone(),
+        element: res,
+    })
+}
+
+fn modulo<'ctx>(
+    left: &Expression,
+    right: &Expression,
+    loc: &Span,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
+    let e1 = transform_expr(left, ctx, executor)?;
+    let e2 = transform_expr(right, ctx, executor)?;
+
+    let mut reports = Vec::new();
+    let int1 = to_z3_int(&e1, &mut reports);
+    let int2 = to_z3_int(&e2, &mut reports);
+    match (int1, int2) {
+        (Ok(n1), Ok(n2)) => {
+            let res = n1 % n2;
+            Ok(Z3Expression::new(loc, &res))
+        }
+        _ => {
+            executor.diagnostics.push(Report::ver_error_with_extra(
+                loc.clone(),
+                String::from("Can not perform modulo operation."),
+                reports,
+            ));
+            Err(())
+        }
+    }
+}
+
+fn equality<'ctx>(
+    left: &Expression,
+    right: &Expression,
+    loc: &Span,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
+    let e1 = transform_expr(left, ctx, executor)?;
+    let e2 = transform_expr(right, ctx, executor)?;
+
+    let res = e1.element._safe_eq(&e2.element).map_err(|_| {
+        executor.diagnostics.push(Report::ver_error(
+            loc.clone(),
+            String::from("Sort mismatch."),
+        ))
+    })?;
+
+    Ok(Z3Expression::new(loc, &res))
+}
+
+fn inequality<'ctx>(
+    left: &Expression,
+    right: &Expression,
+    loc: &Span,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
+    let e1 = transform_expr(left, ctx, executor)?;
+    let e2 = transform_expr(right, ctx, executor)?;
+
+    let res = Dynamic::distinct(ctx, &[&e1.element, &e2.element]);
+
+    Ok(Z3Expression::new(loc, &res))
+}
+
+fn not<'ctx>(
+    e: &Expression,
+    loc: &Span,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
+    let v = transform_expr(e, ctx, executor)?;
+
+    let bool_v = to_z3_bool(&v, &mut executor.diagnostics)?;
+
+    Ok(Z3Expression::new(loc, &bool_v))
+}
+
+fn or<'ctx>(
+    left: &Expression,
+    right: &Expression,
+    loc: &Span,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
+    let e1 = transform_expr(left, ctx, executor)?;
+    let e2 = transform_expr(right, ctx, executor)?;
+
+    let mut reports = Vec::new();
+    let int1 = to_z3_bool(&e1, &mut reports);
+    let int2 = to_z3_bool(&e2, &mut reports);
+    match (int1, int2) {
+        (Ok(n1), Ok(n2)) => {
+            let res = Bool::or(ctx, &[n1, n2]);
+            Ok(Z3Expression::new(loc, &res))
+        }
+        _ => {
+            executor.diagnostics.push(Report::ver_error_with_extra(
+                loc.clone(),
+                String::from("Can not perform boolean OR."),
+                reports,
+            ));
+            Err(())
+        }
+    }
+}
+
+fn and<'ctx>(
+    left: &Expression,
+    right: &Expression,
+    loc: &Span,
+    ctx: &'ctx Context,
+    executor: &mut SymbolicExecutor,
+) -> Result<Z3Expression<'ctx>, ()> {
+    let e1 = transform_expr(left, ctx, executor)?;
+    let e2 = transform_expr(right, ctx, executor)?;
+
+    let mut reports = Vec::new();
+    let int1 = to_z3_bool(&e1, &mut reports);
+    let int2 = to_z3_bool(&e2, &mut reports);
+    match (int1, int2) {
+        (Ok(n1), Ok(n2)) => {
+            let res = Bool::and(ctx, &[n1, n2]);
+            Ok(Z3Expression::new(loc, &res))
+        }
+        _ => {
+            executor.diagnostics.push(Report::ver_error_with_extra(
+                loc.clone(),
+                String::from("Can not perform boolean AND."),
+                reports,
+            ));
+            Err(())
+        }
+    }
+}
+
 fn int<'ctx>(value: &BigInt, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> {
     let c = Int::from_big_int(ctx, value);
-    Z3Expression::Int(Z3UnaryExpression {
-        loc: loc.clone(),
-        element: c,
-    })
+    Z3Expression::new(loc, &c)
 }
 
 fn real<'ctx>(value: &BigRational, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> {
     let c = Real::from_big_rational(ctx, value);
-    Z3Expression::Real(Z3UnaryExpression {
-        loc: loc.clone(),
-        element: c,
-    })
+    Z3Expression::new(loc, &c)
 }
 
 fn bool<'ctx>(value: bool, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> {
     let c = Bool::from_bool(ctx, value);
-    Z3Expression::Boolean(Z3UnaryExpression {
-        loc: loc.clone(),
-        element: c,
-    })
+    Z3Expression::new(loc, &c)
 }
 
 fn string<'ctx>(value: &str, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> {
-    let c = String::from_str(ctx, value).unwrap_or(String::fresh_const(ctx, ""));
-    Z3Expression::String(Z3UnaryExpression {
-        loc: loc.clone(),
-        element: c,
-    })
+    let c = Z3String::from_str(ctx, value).unwrap_or(Z3String::fresh_const(ctx, ""));
+    Z3Expression::new(loc, &c)
 }
 
 fn char<'ctx>(value: char, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> {
     let c = Int::from_u64(ctx, value as u64);
-    Z3Expression::Int(Z3UnaryExpression {
-        loc: loc.clone(),
-        element: c,
-    })
+    Z3Expression::new(loc, &c)
 }
 
 fn enum_<'ctx>(value: usize, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> {
     let c = Int::from_u64(ctx, value as u64);
-    Z3Expression::Int(Z3UnaryExpression {
-        loc: loc.clone(),
-        element: c,
+    Z3Expression::new(loc, &c)
+}
+
+fn to_z3_int<'ctx>(
+    expr: &Z3Expression<'ctx>,
+    diagnostics: &mut Vec<Report>,
+) -> Result<Int<'ctx>, ()> {
+    expr.element.as_int().ok_or_else(|| {
+        diagnostics.push(Report::ver_error(
+            expr.loc.clone(),
+            String::from("Value can not be converted to integer."),
+        ));
+    })
+}
+
+fn to_z3_real<'ctx>(
+    expr: &Z3Expression<'ctx>,
+    diagnostics: &mut Vec<Report>,
+) -> Result<Real<'ctx>, ()> {
+    expr.element.as_real().ok_or_else(|| {
+        diagnostics.push(Report::ver_error(
+            expr.loc.clone(),
+            String::from("Value can not be converted to real."),
+        ));
+    })
+}
+
+fn to_z3_bool<'ctx>(
+    expr: &Z3Expression<'ctx>,
+    diagnostics: &mut Vec<Report>,
+) -> Result<Bool<'ctx>, ()> {
+    expr.element.as_bool().ok_or_else(|| {
+        diagnostics.push(Report::ver_error(
+            expr.loc.clone(),
+            String::from("Value can not be converted to boolean."),
+        ));
+    })
+}
+
+fn to_z3_string<'ctx>(
+    expr: &Z3Expression<'ctx>,
+    diagnostics: &mut Vec<Report>,
+) -> Result<Z3String<'ctx>, ()> {
+    expr.element.as_string().ok_or_else(|| {
+        diagnostics.push(Report::ver_error(
+            expr.loc.clone(),
+            String::from("Value can not be converted to string."),
+        ));
     })
 }