diff --git a/crates/verifier/src/ast.rs b/crates/verifier/src/ast.rs
index c08b235..5fe4a39 100644
--- a/crates/verifier/src/ast.rs
+++ b/crates/verifier/src/ast.rs
@@ -1,5 +1,3 @@
-use std::rc::Rc;
-
 use folidity_diagnostics::Report;
 use folidity_semantics::{
     ast::Expression,
diff --git a/crates/verifier/src/executor.rs b/crates/verifier/src/executor.rs
index b7a95a1..efd955d 100644
--- a/crates/verifier/src/executor.rs
+++ b/crates/verifier/src/executor.rs
@@ -1,5 +1,3 @@
-use std::rc::Rc;
-
 use folidity_diagnostics::Report;
 use folidity_semantics::{
     ContractDefinition,
@@ -7,34 +5,22 @@ use folidity_semantics::{
     SymbolInfo,
 };
 use z3::{
-    ast::{
-        Ast,
-        Dynamic,
-    },
+    ast::Dynamic,
     Context,
     Solver,
     Sort,
 };
 
-use crate::{
-    ast::{
-        Constraint,
-        Declaration,
-        Z3Expression,
-    },
-    transformer::transform_expr,
-    z3_cfg,
+use crate::ast::{
+    Constraint,
+    Declaration,
 };
-
-//
-
 #[derive(Debug)]
 pub struct SymbolicExecutor<'ctx> {
     /// Global solver of the executor.
     ///
     /// We encapsulate it as it can't be easily transferred between scopes.
-    solver: Solver<'ctx>,
-    pub local_contexts: Vec<Context>,
+    context: &'ctx Context,
     /// List of resolved declaration to verify.
     pub declarations: Vec<Declaration<'ctx>>,
     /// Symbol counter to track boolean constants across the program.
@@ -45,28 +31,22 @@ pub struct SymbolicExecutor<'ctx> {
 impl<'ctx> SymbolicExecutor<'ctx> {
     pub fn new(context: &'ctx Context) -> Self {
         Self {
-            solver: Solver::new(context),
-            local_contexts: vec![],
+            context,
             declarations: vec![],
             diagnostics: vec![],
             symbol_counter: 0,
         }
     }
 
-    pub fn parse_declarations(
-        &mut self,
-        contract: &ContractDefinition,
-        context: &'ctx Context,
-    ) -> Result<(), ()> {
+    /// Resolve Model, State and Function bounds into declarations with constraints.
+    pub fn resolve_declarations(&mut self, contract: &ContractDefinition) -> Result<(), ()> {
         let mut error = false;
         let mut diagnostics = Vec::new();
-
-        for i in 0..contract.models.len() {
+        (0..contract.models.len()).for_each(|i| {
             let mut constraints: Vec<Constraint> = vec![];
             let m = &contract.models[i];
-
             for e in &m.bounds {
-                match Constraint::from_expr(e, context, &mut diagnostics, self) {
+                match Constraint::from_expr(e, self.context, &mut diagnostics, self) {
                     Ok(c) => constraints.push(c),
                     Err(_) => {
                         error = true;
@@ -74,7 +54,6 @@ impl<'ctx> SymbolicExecutor<'ctx> {
                     }
                 };
             }
-
             let decl = Declaration {
                 constraints,
                 decl_sym: GlobalSymbol::Model(SymbolInfo {
@@ -85,7 +64,65 @@ impl<'ctx> SymbolicExecutor<'ctx> {
             };
 
             self.declarations.push(decl);
-        }
+        });
+
+        (0..contract.states.len()).for_each(|i| {
+            let mut constraints: Vec<Constraint> = vec![];
+            let s = &contract.states[i];
+            for e in &s.bounds {
+                match Constraint::from_expr(e, self.context, &mut diagnostics, self) {
+                    Ok(c) => constraints.push(c),
+                    Err(_) => {
+                        error = true;
+                        continue;
+                    }
+                };
+            }
+            let decl = Declaration {
+                constraints,
+                decl_sym: GlobalSymbol::State(SymbolInfo {
+                    loc: s.loc.clone(),
+                    i,
+                }),
+                parent: s.from.clone().map(|x| x.0),
+            };
+
+            self.declarations.push(decl);
+        });
+
+        (0..contract.functions.len()).for_each(|i| {
+            let mut constraints: Vec<Constraint> = vec![];
+            let f = &contract.functions[i];
+            for e in &f.bounds {
+                match Constraint::from_expr(e, self.context, &mut diagnostics, self) {
+                    Ok(c) => constraints.push(c),
+                    Err(_) => {
+                        error = true;
+                        continue;
+                    }
+                };
+            }
+
+            let parent_bound = match f.state_bound.clone() {
+                Some(b) => {
+                    match b.from {
+                        Some(f) => Some(f.ty),
+                        None => None,
+                    }
+                }
+                None => None,
+            };
+            let decl = Declaration {
+                constraints,
+                decl_sym: GlobalSymbol::Model(SymbolInfo {
+                    loc: f.loc.clone(),
+                    i,
+                }),
+                parent: parent_bound,
+            };
+
+            self.declarations.push(decl);
+        });
 
         if error {
             return Err(());
@@ -101,13 +138,17 @@ impl<'ctx> SymbolicExecutor<'ctx> {
         context: &'a Context,
     ) -> (Dynamic<'a>, u32) {
         let id = self.symbol_counter;
-        let c = Dynamic::new_const(&context, id, sort);
+        let c = Dynamic::new_const(context, id, sort);
         self.symbol_counter += 1;
         (c, id)
     }
 
     /// Retrieve the context of the internal `solver`.
     pub fn context(&self) -> &Context {
-        self.solver.get_context()
+        self.context
+    }
+
+    pub fn transfer_context(&mut self, solver: Solver<'_>) -> Solver<'_> {
+        solver.translate(self.context)
     }
 }
diff --git a/crates/verifier/src/lib.rs b/crates/verifier/src/lib.rs
index 111c6e0..af7a9f1 100644
--- a/crates/verifier/src/lib.rs
+++ b/crates/verifier/src/lib.rs
@@ -1,5 +1,6 @@
 use executor::SymbolicExecutor;
 use folidity_semantics::{
+    CompilationError,
     ContractDefinition,
     Runner,
 };
@@ -25,12 +26,17 @@ pub fn z3_cfg() -> Config {
 }
 
 impl<'ctx> Runner<ContractDefinition, ()> for SymbolicExecutor<'ctx> {
-    fn run(source: &ContractDefinition) -> Result<(), folidity_semantics::CompilationError>
+    fn run(source: &ContractDefinition) -> Result<(), CompilationError>
     where
         Self: std::marker::Sized,
     {
         let context = Context::new(&z3_cfg());
-        let executor = SymbolicExecutor::new(&context);
+
+        let mut executor = SymbolicExecutor::new(&context);
+
+        if executor.resolve_declarations(source).is_err() {
+            return Err(CompilationError::Formal(executor.diagnostics));
+        }
 
         Ok(())
     }