diff --git a/crates/clarirs_core/src/algorithms/simplify.rs b/crates/clarirs_core/src/algorithms/simplify.rs
index 2bf5c84..d9301ea 100644
--- a/crates/clarirs_core/src/algorithms/simplify.rs
+++ b/crates/clarirs_core/src/algorithms/simplify.rs
@@ -69,6 +69,7 @@ impl<'c> Simplify<'c> for BitVecAst<'c> {
                 BitVecOp::And(arc, arc1) => todo!(),
                 BitVecOp::Or(arc, arc1) => todo!(),
                 BitVecOp::Xor(arc, arc1) => todo!(),
+                BitVecOp::Abs(arc) => todo!(),
                 BitVecOp::Add(arc, arc1) => todo!(),
                 BitVecOp::Sub(arc, arc1) => todo!(),
                 BitVecOp::Mul(arc, arc1) => todo!(),
diff --git a/crates/clarirs_core/src/ast/bitvec.rs b/crates/clarirs_core/src/ast/bitvec.rs
index a77a42c..ef58b10 100644
--- a/crates/clarirs_core/src/ast/bitvec.rs
+++ b/crates/clarirs_core/src/ast/bitvec.rs
@@ -14,6 +14,7 @@ pub enum BitVecOp<'c> {
     And(BitVecAst<'c>, BitVecAst<'c>),
     Or(BitVecAst<'c>, BitVecAst<'c>),
     Xor(BitVecAst<'c>, BitVecAst<'c>),
+    Abs(BitVecAst<'c>),
     Add(BitVecAst<'c>, BitVecAst<'c>),
     Sub(BitVecAst<'c>, BitVecAst<'c>),
     Mul(BitVecAst<'c>, BitVecAst<'c>),
@@ -50,6 +51,7 @@ impl<'c> Op<'c> for BitVecOp<'c> {
             BitVecOp::BVS(..) | BitVecOp::BVV(..) | BitVecOp::SI(..) => vec![],
 
             BitVecOp::Not(a)
+            | BitVecOp::Abs(a)
             | BitVecOp::Reverse(a)
             | BitVecOp::ZeroExt(a, _)
             | BitVecOp::SignExt(a, _)
diff --git a/crates/clarirs_core/src/ast/factory.rs b/crates/clarirs_core/src/ast/factory.rs
index f835a6e..d2c4474 100644
--- a/crates/clarirs_core/src/ast/factory.rs
+++ b/crates/clarirs_core/src/ast/factory.rs
@@ -96,6 +96,13 @@ pub trait AstFactory<'c>: Sized {
         Op::neq(self, lhs, rhs)
     }
 
+    fn abs<Op: SupportsAbs<'c>>(
+        &'c self,
+        ast: &AstRef<'c, Op>,
+    ) -> Result<AstRef<'c, Op>, ClarirsError> {
+        Op::abs(self, ast)
+    }
+
     fn add<Op: SupportsAdd<'c>>(
         &'c self,
         lhs: &AstRef<'c, Op>,
diff --git a/crates/clarirs_core/src/ast/factory_support.rs b/crates/clarirs_core/src/ast/factory_support.rs
index d0ebf9a..cc290f1 100644
--- a/crates/clarirs_core/src/ast/factory_support.rs
+++ b/crates/clarirs_core/src/ast/factory_support.rs
@@ -21,6 +21,7 @@ macro_rules! uniop_support_trait {
 }
 
 uniop_support_trait!(Not, BooleanOp<'c>, make_bool, BitVecOp<'c>, make_bitvec);
+uniop_support_trait!(Abs, BitVecOp<'c>, make_bitvec);
 
 macro_rules! binop_support_trait {
     ($name:ident, $($impler:ty, $factory_func:ident),*) => {
diff --git a/crates/clarirs_py/src/ast/args.rs b/crates/clarirs_py/src/ast/args.rs
index 5086866..f47722f 100644
--- a/crates/clarirs_py/src/ast/args.rs
+++ b/crates/clarirs_py/src/ast/args.rs
@@ -68,7 +68,7 @@ impl ExtractPyArgs for BitVecOp<'static> {
             BitVecOp::BVS(name, size) => vec![name.to_object(py), size.to_object(py)],
             BitVecOp::BVV(bit_vec) => vec![bit_vec.as_biguint().to_object(py)],
             BitVecOp::SI(_, bit_vec, bit_vec1, bit_vec2, _) => todo!(),
-            BitVecOp::Not(expr) => vec![BV::new(py, expr)?.into_any()],
+            BitVecOp::Not(expr) | BitVecOp::Abs(expr) => vec![BV::new(py, expr)?.into_any()],
             BitVecOp::And(lhs, rhs)
             | BitVecOp::Or(lhs, rhs)
             | BitVecOp::Xor(lhs, rhs)
diff --git a/crates/clarirs_py/src/ast/bool.rs b/crates/clarirs_py/src/ast/bool.rs
index 3591b10..d19d517 100644
--- a/crates/clarirs_py/src/ast/bool.rs
+++ b/crates/clarirs_py/src/ast/bool.rs
@@ -86,12 +86,37 @@ impl Bool {
         self.inner.depth() == 1
     }
 
-    fn is_true(self_: PyRef<Self>) -> bool {
-        self_.inner.is_true()
+    fn is_true(&self) -> bool {
+        self.inner.is_true()
     }
 
-    fn is_false(self_: PyRef<Self>) -> bool {
-        self_.inner.is_false()
+    fn is_false(&self) -> bool {
+        self.inner.is_false()
+    }
+
+    fn __invert__(&self, py: Python) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(py, &GLOBAL_CONTEXT.not(&self.inner)?)
+    }
+
+    fn __and__(&self, py: Python, other: CoerceBool) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.and(&self.inner, &<CoerceBool as Into<BoolAst>>::into(other))?,
+        )
+    }
+
+    fn __or__(&self, py: Python, other: CoerceBool) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.or(&self.inner, &<CoerceBool as Into<BoolAst>>::into(other))?,
+        )
+    }
+
+    fn __xor__(&self, py: Python, other: CoerceBool) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.xor(&self.inner, &<CoerceBool as Into<BoolAst>>::into(other))?,
+        )
     }
 }
 
@@ -99,12 +124,13 @@ impl Bool {
 pub fn BoolS(py: Python, name: &str) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(py, &GLOBAL_CONTEXT.bools(name)?)
 }
+
 #[pyfunction]
 pub fn BoolV(py: Python, value: bool) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(py, &GLOBAL_CONTEXT.boolv(value)?)
 }
 
-#[pyfunction]
+#[pyfunction(name = "Eq")]
 pub fn Eq_(py: Python, a: Bound<Bool>, b: Bound<Bool>) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(py, &GLOBAL_CONTEXT.eq_(&a.get().inner, &b.get().inner)?)
 }
@@ -114,19 +140,6 @@ pub fn Neq(py: Python, a: Bound<Bool>, b: Bound<Bool>) -> Result<Py<Bool>, Clari
     Bool::new(py, &GLOBAL_CONTEXT.neq(&a.get().inner, &b.get().inner)?)
 }
 
-#[pyfunction]
-pub fn If(
-    py: Python,
-    cond: Bound<Bool>,
-    then_: Bound<Bool>,
-    else_: Bound<Bool>,
-) -> Result<Py<Bool>, ClaripyError> {
-    Bool::new(
-        py,
-        &GLOBAL_CONTEXT.if_(&cond.get().inner, &then_.get().inner, &else_.get().inner)?,
-    )
-}
-
 #[pyfunction(name = "true")]
 pub fn true_op(py: Python) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(py, &GLOBAL_CONTEXT.true_()?)
@@ -139,7 +152,19 @@ pub fn false_op(py: Python) -> Result<Py<Bool>, ClaripyError> {
 pub(crate) fn import(_: Python, m: &Bound<PyModule>) -> PyResult<()> {
     m.add_class::<Bool>()?;
 
-    add_pyfunctions!(m, BoolS, BoolV, Not, And, Or, Xor, Eq_, If, true_op, false_op,);
+    add_pyfunctions!(
+        m,
+        BoolS,
+        BoolV,
+        Not,
+        And,
+        Or,
+        Xor,
+        Eq_,
+        super::If,
+        true_op,
+        false_op,
+    );
 
     Ok(())
 }
diff --git a/crates/clarirs_py/src/ast/bv.rs b/crates/clarirs_py/src/ast/bv.rs
index c650aff..391000b 100644
--- a/crates/clarirs_py/src/ast/bv.rs
+++ b/crates/clarirs_py/src/ast/bv.rs
@@ -86,6 +86,316 @@ impl BV {
     fn is_leaf(&self) -> bool {
         self.inner.depth() == 1
     }
+
+    fn __add__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.add(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __radd__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__add__(py, other)
+    }
+
+    fn __sub__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.sub(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rsub__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__sub__(py, other)
+    }
+
+    fn __mul__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.mul(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rmul__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__mul__(py, other)
+    }
+
+    fn __truediv__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.udiv(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rtruediv__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__truediv__(py, other)
+    }
+
+    fn __floordiv__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.udiv(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rfloordiv__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__floordiv__(py, other)
+    }
+
+    fn __pow__(
+        &self,
+        py: Python,
+        other: CoerceBV,
+        _modulo: PyObject,
+    ) -> Result<Py<BV>, ClaripyError> {
+        // TODO: handle modulo
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.pow(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rpow__(
+        &self,
+        py: Python,
+        other: CoerceBV,
+        _modulo: PyObject,
+    ) -> Result<Py<BV>, ClaripyError> {
+        self.__pow__(py, other, _modulo)
+    }
+
+    fn __mod__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.urem(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rmod__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__mod__(py, other)
+    }
+
+    fn SDiv(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.sdiv(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn SMod(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.srem(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __and__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.and(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rand__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__and__(py, other)
+    }
+
+    fn __or__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.or(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __ror__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__or__(py, other)
+    }
+
+    fn __xor__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.xor(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rxor__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__xor__(py, other)
+    }
+
+    fn __lshift__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.shl(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rlshift__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__lshift__(py, other)
+    }
+
+    fn __rshift__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.ashr(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __rrshift__(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        self.__rshift__(py, other)
+    }
+
+    fn LShR(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.lshr(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __neg__(&self, py: Python) -> Result<Py<BV>, ClaripyError> {
+        BV::new(py, &GLOBAL_CONTEXT.not(&self.inner)?)
+    }
+
+    fn __invert__(&self, py: Python) -> Result<Py<BV>, ClaripyError> {
+        BV::new(py, &GLOBAL_CONTEXT.not(&self.inner)?)
+    }
+
+    fn __pos__(self_: Py<BV>) -> Result<Py<BV>, ClaripyError> {
+        Ok(self_)
+    }
+
+    fn __abs__(&self, py: Python) -> Result<Py<BV>, ClaripyError> {
+        BV::new(py, &GLOBAL_CONTEXT.abs(&self.inner)?)
+    }
+
+    fn __eq__(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.eq_(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __ne__(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.neq(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __lt__(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.ult(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __le__(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.ule(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __gt__(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.ugt(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn __ge__(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.uge(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn ULT(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.ult(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn ULE(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.ule(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn UGT(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.ugt(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn UGE(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.uge(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn SLT(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.slt(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn SLE(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.sle(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn SGT(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.sgt(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn SGE(&self, py: Python, other: CoerceBV) -> Result<Py<Bool>, ClaripyError> {
+        Bool::new(
+            py,
+            &GLOBAL_CONTEXT.sge(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn Extract(
+        &self,
+        py: Python,
+        upper_bound: u32,
+        lower_bound: u32,
+    ) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.extract(&self.inner, upper_bound, lower_bound)?,
+        )
+    }
+
+    fn concat(&self, py: Python, other: CoerceBV) -> Result<Py<BV>, ClaripyError> {
+        BV::new(
+            py,
+            &GLOBAL_CONTEXT.concat(&self.inner, &<CoerceBV as Into<BitVecAst>>::into(other))?,
+        )
+    }
+
+    fn zero_ext(&self, py: Python, amount: u32) -> Result<Py<BV>, ClaripyError> {
+        BV::new(py, &GLOBAL_CONTEXT.zero_ext(&self.inner, amount)?)
+    }
+
+    fn sign_ext(&self, py: Python, amount: u32) -> Result<Py<BV>, ClaripyError> {
+        BV::new(py, &GLOBAL_CONTEXT.sign_ext(&self.inner, amount)?)
+    }
+
+    #[getter]
+    fn reversed(&self, py: Python) -> Result<Py<BV>, ClaripyError> {
+        BV::new(py, &GLOBAL_CONTEXT.reverse(&self.inner)?)
+    }
 }
 
 #[pyfunction]
diff --git a/crates/clarirs_py/src/ast/coerce.rs b/crates/clarirs_py/src/ast/coerce.rs
new file mode 100644
index 0000000..7dd97f4
--- /dev/null
+++ b/crates/clarirs_py/src/ast/coerce.rs
@@ -0,0 +1,115 @@
+use std::str;
+
+use crate::prelude::*;
+
+pub struct CoerceBool(pub Py<Bool>);
+
+impl FromPyObject<'_> for CoerceBool {
+    fn extract_bound(val: &Bound<PyAny>) -> PyResult<Self> {
+        if let Ok(bool_val) = val.downcast::<Bool>() {
+            Ok(CoerceBool(bool_val.clone().unbind()))
+        } else if let Ok(bool_val) = val.extract::<bool>() {
+            Ok(CoerceBool(
+                Bool::new(val.py(), &GLOBAL_CONTEXT.boolv(bool_val).unwrap()).unwrap(),
+            ))
+        } else {
+            Err(ClaripyError::InvalidArgumentType("Expected Bool".to_string()).into())
+        }
+    }
+}
+
+impl From<CoerceBool> for Py<Bool> {
+    fn from(val: CoerceBool) -> Self {
+        val.0
+    }
+}
+
+impl From<CoerceBool> for BoolAst<'static> {
+    fn from(val: CoerceBool) -> Self {
+        val.0.get().inner.clone()
+    }
+}
+
+pub struct CoerceBV(pub Py<BV>);
+
+impl FromPyObject<'_> for CoerceBV {
+    fn extract_bound(val: &Bound<'_, PyAny>) -> PyResult<Self> {
+        if let Ok(bv_val) = val.downcast::<BV>() {
+            Ok(CoerceBV(bv_val.clone().unbind()))
+        } else if let Ok(bv_val) = val.extract::<u64>() {
+            Ok(CoerceBV(
+                BV::new(val.py(), &GLOBAL_CONTEXT.bvv_prim(bv_val).unwrap()).unwrap(),
+            ))
+        } else {
+            Err(ClaripyError::InvalidArgumentType("Expected BV".to_string()).into())
+        }
+    }
+}
+
+impl From<CoerceBV> for Py<BV> {
+    fn from(val: CoerceBV) -> Self {
+        val.0
+    }
+}
+
+impl From<CoerceBV> for BitVecAst<'static> {
+    fn from(val: CoerceBV) -> Self {
+        val.0.get().inner.clone()
+    }
+}
+
+pub struct CoerceFP(pub Py<FP>);
+
+impl FromPyObject<'_> for CoerceFP {
+    fn extract_bound(val: &Bound<'_, PyAny>) -> PyResult<Self> {
+        if let Ok(fp_val) = val.downcast::<FP>() {
+            Ok(CoerceFP(fp_val.clone().unbind()))
+        } else if let Ok(fp_val) = val.extract::<f64>() {
+            Ok(CoerceFP(
+                FP::new(val.py(), &GLOBAL_CONTEXT.fpv(fp_val).unwrap()).unwrap(),
+            ))
+        } else {
+            Err(ClaripyError::InvalidArgumentType("Expected FP".to_string()).into())
+        }
+    }
+}
+
+impl From<CoerceFP> for Py<FP> {
+    fn from(val: CoerceFP) -> Self {
+        val.0
+    }
+}
+
+impl From<CoerceFP> for FloatAst<'static> {
+    fn from(val: CoerceFP) -> Self {
+        val.0.get().inner.clone()
+    }
+}
+
+pub struct CoerceString(pub Py<PyAstString>);
+
+impl FromPyObject<'_> for CoerceString {
+    fn extract_bound(val: &Bound<'_, PyAny>) -> PyResult<Self> {
+        if let Ok(string_val) = val.downcast::<PyAstString>() {
+            Ok(CoerceString(string_val.clone().unbind()))
+        } else if let Ok(string_val) = val.extract::<&str>() {
+            Ok(CoerceString(
+                PyAstString::new(val.py(), &GLOBAL_CONTEXT.stringv(string_val).unwrap()).unwrap(),
+            ))
+        } else {
+            Err(ClaripyError::InvalidArgumentType("Expected String".to_string()).into())
+        }
+    }
+}
+
+impl From<CoerceString> for Py<PyAstString> {
+    fn from(val: CoerceString) -> Self {
+        val.0
+    }
+}
+
+impl From<CoerceString> for StringAst<'static> {
+    fn from(val: CoerceString) -> Self {
+        val.0.get().inner.clone()
+    }
+}
diff --git a/crates/clarirs_py/src/ast/mod.rs b/crates/clarirs_py/src/ast/mod.rs
index 8620223..68c5525 100644
--- a/crates/clarirs_py/src/ast/mod.rs
+++ b/crates/clarirs_py/src/ast/mod.rs
@@ -3,6 +3,7 @@ pub mod base;
 pub mod bits;
 pub mod bool;
 pub mod bv;
+pub mod coerce;
 pub mod fp;
 pub mod opstring;
 pub mod string;
diff --git a/crates/clarirs_py/src/ast/opstring.rs b/crates/clarirs_py/src/ast/opstring.rs
index f718aa6..7f2eec7 100644
--- a/crates/clarirs_py/src/ast/opstring.rs
+++ b/crates/clarirs_py/src/ast/opstring.rs
@@ -55,6 +55,7 @@ impl ToOpString for BitVecOp<'static> {
             BitVecOp::And(..) => "__and__".to_string(),
             BitVecOp::Or(..) => "__or__".to_string(),
             BitVecOp::Xor(..) => "__xor__".to_string(),
+            BitVecOp::Abs(..) => "__abs__".to_string(),
             BitVecOp::Add(..) => "__add__".to_string(),
             BitVecOp::Sub(..) => "__sub__".to_string(),
             BitVecOp::Mul(..) => "__mul__".to_string(),
diff --git a/crates/clarirs_py/src/error.rs b/crates/clarirs_py/src/error.rs
index 082f118..0e3b19c 100644
--- a/crates/clarirs_py/src/error.rs
+++ b/crates/clarirs_py/src/error.rs
@@ -1,5 +1,5 @@
 use crate::prelude::*;
-use pyo3::{exceptions::PyRuntimeError, PyErr, PyObject};
+use pyo3::{exceptions::PyRuntimeError, DowncastError, DowncastIntoError, PyErr, PyObject};
 use thiserror::Error;
 
 #[derive(Debug, Error)]
@@ -14,6 +14,10 @@ pub enum ClaripyError {
     FailedToExtractArg(PyObject),
     #[error("Python error: {0}")]
     PythonError(String),
+    #[error("Casting error: {0}")]
+    CastingError(String),
+    #[error("Invalid argument type: {0}")]
+    InvalidArgumentType(String),
 }
 
 impl From<ClarirsError> for ClaripyError {
@@ -39,3 +43,15 @@ impl From<ClaripyError> for PyErr {
         PyRuntimeError::new_err(format!("{}", e))
     }
 }
+
+impl From<DowncastError<'_, '_>> for ClaripyError {
+    fn from(e: DowncastError) -> Self {
+        ClaripyError::CastingError(format!("{}", e))
+    }
+}
+
+impl From<DowncastIntoError<'_>> for ClaripyError {
+    fn from(e: DowncastIntoError) -> Self {
+        ClaripyError::CastingError(format!("{}", e))
+    }
+}
diff --git a/crates/clarirs_py/src/prelude.rs b/crates/clarirs_py/src/prelude.rs
index 1f2bc14..bb1e2ef 100644
--- a/crates/clarirs_py/src/prelude.rs
+++ b/crates/clarirs_py/src/prelude.rs
@@ -1,7 +1,15 @@
 pub use crate::ast;
 pub use crate::ast::{
-    args::ExtractPyArgs, base::Base, bits::Bits, bool::Bool, bv::BV, fp::FP, opstring::ToOpString,
-    string::PyAstString, GLOBAL_CONTEXT,
+    args::ExtractPyArgs,
+    base::Base,
+    bits::Bits,
+    bool::Bool,
+    bv::BV,
+    coerce::{CoerceBV, CoerceBool, CoerceFP, CoerceString},
+    fp::FP,
+    opstring::ToOpString,
+    string::PyAstString,
+    GLOBAL_CONTEXT,
 };
 pub use crate::error::ClaripyError;
 pub use clarirs_core::prelude::*;