diff --git a/conjure_oxide/src/ast.rs b/conjure_oxide/src/ast.rs
index 8bfd3bf0f5..90f583f13d 100644
--- a/conjure_oxide/src/ast.rs
+++ b/conjure_oxide/src/ast.rs
@@ -45,6 +45,4 @@ pub enum Expression {
     Sum(Vec<Expression>),
     Eq(Box<Expression>, Box<Expression>),
     Geq(Box<Expression>, Box<Expression>),
-    Not(Box<Expression>),
-    Or(Vec<Expression>),
 }
diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs
index 1ddc3a6704..851c0bc27f 100644
--- a/conjure_oxide/src/lib.rs
+++ b/conjure_oxide/src/lib.rs
@@ -1,2 +1 @@
 pub mod ast;
-mod solvers;
\ No newline at end of file
diff --git a/conjure_oxide/src/solvers/kissat.rs b/conjure_oxide/src/solvers/kissat.rs
deleted file mode 100644
index c3002d6610..0000000000
--- a/conjure_oxide/src/solvers/kissat.rs
+++ /dev/null
@@ -1,113 +0,0 @@
-use crate::ast::{DecisionVariable, Domain, Expression, Model, Name};
-use std::collections::HashMap;
-use String;
-
-type CNF = Vec<Vec<i32>>;
-type Error = String;
-
-/// Loop over variable names and assign indices to them for the CNF format. If a variable is not boolean, raise error.
-fn make_indices(vars: &HashMap<Name, DecisionVariable>) -> Result<HashMap<&Name, i32>, Error> {
-    let mut ans: HashMap<&Name, i32> = HashMap::new();
-    let mut next_index = 1;
-
-    for name in vars.keys() {
-        let variable: &DecisionVariable = vars.get(name).unwrap();
-        match variable.domain {
-            Domain::BoolDomain => {
-                ans.insert(name, next_index);
-                next_index += 1;
-            }
-            _ => {
-                return Err(String::from(
-                    "Could not convert (Model -> CNF):\
-                 all variables must belong to domain BoolDomain!",
-                ))
-            }
-        }
-    }
-
-    return Ok(ans);
-}
-
-/// Convert a single expression into a row of the CNF format
-fn convert_expression(
-    expression: &Expression,
-    symbol_table: &HashMap<&Name, i32>,
-) -> Result<Vec<i32>, Error> {
-    let mut ans: Vec<i32> = vec![];
-
-    match expression {
-        Expression::Reference(name) => match symbol_table.get(&name) {
-            // If it's a variable, just get its index
-            None => {
-                let str_name = match name {
-                    Name::UserName(s_name) => s_name.clone(),
-                    Name::MachineName(i_name) => i_name.to_string(),
-                };
-                return Err(format!("Variable with name {str_name} not found!"));
-            }
-            Some(ind) => {
-                ans.push(*ind);
-            }
-        },
-        Expression::Not(var_box) => {
-            let expr = var_box.as_ref();
-            match expr {
-                // Expression inside the Not()
-                Expression::Reference(_) => {
-                    // If it's a variable, get its index by calling
-                    // convert_expression again, and add a -
-                    let ret = convert_expression(expr, symbol_table)?;
-                    let ind = *ret.first().unwrap();
-                    ans.push(-ind);
-                }
-                _ => {
-                    return Err(String::from(
-                        "Expected Model to be in CNF form,\
-                 expression inside Not must always be a Reference!",
-                    ))
-                }
-            }
-        }
-        Expression::Or(expressions) => {
-            // If it's an Or, we just need to convert expressions inside it and flatten the result
-            for expr in expressions {
-                let ret = convert_expression(expr, symbol_table)?;
-                for ind in ret {
-                    ans.push(ind);
-                }
-            }
-        }
-        _ => {
-            return Err(String::from(
-                "Expected Model to be in CNF form,\
-        only Reference, Not(Reference) and Or(...) allowed!",
-            ))
-        }
-    }
-
-    return Ok(ans);
-}
-
-/// Expects Model to be in the Conjunctive Normal Form:
-/// - All variables must be boolean
-/// - Expressions must be Reference, Not(Reference), or Or(Reference1, Not(Reference2), ...)
-impl TryFrom<Model> for CNF {
-    type Error = Error;
-    fn try_from(conjure_model: Model) -> Result<Self, Self::Error> {
-        let mut ans: Vec<Vec<i32>> = vec![];
-        let constraints = conjure_model.constraints;
-        let variables = conjure_model.variables;
-
-        let names_to_indices: HashMap<&Name, i32> = make_indices(&variables)?;
-
-        for expression in constraints.iter() {
-            match convert_expression(expression, &names_to_indices) {
-                Ok(row) => ans.push(row),
-                Err(msg) => return Err(format!("Could not convert (Model -> CNF): {msg}")),
-            }
-        }
-
-        return Ok(ans);
-    }
-}
diff --git a/conjure_oxide/src/solvers/mod.rs b/conjure_oxide/src/solvers/mod.rs
deleted file mode 100644
index 7b58d4848e..0000000000
--- a/conjure_oxide/src/solvers/mod.rs
+++ /dev/null
@@ -1 +0,0 @@
-pub mod kissat;
\ No newline at end of file
diff --git a/solvers/chuffed/libwrapper.a b/solvers/chuffed/libwrapper.a
index ece196ecc0..2b9638b4f3 100644
Binary files a/solvers/chuffed/libwrapper.a and b/solvers/chuffed/libwrapper.a differ
diff --git a/solvers/chuffed/wrapper.o b/solvers/chuffed/wrapper.o
index 6af35caa0d..5a70149840 100644
Binary files a/solvers/chuffed/wrapper.o and b/solvers/chuffed/wrapper.o differ