diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c19b4fe..ed360e8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -67,7 +67,7 @@ jobs:
         build: [msrv, debug, release]
         include:
           - build: msrv
-            rust: 1.70.0 # MSRV
+            rust: 1.75.0 # MSRV
             target: x86_64-unknown-linux-gnu
             features: full
           - build: debug
@@ -143,7 +143,7 @@ jobs:
       - name: Install Rust
         uses: dtolnay/rust-toolchain@stable
         with:
-          toolchain: 1.70.0 # MSRV
+          toolchain: 1.75.0 # MSRV
           components: clippy
       - uses: Swatinem/rust-cache@v2
       - name: Lint
diff --git a/Cargo.lock b/Cargo.lock
index 907a484..9d11109 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -26,17 +26,6 @@ dependencies = [
  "memchr",
 ]
 
-[[package]]
-name = "async-trait"
-version = "0.1.74"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a66537f1bb974b254c98ed142ff995236e81b9d0fe4db0575f46612cb15eb0f9"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn",
-]
-
 [[package]]
 name = "autocfg"
 version = "1.1.0"
@@ -736,7 +725,6 @@ dependencies = [
 name = "smtlib-lowlevel"
 version = "0.1.8"
 dependencies = [
- "async-trait",
  "insta",
  "itertools",
  "logos",
diff --git a/README.md b/README.md
index 86cb52d..aa0f736 100644
--- a/README.md
+++ b/README.md
@@ -20,10 +20,10 @@ Thus the goal of `smtlib` (and [`smtlib-lowlevel`](https://crates.io/crates/smtl
 
 ## Usage
 
-The primary way to use `smtlib` is by constructing a [`smtlib::Solver`](https://docs.rs/smtlib/latest/smtlib/struct.Solver.html). A solver takes as argument a [`smtlib::Backend`](https://docs.rs/smtlib/latest/smtlib/trait.Backend.html). To see which backends are provided with the library check out the [`smtlib::backend`](https://docs.rs/smtlib/latest/smtlib/backend/index.html) module. Each backend is behind a feature flag, so for example to use the [Z3](https://github.com/Z3Prover/z3) binary backend install `smtlib` by running
+The primary way to use `smtlib` is by constructing a [`smtlib::Solver`](https://docs.rs/smtlib/latest/smtlib/struct.Solver.html). A solver takes as argument a [`smtlib::Backend`](https://docs.rs/smtlib/latest/smtlib/trait.Backend.html). To see which backends are provided with the library check out the [`smtlib::backend`](https://docs.rs/smtlib/latest/smtlib/backend/index.html) module. Some backend is behind a feature flag, so for example to use the [Z3](https://github.com/Z3Prover/z3) statically backend install `smtlib` by running `cargo add smtlib -F z3-static`, but otherwise add it by running:
 
 ```bash
-cargo add smtlib --features z3
+cargo add smtlib
 ```
 
 Now you can go ahead and use the library in your project.
diff --git a/lowlevel/Cargo.toml b/lowlevel/Cargo.toml
index cb90256..7182aaa 100644
--- a/lowlevel/Cargo.toml
+++ b/lowlevel/Cargo.toml
@@ -12,14 +12,10 @@ documentation = "https://docs.rs/smtlib-lowlevel"
 
 [features]
 default = []
-z3 = []
 z3-static = ["dep:z3-sys"]
-cvc5 = []
 serde = ["dep:serde"]
-async = ["dep:async-trait"]
 
 [dependencies]
-async-trait = { version = "0.1.74", optional = true }
 itertools.workspace = true
 logos = "0.13.0"
 miette.workspace = true
@@ -35,4 +31,4 @@ smtlib-lowlevel = { path = ".", features = ["serde"] }
 smtlib-build-util = { version = "0.1.8", path = "../build-util" }
 
 [package.metadata.docs.rs]
-features = ["z3", "cvc5", "serde", "async"]
+features = ["serde"]
diff --git a/lowlevel/src/backend/cvc5.rs b/lowlevel/src/backend/cvc5.rs
index f8a6fd1..5924668 100644
--- a/lowlevel/src/backend/cvc5.rs
+++ b/lowlevel/src/backend/cvc5.rs
@@ -1,4 +1,4 @@
-use std::ffi::OsStr;
+use std::{ffi::OsStr, future::Future};
 
 use super::{Backend, BinaryBackend};
 
@@ -24,10 +24,11 @@ impl Backend for Cvc5Binary {
     }
 }
 
-#[cfg(feature = "async")]
-#[async_trait::async_trait(?Send)]
 impl super::AsyncBackend for Cvc5Binary {
-    async fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error> {
-        self.bin.exec(cmd).map(Into::into)
+    fn exec_async(
+        &mut self,
+        cmd: &crate::Command,
+    ) -> impl Future<Output = Result<String, crate::Error>> {
+        async { self.bin.exec(cmd).map(Into::into) }
     }
 }
diff --git a/lowlevel/src/backend/mod.rs b/lowlevel/src/backend/mod.rs
index 54e7f8a..628aa84 100644
--- a/lowlevel/src/backend/mod.rs
+++ b/lowlevel/src/backend/mod.rs
@@ -8,26 +8,21 @@
 //! ## Backends
 //!
 //! - **[`Z3Binary`]**: A [Z3](https://github.com/Z3Prover/z3) backend using the binary CLI interface.
-//!     - **Enabled by feature:** `z3`
 //! - **[`Z3Static`]**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys` crate](https://github.com/prove-rs/z3.rs).
 //!     - **Enabled by feature:** `z3-static`
 //! - **[`Cvc5Binary`]**: A [cvc5](https://cvc5.github.io/) backend using the binary CLI interface.
-//!     - **Enabled by feature:** `cvc5`
 
 use std::{
+    future::Future,
     io::{BufRead, BufReader, Write},
     process::{Child, ChildStdin, ChildStdout},
 };
 
-#[cfg(feature = "cvc5")]
 mod cvc5;
-#[cfg(feature = "cvc5")]
 pub use cvc5::*;
 
-#[cfg(feature = "z3")]
 mod z3_binary;
 use logos::Lexer;
-#[cfg(feature = "z3")]
 pub use z3_binary::*;
 
 #[cfg(feature = "z3-static")]
@@ -44,13 +39,14 @@ pub trait Backend {
     fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error>;
 }
 
-#[cfg(feature = "async")]
 /// The [`AsyncBackend`] trait is used to interact with SMT solver using the SMT-LIB language.
 ///
 /// For more details read the [`backend`](crate::backend) module documentation.
-#[async_trait::async_trait(?Send)]
 pub trait AsyncBackend {
-    async fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error>;
+    fn exec_async(
+        &mut self,
+        cmd: &crate::Command,
+    ) -> impl Future<Output = Result<String, crate::Error>>;
 }
 
 struct BinaryBackend {
diff --git a/lowlevel/src/backend/z3_binary.rs b/lowlevel/src/backend/z3_binary.rs
index 9f2ce83..472c21f 100644
--- a/lowlevel/src/backend/z3_binary.rs
+++ b/lowlevel/src/backend/z3_binary.rs
@@ -1,4 +1,4 @@
-use std::ffi::OsStr;
+use std::{ffi::OsStr, future::Future};
 
 use super::{Backend, BinaryBackend};
 
@@ -22,10 +22,11 @@ impl Backend for Z3Binary {
     }
 }
 
-#[cfg(feature = "async")]
-#[async_trait::async_trait(?Send)]
 impl super::AsyncBackend for Z3Binary {
-    async fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error> {
-        self.bin.exec(cmd).map(Into::into)
+    fn exec_async(
+        &mut self,
+        cmd: &crate::Command,
+    ) -> impl Future<Output = Result<String, crate::Error>> {
+        async { self.bin.exec(cmd).map(Into::into) }
     }
 }
diff --git a/lowlevel/src/lib.rs b/lowlevel/src/lib.rs
index f068012..89290bb 100644
--- a/lowlevel/src/lib.rs
+++ b/lowlevel/src/lib.rs
@@ -1,4 +1,5 @@
 #![deny(rustdoc::broken_intra_doc_links)]
+#![allow(clippy::manual_async_fn)]
 
 //! # smtlib-lowlevel
 //!
@@ -7,9 +8,7 @@
 use std::collections::HashSet;
 
 use ast::{QualIdentifier, Term};
-#[cfg(feature = "async")]
-use backend::AsyncBackend;
-use backend::Backend;
+use backend::{AsyncBackend, Backend};
 use parse::ParseError;
 
 use crate::ast::{Command, GeneralResponse};
@@ -62,13 +61,11 @@ where
     }
 }
 
-#[cfg(feature = "async")]
 #[derive(Debug)]
 pub struct AsyncDriver<B> {
     backend: B,
 }
 
-#[cfg(feature = "async")]
 impl<B> AsyncDriver<B>
 where
     B: AsyncBackend,
@@ -84,7 +81,7 @@ where
     }
     pub async fn exec(&mut self, cmd: &Command) -> Result<GeneralResponse, Error> {
         // println!("> {cmd}");
-        let res = self.backend.exec(cmd).await?;
+        let res = self.backend.exec_async(cmd).await?;
         let res = if let Some(res) = cmd.parse_response(&res)? {
             GeneralResponse::SpecificSuccessResponse(res)
         } else {
diff --git a/lowlevel/src/tests.rs b/lowlevel/src/tests.rs
index c2a14c7..01ffc97 100644
--- a/lowlevel/src/tests.rs
+++ b/lowlevel/src/tests.rs
@@ -12,7 +12,6 @@ fn bubble_sort() {
     insta::assert_ron_snapshot!(Script::parse(include_str!("../examples/bubble_sort.smt2")));
 }
 
-#[cfg(feature = "z3")]
 mod z3 {
     use crate::{ast::Command, backend::Z3Binary, Driver};
 
diff --git a/smtlib/Cargo.toml b/smtlib/Cargo.toml
index b91dde7..1a5d8d7 100644
--- a/smtlib/Cargo.toml
+++ b/smtlib/Cargo.toml
@@ -13,11 +13,8 @@ documentation = "https://docs.rs/smtlib"
 [features]
 default = []
 serde = ["dep:serde", "smtlib-lowlevel/serde"]
-z3 = ["smtlib-lowlevel/z3"]
 z3-static = ["smtlib-lowlevel/z3-static"]
-cvc5 = ["smtlib-lowlevel/cvc5"]
 const-bit-vec = []
-async = ["smtlib-lowlevel/async"]
 
 [dependencies]
 itertools.workspace = true
@@ -30,11 +27,11 @@ thiserror.workspace = true
 futures = "0.3.29"
 insta.workspace = true
 miette = { workspace = true, features = ["fancy"] }
-smtlib = { path = ".", features = ["serde", "z3", "cvc5", "async"] }
+smtlib = { path = ".", features = ["serde"] }
 
 [build-dependencies]
 smtlib-build-util = { version = "0.1.8", path = "../build-util" }
 smtlib-lowlevel = { version = "0.1.8", path = "../lowlevel" }
 
 [package.metadata.docs.rs]
-features = ["serde", "z3", "cvc5", "const-bit-vec", "async"]
+features = ["serde", "const-bit-vec"]
diff --git a/smtlib/src/lib.rs b/smtlib/src/lib.rs
index 9a25922..37a852a 100644
--- a/smtlib/src/lib.rs
+++ b/smtlib/src/lib.rs
@@ -14,14 +14,12 @@ pub use backend::Backend;
 pub use logics::Logic;
 pub use smtlib_lowlevel::backend;
 
-#[cfg(feature = "async")]
 mod async_solver;
 mod logics;
 mod solver;
 pub mod terms;
 pub mod theories;
 
-#[cfg(feature = "async")]
 pub use async_solver::AsyncSolver;
 pub use solver::Solver;
 pub use theories::{core::*, fixed_size_bit_vectors::*, ints::*, reals::*};