diff --git a/src/context.rs b/src/context.rs
index 1ed0f1f..00890cc 100644
--- a/src/context.rs
+++ b/src/context.rs
@@ -483,6 +483,19 @@ impl Context {
         )
     }
 
+    /// Instruct the solver to exit.
+    pub fn exit(&mut self) -> io::Result<()> {
+        let solver = self
+            .solver
+            .as_mut()
+            .expect("exit requires a running solver");
+        solver.ack_command(
+            &self.arena,
+            self.atoms.success,
+            self.arena.list(vec![self.atoms.exit]),
+        )
+    }
+
     /// Push a new context frame in the solver. Same as SMTLIB's `push` command.
     pub fn push(&mut self) -> io::Result<()> {
         let solver = self
diff --git a/src/known_atoms.rs b/src/known_atoms.rs
index 45de1c6..771449e 100644
--- a/src/known_atoms.rs
+++ b/src/known_atoms.rs
@@ -21,6 +21,7 @@ macro_rules! for_each_known_atom {
             get_unsat_core: "get-unsat-core";
             set_logic: "set-logic";
             set_option: "set-option";
+            exit: "exit";
             push: "push";
             pop: "pop";
             bool: "Bool";