diff --git a/Cargo.lock b/Cargo.lock
index 90a6cabe8..fe17060a5 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -280,8 +280,10 @@ dependencies = [
  "clap",
  "conjure_core",
  "conjure_rules",
+ "itertools",
  "linkme",
  "minion_rs",
+ "regex",
  "serde",
  "serde_json",
  "serde_with",
diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml
index bde4a9cee..cb9baf9a9 100644
--- a/conjure_oxide/Cargo.toml
+++ b/conjure_oxide/Cargo.toml
@@ -24,6 +24,8 @@ strum = "0.26.2"
 versions = "6.1.0"
 linkme = "0.3.22"
 walkdir = "2.5.0"
+itertools = "0.12.1"
+regex = "1.10.3"
 
 [features]
 
diff --git a/conjure_oxide/src/generate_custom.rs b/conjure_oxide/src/generate_custom.rs
index d8adbcf09..b8ba38405 100644
--- a/conjure_oxide/src/generate_custom.rs
+++ b/conjure_oxide/src/generate_custom.rs
@@ -4,13 +4,11 @@
 use crate::parse::model_from_json;
 use conjure_core::ast::Model;
 
-use std::error::Error;
-
 use std::path::PathBuf;
 use walkdir::WalkDir;
 
-/// Searches recursively in `../tests/integration` folder for an `.essence` file matching the given filename,
-/// then uses conjure to process it into astjson, and returns the parsed model.
+/// Searches recursively in `../tests/integration` folder for an `.essence` file matching the given
+/// filename, then uses conjure to process it into astjson, and returns the parsed model.
 ///
 /// # Arguments
 ///
@@ -18,8 +16,8 @@ use walkdir::WalkDir;
 ///
 /// # Returns
 ///
-/// Function returns a `Result<Value, Box<dyn Error>>`, where `Value` is the parsed model
-pub fn get_example_model(filename: &str) -> Result<Model, Box<dyn Error>> {
+/// Function returns a `Result<Value, anyhow::Error>`, where `Value` is the parsed model.
+pub fn get_example_model(filename: &str) -> Result<Model, anyhow::Error> {
     // define relative path -> integration tests dir
     let base_dir = "tests/integration";
     let mut essence_path = PathBuf::new();
@@ -36,11 +34,11 @@ pub fn get_example_model(filename: &str) -> Result<Model, Box<dyn Error>> {
         }
     }
 
-    println!("PATH TO FILE: {}", essence_path.display());
+    //println!("PATH TO FILE: {}", essence_path.display());
 
     // return error if file not found
     if essence_path.as_os_str().is_empty() {
-        return Err(Box::new(std::io::Error::new(
+        return Err(anyhow::Error::new(std::io::Error::new(
             std::io::ErrorKind::NotFound,
             "ERROR: File not found in any subdirectory",
         )));
@@ -57,7 +55,7 @@ pub fn get_example_model(filename: &str) -> Result<Model, Box<dyn Error>> {
     // convert Conjure's stdout from bytes to string
     let astjson = String::from_utf8(output.stdout)?;
 
-    println!("ASTJSON: {}", astjson);
+    //println!("ASTJSON: {}", astjson);
 
     // parse AST JSON from desired Model format
     let generated_mdl = model_from_json(&astjson)?;
@@ -74,19 +72,19 @@ pub fn get_example_model(filename: &str) -> Result<Model, Box<dyn Error>> {
 ///
 /// # Returns
 ///
-/// Function returns a `Result<Value, Box<dyn Error>>`, where `Value` is the parsed model
-pub fn get_example_model_by_path(filepath: &str) -> Result<Model, Box<dyn Error>> {
+/// Function returns a `Result<Value, anyhow::Error>`, where `Value` is the parsed model
+pub fn get_example_model_by_path(filepath: &str) -> Result<Model, anyhow::Error> {
     let essence_path = PathBuf::from(filepath);
 
     // return error if file not found
     if essence_path.as_os_str().is_empty() {
-        return Err(Box::new(std::io::Error::new(
+        return Err(anyhow::Error::new(std::io::Error::new(
             std::io::ErrorKind::NotFound,
             "ERROR: File not found in any subdirectory",
         )));
     }
 
-    println!("PATH TO FILE: {}", essence_path.display());
+    // println!("PATH TO FILE: {}", essence_path.display());
 
     // Command execution using 'conjure' CLI tool with provided path
     let mut cmd = std::process::Command::new("conjure");
@@ -99,7 +97,7 @@ pub fn get_example_model_by_path(filepath: &str) -> Result<Model, Box<dyn Error>
     // convert Conjure's stdout from bytes to string
     let astjson = String::from_utf8(output.stdout)?;
 
-    println!("ASTJSON: {}", astjson);
+    // println!("ASTJSON: {}", astjson);
 
     // parse AST JSON into the desired Model format
     let generated_model = model_from_json(&astjson)?;
diff --git a/conjure_oxide/src/unstable/mod.rs b/conjure_oxide/src/unstable/mod.rs
index 7f45f3281..c31642288 100644
--- a/conjure_oxide/src/unstable/mod.rs
+++ b/conjure_oxide/src/unstable/mod.rs
@@ -1,6 +1,3 @@
 //! Unstable and in-development features of Conjure-Oxide.
-//!
-//! Enabling these may introduce breaking changes that affect code compilation.
 
-#![cfg(feature = "unstable-solver-interface")]
 pub mod solver_interface;
diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs
new file mode 100644
index 000000000..859fc0e74
--- /dev/null
+++ b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs
@@ -0,0 +1,336 @@
+use std::collections::HashMap;
+use std::sync::{Condvar, Mutex, OnceLock};
+
+use crate::unstable::solver_interface::SolverMutCallback;
+use crate::unstable::solver_interface::{states, SolverCallback};
+
+use super::super::model_modifier::NotModifiable;
+use super::super::private;
+use super::super::stats::NoStats;
+use super::super::SearchComplete::*;
+use super::super::SearchIncomplete::*;
+use super::super::SearchStatus::*;
+use super::super::SolveSuccess;
+use super::super::SolverAdaptor;
+use super::super::SolverError;
+use super::super::SolverError::*;
+
+use minion_rs::run_minion;
+use regex::Regex;
+
+use crate::ast as conjureast;
+use minion_rs::ast as minionast;
+
+/// A [SolverAdaptor] for interacting with Minion.
+///
+/// This adaptor uses the `minion_rs` crate to talk to Minion over FFI.
+pub struct Minion {
+    __non_constructable: private::Internal,
+}
+
+static MINION_LOCK: Mutex<()> = Mutex::new(());
+static USER_CALLBACK: OnceLock<Mutex<SolverCallback>> = OnceLock::new();
+static ANY_SOLUTIONS: Mutex<bool> = Mutex::new(false);
+static USER_TERIMINATED: Mutex<bool> = Mutex::new(false);
+
+#[allow(clippy::unwrap_used)]
+fn minion_rs_callback(solutions: HashMap<minionast::VarName, minionast::Constant>) -> bool {
+    *(ANY_SOLUTIONS.lock().unwrap()) = true;
+    let callback = USER_CALLBACK
+        .get_or_init(|| Mutex::new(Box::new(|x| true)))
+        .lock()
+        .unwrap();
+
+    let mut conjure_solutions: HashMap<conjureast::Name, conjureast::Constant> = HashMap::new();
+    for (minion_name, minion_const) in solutions.into_iter() {
+        let conjure_const = match minion_const {
+            minionast::Constant::Bool(x) => conjureast::Constant::Bool(x),
+            minionast::Constant::Integer(x) => conjureast::Constant::Int(x),
+            _ => todo!(),
+        };
+
+        let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap();
+        let conjure_name = if let Some(caps) = machine_name_re.captures(&minion_name) {
+            conjureast::Name::MachineName(caps[1].parse::<i32>().unwrap())
+        } else {
+            conjureast::Name::UserName(minion_name)
+        };
+
+        conjure_solutions.insert(conjure_name, conjure_const);
+    }
+
+    let continue_search = (**callback)(conjure_solutions);
+    if !continue_search {
+        *(USER_TERIMINATED.lock().unwrap()) = true;
+    }
+
+    continue_search
+}
+
+impl private::Sealed for Minion {}
+impl SolverAdaptor for Minion {
+    type Model = minionast::Model;
+    type Solution = minionast::Constant;
+    type Modifier = NotModifiable;
+
+    fn new() -> Minion {
+        Minion {
+            __non_constructable: private::Internal,
+        }
+    }
+
+    #[allow(clippy::unwrap_used)]
+    fn solve(
+        &mut self,
+        model: Self::Model,
+        callback: SolverCallback,
+        _: private::Internal,
+    ) -> Result<SolveSuccess, SolverError> {
+        // our minion callback is global state, so single threading the adaptor as a whole is
+        // probably a good move...
+        #[allow(clippy::unwrap_used)]
+        let mut minion_lock = MINION_LOCK.lock().unwrap();
+
+        #[allow(clippy::unwrap_used)]
+        let mut user_callback = USER_CALLBACK
+            .get_or_init(|| Mutex::new(Box::new(|x| true)))
+            .lock()
+            .unwrap();
+        *user_callback = callback;
+        std::mem::drop(user_callback); // release mutex. REQUIRED so that run_minion can use the
+                                       // user callback and not deadlock.
+
+        minion_rs::run_minion(model, minion_rs_callback).map_err(|err| match err {
+            minion_rs::error::MinionError::RuntimeError(x) => {
+                SolverError::Runtime(format!("{:#?}", x))
+            }
+            minion_rs::error::MinionError::Other(x) => SolverError::Runtime(format!("{:#?}", x)),
+            minion_rs::error::MinionError::NotImplemented(x) => {
+                SolverError::RuntimeNotImplemented(x)
+            }
+            x => SolverError::Runtime(format!("unknown minion_rs error: {:#?}", x)),
+        })?;
+
+        let mut status = Complete(HasSolutions);
+        if *(USER_TERIMINATED.lock()).unwrap() {
+            status = Incomplete(UserTerminated);
+        } else if *(ANY_SOLUTIONS.lock()).unwrap() {
+            status = Complete(NoSolutions);
+        }
+        Ok(SolveSuccess {
+            stats: None,
+            status,
+        })
+    }
+
+    fn solve_mut(
+        &mut self,
+        model: Self::Model,
+        callback: SolverMutCallback<Self>,
+        _: private::Internal,
+    ) -> Result<SolveSuccess, SolverError> {
+        Err(OpNotImplemented("solve_mut".into()))
+    }
+
+    fn load_model(
+        &mut self,
+        model: conjure_core::ast::Model,
+        _: private::Internal,
+    ) -> Result<Self::Model, SolverError> {
+        let mut minion_model = minionast::Model::new();
+        parse_vars(&model, &mut minion_model)?;
+        parse_exprs(&model, &mut minion_model)?;
+        Ok(minion_model)
+    }
+}
+
+fn parse_vars(
+    conjure_model: &conjureast::Model,
+    minion_model: &mut minionast::Model,
+) -> Result<(), SolverError> {
+    // TODO (niklasdewally): remove unused vars?
+    // TODO (niklasdewally): ensure all vars references are used.
+
+    for (name, variable) in conjure_model.variables.iter() {
+        parse_var(name, variable, minion_model)?;
+    }
+    Ok(())
+}
+
+fn parse_var(
+    name: &conjureast::Name,
+    var: &conjureast::DecisionVariable,
+    minion_model: &mut minionast::Model,
+) -> Result<(), SolverError> {
+    match &var.domain {
+        conjureast::Domain::IntDomain(ranges) => _parse_intdomain_var(name, ranges, minion_model),
+        conjureast::Domain::BoolDomain => _parse_booldomain_var(name, minion_model),
+        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
+    }
+}
+
+fn _parse_intdomain_var(
+    name: &conjureast::Name,
+    ranges: &Vec<conjureast::Range<i32>>,
+    minion_model: &mut minionast::Model,
+) -> Result<(), SolverError> {
+    let str_name = _name_to_string(name.to_owned());
+
+    if ranges.len() != 1 {
+        return Err(ModelFeatureNotImplemented(format!(
+            "variable {:?} has {:?} ranges. Multiple ranges / SparseBound is not yet supported.",
+            str_name,
+            ranges.len()
+        )));
+    }
+
+    let range = ranges.first().ok_or(ModelInvalid(format!(
+        "variable {:?} has no range",
+        str_name
+    )))?;
+
+    let (low, high) = match range {
+        conjureast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())),
+        conjureast::Range::Single(x) => Ok((x.to_owned(), x.to_owned())),
+        #[allow(unreachable_patterns)]
+        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
+    }?;
+
+    _try_add_var(
+        str_name.to_owned(),
+        minionast::VarDomain::Bound(low, high),
+        minion_model,
+    )
+}
+
+fn _parse_booldomain_var(
+    name: &conjureast::Name,
+    minion_model: &mut minionast::Model,
+) -> Result<(), SolverError> {
+    let str_name = _name_to_string(name.to_owned());
+    _try_add_var(
+        str_name.to_owned(),
+        minionast::VarDomain::Bool,
+        minion_model,
+    )
+}
+
+fn _try_add_var(
+    name: minionast::VarName,
+    domain: minionast::VarDomain,
+    minion_model: &mut minionast::Model,
+) -> Result<(), SolverError> {
+    minion_model
+        .named_variables
+        .add_var(name.clone(), domain)
+        .ok_or(ModelInvalid(format!(
+            "variable {:?} is defined twice",
+            name
+        )))
+}
+
+fn parse_exprs(
+    conjure_model: &conjureast::Model,
+    minion_model: &mut minionast::Model,
+) -> Result<(), SolverError> {
+    for expr in conjure_model.get_constraints_vec().iter() {
+        parse_expr(expr.to_owned(), minion_model)?;
+    }
+    Ok(())
+}
+
+fn parse_expr(
+    expr: conjureast::Expression,
+    minion_model: &mut minionast::Model,
+) -> Result<(), SolverError> {
+    minion_model.constraints.push(read_expr(expr)?);
+    Ok(())
+}
+
+fn read_expr(expr: conjureast::Expression) -> Result<minionast::Constraint, SolverError> {
+    match expr {
+        conjureast::Expression::SumLeq(_metadata, lhs, rhs) => Ok(minionast::Constraint::SumLeq(
+            read_vars(lhs)?,
+            read_var(*rhs)?,
+        )),
+        conjureast::Expression::SumGeq(_metadata, lhs, rhs) => Ok(minionast::Constraint::SumGeq(
+            read_vars(lhs)?,
+            read_var(*rhs)?,
+        )),
+        conjureast::Expression::Ineq(_metadata, a, b, c) => Ok(minionast::Constraint::Ineq(
+            read_var(*a)?,
+            read_var(*b)?,
+            minionast::Constant::Integer(read_const(*c)?),
+        )),
+        conjureast::Expression::Neq(_metadata, a, b) => Ok(minionast::Constraint::AllDiff(vec![
+            read_var(*a)?,
+            read_var(*b)?,
+        ])),
+        // conjureast::Expression::DivEq(_metadata, a, b, c) => {
+        //     minion_model.constraints.push(minionast::Constraint::Div(
+        //         (read_var(*a)?, read_var(*b)?),
+        //         read_var(*c)?,
+        //     ));
+        //     Ok(())
+        // }
+        conjureast::Expression::AllDiff(_metadata, vars) => {
+            Ok(minionast::Constraint::AllDiff(read_vars(vars)?))
+        }
+        conjureast::Expression::Or(_metadata, exprs) => Ok(minionast::Constraint::WatchedOr(
+            exprs
+                .iter()
+                .map(|x| read_expr(x.to_owned()))
+                .collect::<Result<Vec<minionast::Constraint>, SolverError>>()?,
+        )),
+        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
+    }
+}
+fn read_vars(exprs: Vec<conjureast::Expression>) -> Result<Vec<minionast::Var>, SolverError> {
+    let mut minion_vars: Vec<minionast::Var> = vec![];
+    for expr in exprs {
+        let minion_var = read_var(expr)?;
+        minion_vars.push(minion_var);
+    }
+    Ok(minion_vars)
+}
+
+fn read_var(e: conjureast::Expression) -> Result<minionast::Var, SolverError> {
+    // a minion var is either a reference or a "var as const"
+    match _read_ref(e.clone()) {
+        Ok(name) => Ok(minionast::Var::NameRef(name)),
+        Err(_) => match read_const(e) {
+            Ok(n) => Ok(minionast::Var::ConstantAsVar(n)),
+            Err(x) => Err(x),
+        },
+    }
+}
+
+fn _read_ref(e: conjureast::Expression) -> Result<String, SolverError> {
+    let name = match e {
+        conjureast::Expression::Reference(_metdata, n) => Ok(n),
+        x => Err(ModelInvalid(format!(
+            "expected a reference, but got `{0:?}`",
+            x
+        ))),
+    }?;
+
+    let str_name = _name_to_string(name);
+    Ok(str_name)
+}
+
+fn read_const(e: conjureast::Expression) -> Result<i32, SolverError> {
+    match e {
+        conjureast::Expression::Constant(_, conjureast::Constant::Int(n)) => Ok(n),
+        x => Err(ModelInvalid(format!(
+            "expected a constant, but got `{0:?}`",
+            x
+        ))),
+    }
+}
+
+fn _name_to_string(name: conjureast::Name) -> String {
+    match name {
+        conjureast::Name::UserName(x) => x,
+        conjureast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x),
+    }
+}
diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs
new file mode 100644
index 000000000..04eb63e72
--- /dev/null
+++ b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs
@@ -0,0 +1,5 @@
+//! Solver adaptors.
+
+mod minion;
+#[doc(inline)]
+pub use minion::Minion;
diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs
index e846e3880..d7f19b15b 100644
--- a/conjure_oxide/src/unstable/solver_interface/mod.rs
+++ b/conjure_oxide/src/unstable/solver_interface/mod.rs
@@ -1,10 +1,70 @@
-#![cfg(feature = "unstable-solver-interface")]
-
-//! A new interface for interacting with solvers.
+//! A high-level API for interacting with constraints solvers.
+//!
+//! This module provides a consistent, solver-independent API for interacting with constraints
+//! solvers. It also provides incremental solving support, and the returning of run stats from
+//! solvers.
+//!
+//! -----
+//!
+//! - [Solver<Adaptor>] provides the API for interacting with constraints solvers.
+//!
+//! - The [SolverAdaptor] trait controls how solving actually occurs and handles translation
+//! between the [Solver] type and a specific solver.
+//!
+//! - [adaptors] contains all implemented solver adaptors.
+//!
+//! - The [model_modifier] submodule defines types to help with incremental solving / changing a
+//!   model during search. The entrypoint for incremental solving is the [Solver<A,ModelLoaded>::solve_mut]
+//!   function.
+//!
+//! # Examples
+//!
+//! ## A Successful Minion Model
+//!
+//! ```rust
+//! # use conjure_oxide::generate_custom::get_example_model;
+//! use conjure_oxide::rule_engine::rewrite::rewrite_model;
+//! use conjure_oxide::rule_engine::resolve_rules::resolve_rule_sets;
+//! use conjure_oxide::unstable::solver_interface::{Solver,adaptors,SolverAdaptor};
+//! use conjure_oxide::unstable::solver_interface::states::*;
+//! use std::sync::{Arc,Mutex};
+//!
+//! // Define and rewrite a model for minion.
+//! let model = get_example_model("bool-03").unwrap();
+//! let rule_sets = resolve_rule_sets(vec!["Minion", "Constant"]).unwrap();
+//! let model = rewrite_model(&model,&rule_sets).unwrap();
+//!
+//!
+//! // Solve using Minion.
+//! let solver = Solver::new(adaptors::Minion::new());
+//! let solver: Solver<adaptors::Minion,ModelLoaded> = solver.load_model(model).unwrap();
+//!
+//! // In this example, we will count solutions.
+//! //
+//! // The solver interface is designed to allow adaptors to use multiple-threads / processes if
+//! // necessary. Therefore, the callback type requires all variables inside it to have a static
+//! // lifetime and to implement Send (i.e. the variable can be safely shared between theads).
+//! //
+//! // We use Arc<Mutex<T>> to create multiple references to a threadsafe mutable
+//! // variable of type T.
+//! //
+//! // Using the move |x| ... closure syntax, we move one of these references into the closure.
+//! // Note that a normal closure borrow variables from the parent so is not
+//! // thread-safe.
+//!
+//! let counter_ref = Arc::new(Mutex::new(0));
+//! let counter_ref_2 = counter_ref.clone();
+//! solver.solve(Box::new(move |_| {
+//!   let mut counter = (*counter_ref_2).lock().unwrap();
+//!   *counter += 1;
+//!   true
+//!   }));
+//!
+//! let mut counter = (*counter_ref).lock().unwrap();
+//! assert_eq!(*counter,2);
+//! ```
 //!
-//! # Example
 //!
-//! TODO
 
 // # Implementing Solver interfaces
 //
@@ -23,27 +83,70 @@
 #![allow(unused)]
 #![warn(clippy::exhaustive_enums)]
 
+pub mod adaptors;
+pub mod model_modifier;
+pub mod stats;
+
 #[doc(hidden)]
-mod private {
-    // Used to limit calling trait functions outside this module.
-    #[doc(hidden)]
-    pub struct Internal;
+mod private;
 
-    // https://predr.ag/blog/definitive-guide-to-sealed-traits-in-rust/#the-trick-for-sealing-traits
-    // Make traits unimplementable from outside of this module.
-    #[doc(hidden)]
-    pub trait Sealed {}
-}
+pub mod states;
 
-use self::incremental::*;
-use self::solver_states::*;
+use self::model_modifier::*;
+use self::states::*;
+use self::stats::Stats;
 use anyhow::anyhow;
+use conjure_core::ast::Constant;
+use conjure_core::ast::DecisionVariable;
 use conjure_core::ast::{Domain, Expression, Model, Name};
+use itertools::Either;
 use std::collections::HashMap;
 use std::error::Error;
 use std::fmt::{Debug, Display};
-
-/// A [`SolverAdaptor`] provide an interface to an underlying solver. Used by [`Solver`].
+use std::time::Instant;
+use thiserror::Error;
+
+/// The type for user-defined callbacks for use with [Solver].
+///
+/// Note that this enforces threadsafetyb
+pub type SolverCallback = Box<dyn Fn(HashMap<Name, Constant>) -> bool + Send>;
+pub type SolverMutCallback<A> =
+    Box<dyn Fn(HashMap<Name, Constant>, <A as SolverAdaptor>::Modifier) -> bool + Send>;
+
+/// A common interface for calling underlying solver APIs inside a [`Solver`].
+///
+/// Implementations of this trait arn't directly callable and should be used through [`Solver`] .
+///
+/// The below documentation lists the formal requirements that all implementations of
+/// [`SolverAdaptor`] should follow - **see the top level module documentation and [`Solver`] for
+/// usage details.**
+///
+/// # Encapsulation
+///  
+///  The [`SolverAdaptor`] trait **must** only be implemented inside a submodule of this one,
+///  and **should** only be called through [`Solver`].
+///
+/// The `private::Sealed` trait and `private::Internal` type enforce these requirements by only
+/// allowing trait implementations and calling of methods of SolverAdaptor to occur inside this
+/// module.
+///
+/// # Thread Safety
+///
+/// Multiple instances of [`Solver`] can be run in parallel across multiple threads.
+///
+/// [`Solver`] provides no concurrency control or thread-safety; therefore, adaptors **must**
+/// ensure that multiple instances of themselves can be ran in parallel. This applies to all
+/// stages of solving including having two active `solve()` calls happening at a time, loading
+/// a model while another is mid-solve, loading two models at once, etc.
+///
+/// A [SolverAdaptor] **may** use whatever threading or process model it likes underneath the hood,
+/// as long as it obeys the above.
+///
+/// Method calls **should** block instead of erroring where possible.
+///
+/// Underlying solvers that only have one instance per process (such as Minion) **should** block
+/// (eg. using a [`Mutex<()>`](`std::sync::Mutex`)) to run calls to
+/// [`Solver<A,ModelLoaded>::solve()`] and [`Solver<A,ModelLoaded>::solve_mut()`] sequentially.
 pub trait SolverAdaptor: private::Sealed {
     /// The native model type of the underlying solver.
     type Model: Clone;
@@ -51,62 +154,97 @@ pub trait SolverAdaptor: private::Sealed {
     /// The native solution type of the underlying solver.
     type Solution: Clone;
 
-    /// The [`ModelModifier`](incremental::ModelModifier) used during incremental search.
+    /// The [`ModelModifier`](model_modifier::ModelModifier) used during incremental search.
     ///
-    /// If incremental solving is not supported, this SHOULD be set to [NotModifiable](`incremental::NotModifiable`) .
-    type Modifier: incremental::ModelModifier;
+    /// If incremental solving is not supported, this **should** be set to [NotModifiable](model_modifier::NotModifiable) .
+    type Modifier: model_modifier::ModelModifier;
 
-    /// Run the solver on the given model.
+    fn new() -> Self;
+
+    /// Runs the solver on the given model.
     ///
-    /// Implementations of this function MUST call the user provided callback whenever a solution
+    /// Implementations of this function **must** call the user provided callback whenever a solution
     /// is found. If the user callback returns `true`, search should continue, if the user callback
     /// returns `false`, search should terminate.
+    ///
+    /// # Returns
+    ///
+    /// If the solver terminates without crashing a [SolveSuccess] struct **must** returned. The
+    /// value of [SearchStatus] can be used to denote whether the underlying solver completed its
+    /// search or not. The latter case covers most non-crashing "failure" cases including user
+    /// termination, timeouts, etc.
+    ///
+    /// To help populate [SearchStatus], it may be helpful to implement counters that track if the
+    /// user callback has been called yet, and its return value. This information makes it is
+    /// possible to distinguish between the most common search statuses:
+    /// [SearchComplete::HasSolutions], [SearchComplete::NoSolutions], and
+    /// [SearchIncomplete::UserTerminated].
     fn solve(
         &mut self,
         model: Self::Model,
-        callback: fn(HashMap<String, String>) -> bool,
+        callback: SolverCallback,
         _: private::Internal,
-    ) -> Result<ExecutionSuccess, ExecutionFailure>;
+    ) -> Result<SolveSuccess, SolverError>;
 
-    /// Run the solver on the given model, allowing modification of the model through a
+    /// Runs the solver on the given model, allowing modification of the model through a
     /// [`ModelModifier`].
     ///
-    /// Implementations of this function MUST return [`OpNotSupported`](`ModificationFailure::OpNotSupported`)
-    /// if modifying the model mid-search is not supported. These implementations may also find the
-    /// [`NotModifiable`] modifier useful.
+    /// Implementations of this function **must** return [`OpNotSupported`](`ModificationFailure::OpNotSupported`)
+    /// if modifying the model mid-search is not supported.
     ///
-    /// As with [`solve`](SolverAdaptor::solve), this function MUST call the user provided callback
-    /// function whenever a solution is found.
+    /// Otherwise, this should work in the same way as [`solve`](SolverAdaptor::solve).
     fn solve_mut(
         &mut self,
         model: Self::Model,
-        callback: fn(HashMap<String, String>, Self::Modifier) -> bool,
+        callback: SolverMutCallback<Self>,
         _: private::Internal,
-    ) -> Result<ExecutionSuccess, ExecutionFailure>;
+    ) -> Result<SolveSuccess, SolverError>;
     fn load_model(
         &mut self,
         model: Model,
         _: private::Internal,
-    ) -> Result<Self::Model, anyhow::Error>;
+    ) -> Result<Self::Model, SolverError>;
     fn init_solver(&mut self, _: private::Internal) {}
 }
 
-/// A Solver executes of a Conjure-Oxide model usign a specified solver.
+/// An abstract representation of a constraints solver.
+///
+/// [Solver] provides a common interface for interacting with a constraint solver. It also
+/// abstracts over solver-specific datatypes, handling the translation to/from [conjure_core::ast]
+/// types for a model and its solutions.
+///
+/// Details of how a model is solved is specified by the [SolverAdaptor]. This includes: the
+/// underlying solver used, the translation of the model to a solver compatible form, how solutions
+/// are translated back to [conjure_core::ast] types, and how incremental solving is implemented.
+/// As such, there may be multiple [SolverAdaptor] implementations for a single underlying solver:
+/// eg. one adaptor may give solutions in a representation close to the solvers, while another may
+/// attempt to rewrite it back into Essence.
+///
+#[derive(Clone)]
 pub struct Solver<A: SolverAdaptor, State: SolverState = Init> {
-    state: std::marker::PhantomData<State>,
+    state: State,
     adaptor: A,
     model: Option<A::Model>,
 }
 
+impl<Adaptor: SolverAdaptor> Solver<Adaptor> {
+    pub fn new(solver_adaptor: Adaptor) -> Solver<Adaptor> {
+        let mut solver = Solver {
+            state: Init,
+            adaptor: solver_adaptor,
+            model: None,
+        };
+
+        solver.adaptor.init_solver(private::Internal);
+        solver
+    }
+}
+
 impl<A: SolverAdaptor> Solver<A, Init> {
-    // TODO: decent error handling
-    pub fn load_model(mut self, model: Model) -> Result<Solver<A, ModelLoaded>, ()> {
-        let solver_model = &mut self
-            .adaptor
-            .load_model(model, private::Internal)
-            .map_err(|_| ())?;
+    pub fn load_model(mut self, model: Model) -> Result<Solver<A, ModelLoaded>, SolverError> {
+        let solver_model = &mut self.adaptor.load_model(model, private::Internal)?;
         Ok(Solver {
-            state: std::marker::PhantomData::<ModelLoaded>,
+            state: ModelLoaded,
             adaptor: self.adaptor,
             model: Some(solver_model.clone()),
         })
@@ -116,128 +254,127 @@ impl<A: SolverAdaptor> Solver<A, Init> {
 impl<A: SolverAdaptor> Solver<A, ModelLoaded> {
     pub fn solve(
         mut self,
-        callback: fn(HashMap<String, String>) -> bool,
-    ) -> Result<ExecutionSuccess, ExecutionFailure> {
+        callback: SolverCallback,
+    ) -> Result<Solver<A, ExecutionSuccess>, SolverError> {
         #[allow(clippy::unwrap_used)]
-        self.adaptor
-            .solve(self.model.unwrap(), callback, private::Internal)
+        let start_time = Instant::now();
+
+        #[allow(clippy::unwrap_used)]
+        let result = self
+            .adaptor
+            .solve(self.model.clone().unwrap(), callback, private::Internal);
+
+        let duration = start_time.elapsed();
+
+        match result {
+            Ok(x) => Ok(Solver {
+                adaptor: self.adaptor,
+                model: self.model,
+                state: ExecutionSuccess {
+                    stats: x.stats,
+                    status: x.status,
+                    _sealed: private::Internal,
+                    wall_time_s: duration.as_secs_f64(),
+                },
+            }),
+            Err(x) => Err(x),
+        }
     }
 
     pub fn solve_mut(
         mut self,
-        callback: fn(HashMap<String, String>, A::Modifier) -> bool,
-    ) -> Result<ExecutionSuccess, ExecutionFailure> {
+        callback: SolverMutCallback<A>,
+    ) -> Result<Solver<A, ExecutionSuccess>, SolverError> {
         #[allow(clippy::unwrap_used)]
-        self.adaptor
-            .solve_mut(self.model.unwrap(), callback, private::Internal)
+        let start_time = Instant::now();
+
+        #[allow(clippy::unwrap_used)]
+        let result =
+            self.adaptor
+                .solve_mut(self.model.clone().unwrap(), callback, private::Internal);
+
+        let duration = start_time.elapsed();
+
+        match result {
+            Ok(x) => Ok(Solver {
+                adaptor: self.adaptor,
+                model: self.model,
+                state: ExecutionSuccess {
+                    stats: x.stats,
+                    status: x.status,
+                    _sealed: private::Internal,
+                    wall_time_s: duration.as_secs_f64(),
+                },
+            }),
+            Err(x) => Err(x),
+        }
     }
 }
 
-impl<T: SolverAdaptor> Solver<T> {
-    pub fn new(solver_adaptor: T) -> Solver<T> {
-        let mut solver = Solver {
-            state: std::marker::PhantomData::<Init>,
-            adaptor: solver_adaptor,
-            model: None,
-        };
+impl<A: SolverAdaptor> Solver<A, ExecutionSuccess> {
+    pub fn stats(self) -> Option<Box<dyn Stats>> {
+        self.state.stats
+    }
 
-        solver.adaptor.init_solver(private::Internal);
-        solver
+    pub fn wall_time_s(&self) -> f64 {
+        self.state.wall_time_s
     }
 }
 
-pub mod solver_states {
-    //! States of a [`Solver`].
-
-    use super::private::Sealed;
-    use super::Solver;
-
-    pub trait SolverState: Sealed {}
-
-    impl Sealed for Init {}
-    impl Sealed for ModelLoaded {}
-    impl Sealed for ExecutionSuccess {}
-    impl Sealed for ExecutionFailure {}
-
-    impl SolverState for Init {}
-    impl SolverState for ModelLoaded {}
-    impl SolverState for ExecutionSuccess {}
-    impl SolverState for ExecutionFailure {}
+/// Errors returned by [Solver] on failure.
+#[non_exhaustive]
+#[derive(Debug, Error, Clone)]
+pub enum SolverError {
+    #[error("operation not implemented yet: {0}")]
+    OpNotImplemented(String),
 
-    pub struct Init;
-    pub struct ModelLoaded;
+    #[error("operation not supported: {0}")]
+    OpNotSupported(String),
 
-    /// The state returned by [`Solver`] if solving has been successful.
-    pub struct ExecutionSuccess;
+    #[error("model feature not supported: {0}")]
+    ModelFeatureNotSupported(String),
 
-    /// The state returned by [`Solver`] if solving has not been successful.
-    #[non_exhaustive]
-    pub enum ExecutionFailure {
-        /// The desired function or solver is not implemented yet.
-        OpNotImplemented,
+    #[error("model feature not implemented yet: {0}")]
+    ModelFeatureNotImplemented(String),
 
-        /// The solver does not support this operation.
-        OpNotSupported,
+    // use for semantics / type errors, use the above for syntax
+    #[error("model invalid: {0}")]
+    ModelInvalid(String),
 
-        /// Solving timed-out.
-        TimedOut,
+    #[error("error during solver execution: not implemented: {0}")]
+    RuntimeNotImplemented(String),
 
-        /// An unspecified error has occurred.
-        Error(anyhow::Error),
-    }
+    #[error("error during solver execution: {0}")]
+    Runtime(String),
 }
 
-pub mod incremental {
-    //! Incremental / mutable solving (changing the model during search).
-    //!
-    //! Incremental solving can be triggered for a solverthrough the
-    //! [`Solver::solve_mut`] method.
-    //!
-    //! This gives access to a [`ModelModifier`] in the solution retrieval callback.
-    use super::private;
-    use super::Solver;
-    use conjure_core::ast::{Domain, Expression, Model, Name};
-
-    /// A ModelModifier provides an interface to modify a model during solving.
-    ///
-    /// Modifications are defined in terms of Conjure AST nodes, so must be translated to a solver
-    /// specfic form before use.
-    ///
-    /// It is implementation defined whether these constraints can be given at high level and passed
-    /// through the rewriter, or only low-level solver constraints are supported.
-    ///
-    /// See also: [`Solver::solve_mut`].
-    pub trait ModelModifier: private::Sealed {
-        fn add_constraint(constraint: Expression) -> Result<(), ModificationFailure> {
-            Err(ModificationFailure::OpNotSupported)
-        }
-
-        fn add_variable(name: Name, domain: Domain) -> Result<(), ModificationFailure> {
-            Err(ModificationFailure::OpNotSupported)
-        }
-    }
-
-    /// A [`ModelModifier`] for a solver that does not support incremental solving. Returns
-    /// [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) for all operations.
-    pub struct NotModifiable;
-
-    impl private::Sealed for NotModifiable {}
-    impl ModelModifier for NotModifiable {}
-
-    /// The requested modification to the model has failed.
-    #[non_exhaustive]
-    pub enum ModificationFailure {
-        /// The desired operation is not supported for this solver adaptor.
-        OpNotSupported,
+/// Returned from [SolverAdaptor] when solving is successful.
+pub struct SolveSuccess {
+    stats: Option<Box<dyn Stats>>,
+    status: SearchStatus,
+}
 
-        /// The desired operation is supported by this solver adaptor, but has not been
-        /// implemented yet.
-        OpNotImplemented,
+pub enum SearchStatus {
+    /// The search was complete (i.e. the solver found all possible solutions)
+    Complete(SearchComplete),
+    /// The search was incomplete (i.e. it was terminated before all solutions were found)
+    Incomplete(SearchIncomplete),
+}
 
-        // The arguments given to the operation are invalid.
-        ArgsInvalid(anyhow::Error),
+#[non_exhaustive]
+pub enum SearchIncomplete {
+    Timeout,
+    UserTerminated,
+    #[doc(hidden)]
+    /// This variant should not be matched - it exists to simulate non-exhaustiveness of this enum.
+    __NonExhaustive,
+}
 
-        /// An unspecified error has occurred.
-        Error(anyhow::Error),
-    }
+#[non_exhaustive]
+pub enum SearchComplete {
+    HasSolutions,
+    NoSolutions,
+    #[doc(hidden)]
+    /// This variant should not be matched - it exists to simulate non-exhaustiveness of this enum.
+    __NonExhaustive,
 }
diff --git a/conjure_oxide/src/unstable/solver_interface/model_modifier.rs b/conjure_oxide/src/unstable/solver_interface/model_modifier.rs
new file mode 100644
index 000000000..c0cd880bf
--- /dev/null
+++ b/conjure_oxide/src/unstable/solver_interface/model_modifier.rs
@@ -0,0 +1,53 @@
+//! Modifying a model during search.
+//!
+//! Incremental solving can be triggered for a solverthrough the
+//! [`Solver::solve_mut`] method.
+//!
+//! This gives access to a [`ModelModifier`] in the solution retrieval callback.
+
+use super::private;
+use super::Solver;
+use conjure_core::ast::{Domain, Expression, Model, Name};
+
+/// A ModelModifier provides an interface to modify a model during solving.
+///
+/// Modifications are defined in terms of Conjure AST nodes, so must be translated to a solver
+/// specfic form before use.
+///
+/// It is implementation defined whether these constraints can be given at high level and passed
+/// through the rewriter, or only low-level solver constraints are supported.
+///
+/// See also: [`Solver::solve_mut`].
+pub trait ModelModifier: private::Sealed {
+    fn add_constraint(constraint: Expression) -> Result<(), ModificationFailure> {
+        Err(ModificationFailure::OpNotSupported)
+    }
+
+    fn add_variable(name: Name, domain: Domain) -> Result<(), ModificationFailure> {
+        Err(ModificationFailure::OpNotSupported)
+    }
+}
+
+/// A [`ModelModifier`] for a solver that does not support incremental solving. Returns
+/// [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) for all operations.
+pub struct NotModifiable;
+
+impl private::Sealed for NotModifiable {}
+impl ModelModifier for NotModifiable {}
+
+/// The requested modification to the model has failed.
+#[non_exhaustive]
+pub enum ModificationFailure {
+    /// The desired operation is not supported for this solver adaptor.
+    OpNotSupported,
+
+    /// The desired operation is supported by this solver adaptor, but has not been
+    /// implemented yet.
+    OpNotImplemented,
+
+    // The arguments given to the operation are invalid.
+    ArgsInvalid(anyhow::Error),
+
+    /// An unspecified error has occurred.
+    Error(anyhow::Error),
+}
diff --git a/conjure_oxide/src/unstable/solver_interface/private.rs b/conjure_oxide/src/unstable/solver_interface/private.rs
new file mode 100644
index 000000000..67f87b89c
--- /dev/null
+++ b/conjure_oxide/src/unstable/solver_interface/private.rs
@@ -0,0 +1,8 @@
+// Used to limit calling trait functions outside this module.
+#[doc(hidden)]
+pub struct Internal;
+
+// https://predr.ag/blog/definitive-guide-to-sealed-traits-in-rust/#the-trick-for-sealing-traits
+// Make traits unimplementable from outside of this module.
+#[doc(hidden)]
+pub trait Sealed {}
diff --git a/conjure_oxide/src/unstable/solver_interface/states.rs b/conjure_oxide/src/unstable/solver_interface/states.rs
new file mode 100644
index 000000000..b0f4f9e97
--- /dev/null
+++ b/conjure_oxide/src/unstable/solver_interface/states.rs
@@ -0,0 +1,49 @@
+//! States of a [`Solver`].
+use std::fmt::Display;
+
+use thiserror::Error;
+
+use super::private::Internal;
+use super::private::Sealed;
+use super::stats::*;
+use super::SearchStatus;
+use super::Solver;
+use super::SolverError;
+
+pub trait SolverState: Sealed {}
+
+impl Sealed for Init {}
+impl Sealed for ModelLoaded {}
+impl Sealed for ExecutionSuccess {}
+impl Sealed for ExecutionFailure {}
+
+impl SolverState for Init {}
+impl SolverState for ModelLoaded {}
+impl SolverState for ExecutionSuccess {}
+impl SolverState for ExecutionFailure {}
+
+pub struct Init;
+pub struct ModelLoaded;
+
+/// The state returned by [`Solver`] if solving has been successful.
+pub struct ExecutionSuccess {
+    /// Execution statistics.
+    pub stats: Option<Box<dyn Stats>>,
+
+    /// The status of the search
+    pub status: SearchStatus,
+
+    // Wall time elapsed in seconds.
+    pub wall_time_s: f64,
+
+    /// Cannot construct this from outside this module.
+    pub _sealed: Internal,
+}
+
+/// The state returned by [`Solver`] if solving has not been successful.
+pub struct ExecutionFailure {
+    pub why: SolverError,
+
+    /// Cannot construct this from outside this module.
+    pub _sealed: Internal,
+}
diff --git a/conjure_oxide/src/unstable/solver_interface/stats.rs b/conjure_oxide/src/unstable/solver_interface/stats.rs
new file mode 100644
index 000000000..6aa14db07
--- /dev/null
+++ b/conjure_oxide/src/unstable/solver_interface/stats.rs
@@ -0,0 +1,8 @@
+//! Statistics about a solver run.
+use super::private::Sealed;
+
+pub trait Stats: Sealed {}
+
+pub struct NoStats;
+impl Sealed for NoStats {}
+impl Stats for NoStats {}
diff --git a/conjure_oxide/src/utils/conjure.rs b/conjure_oxide/src/utils/conjure.rs
index b0c903482..58b12e718 100644
--- a/conjure_oxide/src/utils/conjure.rs
+++ b/conjure_oxide/src/utils/conjure.rs
@@ -1,19 +1,15 @@
 use crate::parse::model_from_json;
-use crate::solvers::minion::MinionModel;
-use crate::solvers::FromConjureModel;
 use crate::utils::json::sort_json_object;
 use crate::Error as ParseErr;
-use conjure_core::ast::Model;
-use minion_rs::ast::{Constant, VarName};
-use minion_rs::run_minion;
+use conjure_core::ast::{Constant, Model, Name};
+use itertools::Either::{Left, Right};
 use serde_json::{Map, Value as JsonValue};
 use std::collections::HashMap;
-use std::ops::Deref;
-use std::sync::{Condvar, Mutex};
+use std::sync::{Arc, Mutex};
 use thiserror::Error as ThisError;
 
-static ALL_SOLUTIONS: Mutex<Vec<HashMap<VarName, Constant>>> = Mutex::new(vec![]);
-static LOCK: (Mutex<bool>, Condvar) = (Mutex::new(false), Condvar::new());
+use crate::unstable::solver_interface::adaptors::Minion;
+use crate::unstable::solver_interface::{Solver, SolverAdaptor};
 
 #[derive(Debug, ThisError)]
 pub enum EssenceParseError {
@@ -61,75 +57,35 @@ pub fn parse_essence_file(path: &str, filename: &str) -> Result<Model, EssencePa
     Ok(parsed_model)
 }
 
-pub fn get_minion_solutions(
-    model: Model,
-) -> Result<Vec<HashMap<VarName, Constant>>, anyhow::Error> {
-    fn callback(solutions: HashMap<VarName, Constant>) -> bool {
-        match ALL_SOLUTIONS.lock() {
-            Ok(mut guard) => {
-                guard.push(solutions);
-                true
-            }
-            Err(e) => {
-                eprintln!("Error getting lock on ALL_SOLUTIONS: {}", e);
-                false
-            }
-        }
-    }
+pub fn get_minion_solutions(model: Model) -> Result<Vec<HashMap<Name, Constant>>, anyhow::Error> {
+    let solver = Solver::new(Minion::new());
 
     println!("Building Minion model...");
-    let minion_model = MinionModel::from_conjure(model)?;
-
-    // @niklasdewally would be able to explain this better
-    // We use a condvar to keep a lock on the ALL_SOLUTIONS mutex until it goes out of scope
-    // So, no other threads can mutate ALL_SOLUTIONS while we're running Minion, only our callback can
-    let (lock, condvar) = &LOCK;
-    #[allow(clippy::unwrap_used)] // If the mutex is poisoned, we want to panic anyway
-    let mut _lock_guard = condvar
-        .wait_while(lock.lock().unwrap(), |locked| *locked)
-        .unwrap();
-
-    *_lock_guard = true;
+    let solver = solver.load_model(model)?;
 
     println!("Running Minion...");
-    match run_minion(minion_model, callback) {
-        Ok(res) => res,
-        Err(e) => {
-            eprintln!("Error running Minion: {}", e);
-            return Err(anyhow::anyhow!("Error running Minion: {}", e));
-        }
-    };
-
-    let ans = match ALL_SOLUTIONS.lock() {
-        Ok(mut guard) => {
-            let ans = guard.deref().clone();
-            guard.clear(); // Clear the solutions for the next test
-            ans
-        }
-        Err(e) => {
-            eprintln!("Error getting lock on ALL_SOLUTIONS: {}", e);
-            return Err(anyhow::anyhow!(
-                "Error getting lock on ALL_SOLUTIONS: {}",
-                e
-            ));
-        }
-    };
-
-    // Release the lock and wake the next waiting thread
-    *_lock_guard = false;
-    std::mem::drop(_lock_guard);
-    condvar.notify_one();
 
-    Ok(ans)
+    let all_solutions_ref = Arc::new(Mutex::<Vec<HashMap<Name, Constant>>>::new(vec![]));
+    let all_solutions_ref_2 = all_solutions_ref.clone();
+    #[allow(clippy::unwrap_used)]
+    solver.solve(Box::new(move |sols| {
+        let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
+        (*all_solutions).push(sols);
+        true
+    }))?;
+
+    #[allow(clippy::unwrap_used)]
+    let sols = (*all_solutions_ref).lock().unwrap();
+    Ok((*sols).clone())
 }
 
-pub fn minion_solutions_to_json(solutions: &Vec<HashMap<VarName, Constant>>) -> JsonValue {
+pub fn minion_solutions_to_json(solutions: &Vec<HashMap<Name, Constant>>) -> JsonValue {
     let mut json_solutions = Vec::new();
     for solution in solutions {
         let mut json_solution = Map::new();
         for (var_name, constant) in solution {
             let serialized_constant = match constant {
-                Constant::Integer(i) => JsonValue::Number((*i).into()),
+                Constant::Int(i) => JsonValue::Number((*i).into()),
                 Constant::Bool(b) => JsonValue::Bool(*b),
                 x => unimplemented!("{:#?}", x),
             };
diff --git a/conjure_oxide/src/utils/testing.rs b/conjure_oxide/src/utils/testing.rs
index 3b3884613..6b9b72241 100644
--- a/conjure_oxide/src/utils/testing.rs
+++ b/conjure_oxide/src/utils/testing.rs
@@ -2,7 +2,8 @@ use crate::utils::conjure::minion_solutions_to_json;
 use crate::utils::json::sort_json_object;
 use crate::utils::misc::to_set;
 use crate::Error;
-use conjure_core::ast::Model as ConjureModel;
+use conjure_core::ast::Name::UserName;
+use conjure_core::ast::{Constant, Model as ConjureModel, Name};
 use minion_rs::ast::{Constant as MinionConstant, VarName as MinionVarName};
 use serde_json::{Error as JsonError, Value as JsonValue};
 use std::collections::{HashMap, HashSet};
@@ -85,7 +86,7 @@ pub fn read_model_json(
 
 pub fn minion_solutions_from_json(
     serialized: &str,
-) -> Result<Vec<HashMap<MinionVarName, MinionConstant>>, anyhow::Error> {
+) -> Result<Vec<HashMap<Name, Constant>>, anyhow::Error> {
     let json: JsonValue = serde_json::from_str(serialized)?;
 
     let json_array = json
@@ -106,13 +107,13 @@ pub fn minion_solutions_from_json(
                     let n = n
                         .as_i64()
                         .ok_or(Error::Parse("Invalid integer".to_owned()))?;
-                    MinionConstant::Integer(n as i32)
+                    Constant::Int(n as i32)
                 }
-                JsonValue::Bool(b) => MinionConstant::Bool(*b),
+                JsonValue::Bool(b) => Constant::Bool(*b),
                 _ => return Err(Error::Parse("Invalid constant".to_owned()).into()),
             };
 
-            sol.insert(MinionVarName::from(var_name), constant);
+            sol.insert(UserName(var_name.into()), constant);
         }
 
         solutions.push(sol);
@@ -122,7 +123,7 @@ pub fn minion_solutions_from_json(
 }
 
 pub fn save_minion_solutions_json(
-    solutions: &Vec<HashMap<MinionVarName, MinionConstant>>,
+    solutions: &Vec<HashMap<Name, Constant>>,
     path: &str,
     test_name: &str,
     accept: bool,
diff --git a/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json
index 991d98a76..293ab86db 100644
--- a/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json
@@ -1,8 +1,8 @@
 [
   {
-    "x": 0
+    "UserName(x)": 0
   },
   {
-    "x": 1
+    "UserName(x)": 1
   }
 ]
\ No newline at end of file
diff --git a/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json
index a35964e6c..261073022 100644
--- a/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json
@@ -1,18 +1,18 @@
 [
   {
-    "x": 0,
-    "y": 0
+    "UserName(x)": 0,
+    "UserName(y)": 0
   },
   {
-    "x": 0,
-    "y": 1
+    "UserName(x)": 0,
+    "UserName(y)": 1
   },
   {
-    "x": 1,
-    "y": 0
+    "UserName(x)": 1,
+    "UserName(y)": 0
   },
   {
-    "x": 1,
-    "y": 1
+    "UserName(x)": 1,
+    "UserName(y)": 1
   }
 ]
\ No newline at end of file
diff --git a/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json
index 04c3691bb..41f27f106 100644
--- a/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json
@@ -1,10 +1,10 @@
 [
   {
-    "x": 0,
-    "y": 1
+    "UserName(x)": 0,
+    "UserName(y)": 1
   },
   {
-    "x": 1,
-    "y": 0
+    "UserName(x)": 1,
+    "UserName(y)": 0
   }
 ]
\ No newline at end of file
diff --git a/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json
index 16e182aab..ed1979f9f 100644
--- a/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json
@@ -1,7 +1,7 @@
 [
   {
-    "0": 3,
-    "a": 3,
-    "b": 3
+    "MachineName(0)": 3,
+    "UserName(a)": 3,
+    "UserName(b)": 3
   }
 ]
\ No newline at end of file
diff --git a/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json
index fb8e40563..82b2c192c 100644
--- a/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json
@@ -1,42 +1,42 @@
 [
   {
-    "0": 1,
-    "a": 1,
-    "b": 1
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 1
   },
   {
-    "0": 1,
-    "a": 1,
-    "b": 2
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 2
   },
   {
-    "0": 1,
-    "a": 1,
-    "b": 3
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 3
   },
   {
-    "0": 1,
-    "a": 2,
-    "b": 1
+    "MachineName(0)": 1,
+    "UserName(a)": 2,
+    "UserName(b)": 1
   },
   {
-    "0": 1,
-    "a": 3,
-    "b": 1
+    "MachineName(0)": 1,
+    "UserName(a)": 3,
+    "UserName(b)": 1
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 2
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 3
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 3
   },
   {
-    "0": 2,
-    "a": 3,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 3,
+    "UserName(b)": 2
   }
 ]
\ No newline at end of file
diff --git a/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json
index 9f4798a80..13d32026b 100644
--- a/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json
@@ -1,37 +1,37 @@
 [
   {
-    "0": 1,
-    "a": 1,
-    "b": 2
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 2
   },
   {
-    "0": 1,
-    "a": 1,
-    "b": 3
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 3
   },
   {
-    "0": 1,
-    "a": 1,
-    "b": 4
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 4
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 2
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 3
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 3
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 4
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 4
   },
   {
-    "0": 2,
-    "a": 3,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 3,
+    "UserName(b)": 2
   }
 ]
\ No newline at end of file
diff --git a/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json
index c326a64db..b3ae27c7a 100644
--- a/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json
@@ -1,47 +1,47 @@
 [
   {
-    "0": 1,
-    "a": 1,
-    "b": 2
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 2
   },
   {
-    "0": 1,
-    "a": 1,
-    "b": 3
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 3
   },
   {
-    "0": 1,
-    "a": 1,
-    "b": 4
+    "MachineName(0)": 1,
+    "UserName(a)": 1,
+    "UserName(b)": 4
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 2
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 3
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 3
   },
   {
-    "0": 2,
-    "a": 2,
-    "b": 4
+    "MachineName(0)": 2,
+    "UserName(a)": 2,
+    "UserName(b)": 4
   },
   {
-    "0": 2,
-    "a": 3,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 3,
+    "UserName(b)": 2
   },
   {
-    "0": 2,
-    "a": 4,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 4,
+    "UserName(b)": 2
   },
   {
-    "0": 2,
-    "a": 5,
-    "b": 2
+    "MachineName(0)": 2,
+    "UserName(a)": 5,
+    "UserName(b)": 2
   }
 ]
\ No newline at end of file
diff --git a/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json
index 24874137f..1cc649f7c 100644
--- a/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json
+++ b/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json
@@ -1,12 +1,12 @@
 [
   {
-    "a": 1,
-    "b": 1,
-    "c": 2
+    "UserName(a)": 1,
+    "UserName(b)": 1,
+    "UserName(c)": 2
   },
   {
-    "a": 2,
-    "b": 1,
-    "c": 1
+    "UserName(a)": 2,
+    "UserName(b)": 1,
+    "UserName(c)": 1
   }
 ]
\ No newline at end of file