diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 951bc6e7..004ed7f2 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -2061,7 +2061,7 @@ module Make(Plugin : PLUGIN)
     let c = Clause.make c Hyp in
     add_clause_ st c
 
-  let solve (st:t) ?(assumptions=[]) () : res =
+  let solve ?(assumptions=[]) (st:t) : res =
     cancel_until st 0;
     Vec.clear st.assumptions;
     List.iter (Vec.push st.assumptions) assumptions;
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index dbc3bd4d..f21f958c 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -433,7 +433,7 @@ module type S = sig
   val add_clause_a : t -> atom array -> unit
   (** Lower level addition of clauses *)
 
-  val solve : t -> ?assumptions:atom list -> unit -> res
+  val solve : ?assumptions:atom list -> t -> res
   (** Try and solves the current set of clauses.
       @param assumptions additional atomic assumptions to be temporarily added.
         The assumptions are just used for this call to [solve], they are
diff --git a/src/main/main.ml b/src/main/main.ml
index b4f86061..eb13666c 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -37,7 +37,7 @@ module Process = struct
     List.for_all (fun x -> x) l
 
   let prove ~assumptions () =
-    let res = S.solve st ~assumptions () in
+    let res = S.solve ~assumptions st in
     let t = Sys.time () in
     begin match res with
       | S.Sat state ->
diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml
index 8b05c6f8..0dfb04fc 100644
--- a/src/sudoku/sudoku_solve.ml
+++ b/src/sudoku/sudoku_solve.ml
@@ -263,7 +263,7 @@ end = struct
     Log.debugf 2
       (fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);
     let r =
-      match S.solve self.solver ~assumptions () with
+      match S.solve self.solver ~assumptions with
       | S.Sat _ -> Some (Theory.grid (S.theory self.solver))
       | S.Unsat _ -> None
     in
diff --git a/tests/icnf-solve/icnf_solve.ml b/tests/icnf-solve/icnf_solve.ml
index 4115237b..d6b2467b 100644
--- a/tests/icnf-solve/icnf_solve.ml
+++ b/tests/icnf-solve/icnf_solve.ml
@@ -68,7 +68,7 @@ module Solver = struct
   let to_int a : int = F.to_int @@ S.Atom.formula a
   let solve s ass =
     let ass = Array.to_list ass in
-    match S.solve ~assumptions:ass s () with
+    match S.solve ~assumptions:ass s with
     | S.Sat _ -> Ok ()
     | S.Unsat { unsat_assumptions; _ } ->
       let core = unsat_assumptions() in